English
Assume Nonempty β and s ⊆ β. For f : β → α and g : s → α with appropriate bounds, the supremum of the image f '' s under g equals the supremum over a ∈ s of g(a).
Русский
Пусть β непусто, s ⊆ β. Для f: β → α и g: s → α с соответствующими границами, верхняя граница образа f''s через g равна верхней границе по s.
LaTeX
$$$\sup (f''s) = \sup_{a \in s} g(a).$$$
Lean4
theorem csSup_image [Nonempty β] {s : Set β} (hs : s.Nonempty) {f : β → α} (hf : BddAbove (Set.range fun i : s ↦ f i))
(hf' : sSup ∅ ≤ ⨆ i : s, f i) : sSup (f '' s) = ⨆ a ∈ s, f a := by
rw [← ciSup_subtype'' hs hf hf', iSup, Set.image_eq_range]