bddAbove_iff_small — Mathlib

English

A set of cardinals is bounded above iff it is small.

Русский

Множество кардиналов ограничено сверху тогда и только тогда, когда оно мало.

LaTeX

$$$BddAbove\, s \iff Small\, s$$$

Lean4

/-- A set of cardinals is bounded above iff it's small, i.e. it corresponds to a usual ZFC set. -/
theorem bddAbove_iff_small {s : Set Cardinal.{u}} : BddAbove s ↔ Small.{u} s :=
  ⟨fun ⟨a, ha⟩ => @small_subset _ (Iic a) s (fun _ h => ha h) _,
    by
    rintro ⟨ι, ⟨e⟩⟩
    use sum.{u, u} fun x ↦ e.symm x
    intro a ha
    simpa using le_sum (fun x ↦ e.symm x) (e ⟨a, ha⟩)⟩

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