linearGrowthInf_const — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem linearGrowthInf_const (h : b ≠ ⊥) (h' : b ≠ ⊤) : linearGrowthInf (fun _ ↦ b) = 0 :=
  (tendsto_const_div_atTop_nhds_zero_nat h h').liminf_eq

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