# Metamath Proof Explorer

## Definition df-liminf

Description: Define the inferior limit of a sequence of extended real numbers. (Contributed by GS, 2-Jan-2022)

Ref Expression
Assertion df-liminf ${⊢}\mathrm{lim inf}=\left({x}\in \mathrm{V}⟼sup\left(\mathrm{ran}\left({k}\in ℝ⟼sup\left({x}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 clsi ${class}\mathrm{lim inf}$
1 vx ${setvar}{x}$
2 cvv ${class}\mathrm{V}$
3 vk ${setvar}{k}$
4 cr ${class}ℝ$
5 1 cv ${setvar}{x}$
6 3 cv ${setvar}{k}$
7 cico ${class}\left[.\right)$
8 cpnf ${class}\mathrm{+\infty }$
9 6 8 7 co ${class}\left[{k},\mathrm{+\infty }\right)$
10 5 9 cima ${class}{x}\left[\left[{k},\mathrm{+\infty }\right)\right]$
11 cxr ${class}{ℝ}^{*}$
12 10 11 cin ${class}\left({x}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}\right)$
13 clt ${class}<$
14 12 11 13 cinf ${class}sup\left({x}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)$
15 3 4 14 cmpt ${class}\left({k}\in ℝ⟼sup\left({x}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)$
16 15 crn ${class}\mathrm{ran}\left({k}\in ℝ⟼sup\left({x}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)$
17 16 11 13 csup ${class}sup\left(\mathrm{ran}\left({k}\in ℝ⟼sup\left({x}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)$
18 1 2 17 cmpt ${class}\left({x}\in \mathrm{V}⟼sup\left(\mathrm{ran}\left({k}\in ℝ⟼sup\left({x}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)\right)$
19 0 18 wceq ${wff}\mathrm{lim inf}=\left({x}\in \mathrm{V}⟼sup\left(\mathrm{ran}\left({k}\in ℝ⟼sup\left({x}\left[\left[{k},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)\right)$