iSup_subtype — Mathlib

English

Let p be a predicate on ι and f : Subtype p → α. Then the supremum of f equals the supremum over i of f restricted to i together with its witness h: p i.

Русский

Пусть p — предикат на ι и f : Subtype p → α. Тогда ⨆ f = ⨆_{i} ⨆_{h : p i} f⟨i,h⟩.

LaTeX

$$$$\bigvee_{i : ι} \bigvee_{h : p i} f(i,h) = \bigvee_{x : Subtype p} f(x.x, x.property).$$$$

Lean4

theorem iSup_subtype {p : ι → Prop} {f : Subtype p → α} : iSup f = ⨆ (i) (h : p i), f ⟨i, h⟩ :=
  le_antisymm (iSup_le fun ⟨i, h⟩ => @le_iSup₂ _ _ p _ (fun i h => f ⟨i, h⟩) i h) (iSup₂_le fun _ _ => le_iSup _ _)

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