English
If f is monotone on the closed interval Icc[a,b], the infimum of the image f''Icc[a,b] is f(a).
Русский
Пусть f монотонна на окрестности Icc[a,b]. Тогда inf{ f(x) : x ∈ Icc[a,b] } равен f(a).
LaTeX
$$$[Preorder\ \alpha][ConditionallyCompleteLattice\ \beta]\ {f:\alpha\to\beta}\ {a,b:\alpha}\ (hab: a \le b) (h': MonotoneOn f (Icc a b)) : sInf (f '' Icc a b) = f a$$$
Lean4
theorem sInf_image_Icc [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {a b : α} (hab : a ≤ b)
(h' : MonotoneOn f (Icc a b)) : sInf (f '' Icc a b) = f a :=
by
refine IsGLB.csInf_eq ?_ ((nonempty_Icc.mpr hab).image f)
refine isGLB_iff_le_iff.mpr (fun b' ↦ ⟨?_, ?_⟩)
· intro hb'
rintro _ ⟨x, hx, rfl⟩
exact hb'.trans <| h' (left_mem_Icc.mpr hab) hx hx.1
· exact fun hb' ↦ hb' ⟨a, by simp [hab]⟩
