iSup_psigma' — Mathlib

English

Let f : (i) → (κ i → α). Then iSup over i of iSup over j equals iSup over x : Σ i, κ i of f x.fst x.snd.

Русский

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

LaTeX

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

Lean4

theorem iSup_psigma' {ι : Sort*} {κ : ι → Sort*} (f : ∀ i, κ i → α) :
    (⨆ i, ⨆ j, f i j) = ⨆ ij : Σ' i, κ i, f ij.1 ij.2 :=
  (iSup_psigma fun x ↦ f x.1 x.2).symm

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