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