linearGrowthInf_bot — Mathlib

English

linearGrowthInf of the all-bottom sequence equals bottom.

Русский

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

LaTeX

$$$\operatorname{linearGrowthInf}(\mathbf{\bot}) = \mathbf{\bot}.$$$

Lean4

theorem linearGrowthInf_bot : linearGrowthInf (⊥ : ℕ → EReal) = (⊥ : EReal) :=
  by
  apply le_bot_iff.1
  rw [← linearGrowthSup_bot]
  exact linearGrowthInf_le_linearGrowthSup

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