iSup_psigma — Mathlib

English

Let f : (i, j) ↦ α with i ∈ β and j ∈ κ i. Then iSup over i, j of f i j equals iSup over i of iSup over j of f (i, j).

Русский

Пусть f : (i, j) → α, где j ∈ κ i. Тогда iSup по i и j равен iSup по i, потом по j, от f(i,j).

LaTeX

$$$$ \iSup_{ij} f_{ij} = \iSup_i \iSup_j f_{ij} $$$$

Lean4

theorem iSup_psigma {ι : Sort*} {κ : ι → Sort*} (f : (Σ' i, κ i) → α) : ⨆ ij, f ij = ⨆ i, ⨆ j, f ⟨i, j⟩ :=
  eq_of_forall_ge_iff fun c ↦ by simp only [iSup_le_iff, PSigma.forall]

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