linearGrowthInf_iInf — Mathlib

English

For α finite, linearGrowthInf (⨅ i ∈ α, u i) equals ⨅ i ∈ α, linearGrowthInf(u i).

Русский

Для конечного α справедливо: линейный Inf от склеенного минимума равен инфимууму линейного Inf по каждому i.

LaTeX

$$$\operatorname{linearGrowthInf}\Bigl(\inf_{i\in s} u(i)\Bigr) = \inf_{i\in s} \operatorname{linearGrowthInf}(u(i))$$$

Lean4

theorem linearGrowthInf_iInf {ι : Type*} [Finite ι] (u : ι → ℕ → EReal) :
    linearGrowthInf (⨅ i, u i) = ⨅ i, linearGrowthInf (u i) := by
  rw [← iInf_univ, linearGrowthInf_biInf u Set.finite_univ, iInf_univ]

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