linearGrowthSup_bot — Mathlib

English

linearGrowthSup of the all-zero sequence equals zero.

Русский

linearGrowthSup последовательности, все элементы которой ноль, равен нулю.

LaTeX

$$$\operatorname{linearGrowthSup}(\mathbf{0}) = 0.$$$

Lean4

theorem linearGrowthSup_bot : linearGrowthSup (⊥ : ℕ → EReal) = (⊥ : EReal) :=
  by
  nth_rw 2 [← limsup_const (f := atTop (α := ℕ)) ⊥]
  refine limsup_congr <| (eventually_gt_atTop 0).mono fun n n_pos ↦ ?_
  exact bot_div_of_pos_ne_top (by positivity) (natCast_ne_top n)

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