linearGrowthSup_biSup — Mathlib

English

For α finite, linearGrowthSup (⨆ x ∈ s, u x) = ⨆ x ∈ s, linearGrowthSup (u x).

Русский

Для конечной множества x ∈ s: линейный верхний рост от суммирования равен верхнему росту по каждому x.

LaTeX

$$$\operatorname{linearGrowthSup}\bigl(\sup_{x\in s} u(x)\bigr) = \sup_{x\in s} \operatorname{linearGrowthSup}(u(x))$$$

Lean4

theorem linearGrowthSup_biSup {α : Type*} (u : α → ℕ → EReal) {s : Set α} (hs : s.Finite) :
    linearGrowthSup (⨆ x ∈ s, u x) = ⨆ x ∈ s, linearGrowthSup (u x) :=
  by
  have := map_finset_sup linearGrowthSupBotHom hs.toFinset u
  simpa only [linearGrowthSupBotHom, SupBotHom.coe_mk, SupHom.coe_mk, Finset.sup_eq_iSup, hs.mem_toFinset, comp_apply]

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