linearGrowthSup_iSup — Mathlib

English

For finite index set, linearGrowthSup (iSup i, u i) equals iSup i, linearGrowthSup (u i).

Русский

Для конечного индекса: верхний рост от iSup совпадает с iSup верхних ростов.

LaTeX

$$$\operatorname{linearGrowthSup}\bigl(\iSup i\, u(i)\bigr) = \iSup i\, \operatorname{linearGrowthSup}(u(i))$$$

Lean4

theorem linearGrowthSup_iSup {ι : Type*} [Finite ι] (u : ι → ℕ → EReal) :
    linearGrowthSup (⨆ i, u i) = ⨆ i, linearGrowthSup (u i) := by
  rw [← iSup_univ, linearGrowthSup_biSup u Set.finite_univ, iSup_univ]

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