English
The real-valued supremum of a set corresponds to the supremum of its image under the inclusion.
Русский
Верхняя грань множества в ℝ соответствует сверхуобразу его образа при включении.
LaTeX
$$$ \\uparrow(\\mathrm{sSup}\\, s) = \\mathrm{sSup}\\, (\\uparrow)'' s. $$$
Lean4
@[norm_cast]
theorem coe_sSup (s : Set ℝ≥0) : (↑(sSup s) : ℝ) = sSup (((↑) : ℝ≥0 → ℝ) '' s) :=
by
rcases Set.eq_empty_or_nonempty s with rfl | hs
· simp
by_cases H : BddAbove s
· have A : sSup (Subtype.val '' s) ∈ Set.Ici 0 :=
by
apply Real.sSup_nonneg
rintro - ⟨y, -, rfl⟩
exact y.2
exact (@subset_sSup_of_within ℝ (Set.Ici (0 : ℝ)) _ _ (_) s hs H A).symm
· simp only [csSup_of_not_bddAbove H, csSup_empty, bot_eq_zero', NNReal.coe_zero]
apply (Real.sSup_of_not_bddAbove ?_).symm
contrapose! H
exact bddAbove_coe.1 H
