Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-liminf Structured version   Visualization version   GIF version

Definition df-liminf 40502
 Description: Define the inferior limit of a sequence of extended real numbers. (Contributed by GS, 2-Jan-2022.)
Assertion
Ref Expression
df-liminf lim inf = (𝑥 ∈ V ↦ sup(ran (𝑘 ∈ ℝ ↦ inf(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
Distinct variable group:   𝑥,𝑘

Detailed syntax breakdown of Definition df-liminf
StepHypRef Expression
1 clsi 40501 . 2 class lim inf
2 vx . . 3 setvar 𝑥
3 cvv 3351 . . 3 class V
4 vk . . . . . 6 setvar 𝑘
5 cr 10137 . . . . . 6 class
62cv 1630 . . . . . . . . 9 class 𝑥
74cv 1630 . . . . . . . . . 10 class 𝑘
8 cpnf 10273 . . . . . . . . . 10 class +∞
9 cico 12382 . . . . . . . . . 10 class [,)
107, 8, 9co 6793 . . . . . . . . 9 class (𝑘[,)+∞)
116, 10cima 5252 . . . . . . . 8 class (𝑥 “ (𝑘[,)+∞))
12 cxr 10275 . . . . . . . 8 class *
1311, 12cin 3722 . . . . . . 7 class ((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*)
14 clt 10276 . . . . . . 7 class <
1513, 12, 14cinf 8503 . . . . . 6 class inf(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )
164, 5, 15cmpt 4863 . . . . 5 class (𝑘 ∈ ℝ ↦ inf(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))
1716crn 5250 . . . 4 class ran (𝑘 ∈ ℝ ↦ inf(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))
1817, 12, 14csup 8502 . . 3 class sup(ran (𝑘 ∈ ℝ ↦ inf(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < )
192, 3, 18cmpt 4863 . 2 class (𝑥 ∈ V ↦ sup(ran (𝑘 ∈ ℝ ↦ inf(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
201, 19wceq 1631 1 wff lim inf = (𝑥 ∈ V ↦ sup(ran (𝑘 ∈ ℝ ↦ inf(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
 Colors of variables: wff setvar class This definition is referenced by:  liminfval  40509
 Copyright terms: Public domain W3C validator