iSup_subtype' — Mathlib

English

Let p be a predicate on ι and f : ∀ i, p i → α. Then the supremum over i of f(i, h) with h varying equals the supremum over x : Subtype p of f(x.x, x.y).

Русский

Пусть p — предикат на ι и f : ∀ i, p i → α. Тогда ⨆ i h f(i,h) = ⨆ x : Subtype p, f x x.property.

LaTeX

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

Lean4

theorem iSup_subtype' {p : ι → Prop} {f : ∀ i, p i → α} : ⨆ (i) (h), f i h = ⨆ x : Subtype p, f x x.property :=
  (@iSup_subtype _ _ _ p fun x => f x.val x.property).symm

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