linearGrowthInf_const_mul_self — Mathlib

English

For any a ∈ EReal, linearGrowthInf(n ↦ a • n) = a.

Русский

Для любого a ∈ EReal линейный инфим последовательности n ↦ a • n равен a.

LaTeX

$$$\operatorname{linearGrowthInf}(n \mapsto a \cdot n) = a.$$$

Lean4

theorem linearGrowthInf_const_mul_self : linearGrowthInf (fun n ↦ a * n) = a :=
  le_antisymm (Frequently.linearGrowthInf_le (Frequently.of_forall fun _ ↦ le_refl _))
    (Eventually.le_linearGrowthInf (Eventually.of_forall fun _ ↦ le_refl _))

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