csSup_image — Mathlib

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]

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