bddAbove_image — Mathlib

English

If s is bounded above, then its image under any function is bounded above as well.

Русский

Если множество ограничено сверху, то и его образ под любой функцией ограничен сверху.

LaTeX

$$$BddAbove\ s \Rightarrow BddAbove\ (f''s)$$$

Lean4

theorem bddAbove_image {s : Set Ordinal.{u}} (hf : BddAbove s) (f : Ordinal.{u} → Ordinal.{max u v}) :
    BddAbove (f '' s) := by
  rw [bddAbove_iff_small] at hf ⊢
  exact small_lift _

Похожие утверждения