bddAbove_ord_image_iff — Mathlib

English

The image of a set under ord is bounded above iff the original set is bounded above.

Русский

Образ при ORD образе множества ограничен сверху тогда и только тогда, когда исходное множество ограничено сверху.

LaTeX

$$$\operatorname{BddAbove}(\operatorname{ord}'' s) \iff \operatorname{BddAbove}(s)$$$

Lean4

theorem bddAbove_ord_image_iff {s : Set Cardinal} : BddAbove (ord '' s) ↔ BddAbove s :=
  gc_ord_card.bddAbove_l_image

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