iSup_exists — Mathlib

English

Let p be a predicate and f: Exists p → α. Then iSup over all x is equal to iSup over pairs (i,h) with x = ⟨i,h⟩.

Русский

Пусть p — предикат и f: Exists p → α. Тогда iSup по всем x равен iSup над парами (i,h) с x = ⟨i,h⟩.

LaTeX

$$$\\\\bigvee_{x} f(x) = \\\\bigvee_{i} \\\\bigvee_{h} f(i,h)$$$

Lean4

@[simp]
theorem iSup_exists {p : ι → Prop} {f : Exists p → α} : ⨆ x, f x = ⨆ (i) (h), f ⟨i, h⟩ :=
  le_antisymm (iSup_le fun ⟨i, h⟩ => @le_iSup₂ _ _ _ _ (fun _ _ => _) i h) (iSup₂_le fun _ _ => le_iSup _ _)

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