English
The image of the infimum of a set equals the infimum of the image.
Русский
Образ наименьшего элемента множества через включение равен наименьшему элементу образа.
LaTeX
$$$ (\\uparrow)(\\mathrm{sInf}\\ s) = \\mathrm{sInf}\\ ((\\uparrow)'' s). $$$
Lean4
@[norm_cast]
theorem coe_sInf (s : Set ℝ≥0) : (↑(sInf s) : ℝ) = sInf (((↑) : ℝ≥0 → ℝ) '' s) :=
by
rcases Set.eq_empty_or_nonempty s with rfl | hs
· simp only [Set.image_empty, Real.sInf_empty, coe_eq_zero]
exact @subset_sInf_emptyset ℝ (Set.Ici (0 : ℝ)) _ _ (_)
have A : sInf (Subtype.val '' s) ∈ Set.Ici 0 :=
by
apply Real.sInf_nonneg
rintro - ⟨y, -, rfl⟩
exact y.2
exact (@subset_sInf_of_within ℝ (Set.Ici (0 : ℝ)) _ _ (_) s hs (OrderBot.bddBelow s) A).symm
