English
Let α and β be preordered sets and f: α → β be monotone. If a set s ⊆ α is bounded above, then the image f''s is bounded above in β; in particular f(C) is an upper bound for all elements of f''s when C is an upper bound for s.
Русский
Пусть α и β — упорядоченные множества, f: α → β монотонна. Если множество s ⊆ α ограничено сверху, то образ f''s в β тоже ограничен сверху; в частности f(C) является верхней гранью для всех элементов f''s, если C — верхняя грань для s.
LaTeX
$$$\operatorname{BddAbove}(s) \Rightarrow \operatorname{BddAbove}(f'' s)$$$
Lean4
/-- The image under a monotone function of a set which is bounded above is bounded above. See also
`BddAbove.image2`. -/
theorem map_bddAbove : BddAbove s → BddAbove (f '' s)
| ⟨C, hC⟩ => ⟨f C, Hf.mem_upperBounds_image hC⟩
