sSup_image — Mathlib

English

Let α be a complete lattice, β a type, s a subset of β, and f a function from β to α. Then the supremum of the image f''s equals the supremum over s of f.

Русский

Пусть α — полная решетка, β — множество, s ⊆ β, и f: β → α. Тогда супремум образа f''s равен супремуму по элементам s от f.

LaTeX

$$$$ \\sup\\{ f(x) : x \\in s \\} = \\sup_{a \\in s} f(a) $$$$

Lean4

theorem sSup_image {s : Set β} {f : β → α} : sSup (f '' s) = ⨆ a ∈ s, f a := by rw [← iSup_subtype'', sSup_image']

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