English
The image under a monotone function on a set t of a subset which has a lower bound in t is bounded below.
Русский
Образ монотонной функции на множесте t от подмножества, имеющего нижнюю грань в t, ограничен снизу.
LaTeX
$$$(Hf : MonotoneOn f t) \land (Hst : s \subseteq t) : (\mathrm{lowerBounds}(s) \cap t).Nonempty \Rightarrow \mathrm{BddBelow}(\mathrm{image}(f,s))$$$
Lean4
/-- The image under a monotone function on a set `t` of a subset which has a lower bound in `t`
is bounded below. -/
theorem map_bddBelow (Hf : MonotoneOn f t) (Hst : s ⊆ t) : (lowerBounds s ∩ t).Nonempty → BddBelow (f '' s) :=
fun ⟨C, hs, ht⟩ => ⟨f C, Hf.mem_lowerBounds_image Hst hs ht⟩
