linearGrowthInf_biInf — Mathlib

English

If u : α → ℕ → EReal with α finite, then linearGrowthInf (⨅ x ∈ α, u x) = ⨅ x ∈ α, linearGrowthInf (u x).

Русский

Пусть u : α → ℕ → EReal с α конечным, тогда linearGrowthInf(⨅ x∈α, u x) = ⨅ x∈α, linearGrowthInf(u x).

LaTeX

$$$\operatorname{linearGrowthInf}\Bigl(\inf_{x\in\alpha} u(x)\Bigr) = \inf_{x\in\alpha} \operatorname{linearGrowthInf}(u(x))$$$

Lean4

theorem linearGrowthInf_biInf {α : Type*} (u : α → ℕ → EReal) {s : Set α} (hs : s.Finite) :
    linearGrowthInf (⨅ x ∈ s, u x) = ⨅ x ∈ s, linearGrowthInf (u x) :=
  by
  have := map_finset_inf linearGrowthInfTopHom hs.toFinset u
  simpa only [linearGrowthInfTopHom, InfTopHom.coe_mk, InfHom.coe_mk, Finset.inf_eq_iInf, hs.mem_toFinset, comp_apply]

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