linearGrowthSup_const — Mathlib

English

For any b ∈ EReal with b ≠ ⊥ and b ≠ ⊤, linearGrowthSup(const b) = 0.

Русский

Для любого константного b ∈ EReal с b ≠ ⊥ и b ≠ ⊤, linearGrowthSup(const b) = 0.

LaTeX

$$$\operatorname{linearGrowthSup}(\lambda n. b) = 0$ при $b \neq \perp$ и $b \neq \top$.$$

Lean4

theorem linearGrowthSup_const (h : b ≠ ⊥) (h' : b ≠ ⊤) : linearGrowthSup (fun _ ↦ b) = 0 :=
  (tendsto_const_div_atTop_nhds_zero_nat h h').limsup_eq

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