This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-limsup

Description: Define the superior limit of an infinite sequence of extended real numbers. Definition 12-4.1 of Gleason p. 175. See limsupval for its value. (Contributed by NM, 26-Oct-2005) (Revised by AV, 11-Sep-2020)

Ref Expression
Assertion df-limsup ⊢ lim sup = x ∈ V ⟼ inf ran ⁡ k ∈ ℝ ⟼ sup x k +∞ ∩ ℝ * ℝ * < ℝ * <

Detailed syntax breakdown

Step Hyp Ref Expression
0 clsp class lim sup
1 vx setvar x
2 cvv class V
3 vk setvar k
4 cr class ℝ
5 1 cv setvar x
6 3 cv setvar k
7 cico class .
8 cpnf class +∞
9 6 8 7 co class k +∞
10 5 9 cima class x k +∞
11 cxr class ℝ *
12 10 11 cin class x k +∞ ∩ ℝ *
13 clt class <
14 12 11 13 csup class sup x k +∞ ∩ ℝ * ℝ * <
15 3 4 14 cmpt class k ∈ ℝ ⟼ sup x k +∞ ∩ ℝ * ℝ * <
16 15 crn class ran ⁡ k ∈ ℝ ⟼ sup x k +∞ ∩ ℝ * ℝ * <
17 16 11 13 cinf class inf ran ⁡ k ∈ ℝ ⟼ sup x k +∞ ∩ ℝ * ℝ * < ℝ * <
18 1 2 17 cmpt class x ∈ V ⟼ inf ran ⁡ k ∈ ℝ ⟼ sup x k +∞ ∩ ℝ * ℝ * < ℝ * <
19 0 18 wceq wff lim sup = x ∈ V ⟼ inf ran ⁡ k ∈ ℝ ⟼ sup x k +∞ ∩ ℝ * ℝ * < ℝ * <