sSup_image' — Mathlib

English

The supremum of the image of a set under f equals the supremum over the original elements: sSup (f '' s) = ⨆ a : s, (a : α).

Русский

Супремум образа множества под отображением f равен супремуму самих элементов множества: sSup (f '' s) = ⨆ a : s, (a : α).

LaTeX

$$$$ \operatorname{sSup}(\operatorname{Set.image} f s) = \bigvee_{a : s} (a : \alpha) $$$$

Lean4

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

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