iSup_sigma — Mathlib

English

Let p: β → Type and f : Σ p → α. Then iSup over x equals iSup over i, j of f ⟨i, j⟩.

Русский

Пусть p: β → Type и f : Σ p → α. Тогда iSup по x равен iSup по i, j: f ⟨i, j⟩.

LaTeX

$$$$ \iSup_{x} f x = \iSup_{i} \iSup_{j} f \langle i, j \rangle $$$$

Lean4

theorem iSup_sigma {p : β → Type*} {f : Sigma p → α} : ⨆ x, f x = ⨆ (i) (j), f ⟨i, j⟩ :=
  eq_of_forall_ge_iff fun c => by simp only [iSup_le_iff, Sigma.forall]

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