iSup_sigma' — Mathlib

English

Let f : (β) → (κ β → α). Then iSup over i of iSup over j of f i j equals iSup over x : Σ i, κ i, f x.1 x.2.

Русский

Пусть f : ∀ i, κ i → α. Тогда iSup по i и по j равен iSup по x : Σ i, κ i, f x.1 x.2.

LaTeX

$$$$ \iSup_{i} \iSup_{j} f i j = \iSup_{x : \Sigma i, \kappa i} f x.1 x.2 $$$$

Lean4

theorem iSup_sigma' {κ : β → Type*} (f : ∀ i, κ i → α) : (⨆ i, ⨆ j, f i j) = ⨆ x : Σ i, κ i, f x.1 x.2 :=
  (iSup_sigma (f := fun x ↦ f x.1 x.2)).symm

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