linearGrowthSup_const_mul_self — Mathlib

English

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

Русский

Для любого a ∈ EReal линейный суп индуктивно-подобной последовательности равен a.

LaTeX

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

Lean4

theorem linearGrowthSup_const_mul_self : linearGrowthSup (fun n ↦ a * n) = a :=
  le_antisymm (Eventually.linearGrowthSup_le (Eventually.of_forall fun _ ↦ le_refl _))
    (Frequently.le_linearGrowthSup (Frequently.of_forall fun _ ↦ le_refl _))

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