linearGrowthInf_top — Mathlib

English

linearGrowthInf of the top sequence equals top.

Русский

linearGrowthInf последовательности верхнего предела равен верхнему пределу.

LaTeX

$$$\operatorname{linearGrowthInf}(\top) = \top.$$$

Lean4

theorem linearGrowthInf_top : linearGrowthInf ⊤ = (⊤ : EReal) :=
  by
  nth_rw 2 [← liminf_const (f := atTop (α := ℕ)) ⊤]
  refine liminf_congr (eventually_atTop.2 ?_)
  exact ⟨1, fun n n_pos ↦ top_div_of_pos_ne_top (Nat.cast_pos'.2 n_pos) (natCast_ne_top n)⟩

Похожие утверждения