iSup_subtype'' — Mathlib

English

Let p be a predicate on ι and f assigns to each i with witness h : p i an α. Then the supremum over i with h of f i h equals the supremum over x : Subtype p of f x x.property.

Русский

Пусть p — предикат на ι, а f(i,h) задаёт элемент α. Тогда супремум по всем i с доказательством p(i) равен супремуму по всем элементам подпредельного множества: f(x, x.p).

LaTeX

$$$ \\sup_{i: ι} \\sup_{h: p(i)} f(i,h) = \\sup_{x: \\{ i : ι \\mid p(i) \\}} f(x.val, x.property) $$$

Lean4

theorem iSup_subtype'' {ι} (s : Set ι) (f : ι → α) : ⨆ i : s, f i = ⨆ (t : ι) (_ : t ∈ s), f t :=
  iSup_subtype

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