lt_univ — Mathlib

English

A cardinal c is strictly less than the universe iff there exists c' with c = lift(c').

Русский

Кардинал c меньше универсума тогда и только тогда, когда существует c' такой, что c = lift(c').

LaTeX

$$$c < \\mathrm{univ} \\iff \\exists c',\\ c = \\mathrm{lift}(c')$$$

Lean4

theorem lt_univ {c} : c < univ.{u, u + 1} ↔ ∃ c', c = lift.{u + 1, u} c' :=
  ⟨fun h => by
    have := ord_lt_ord.2 h
    rw [ord_univ] at this
    obtain ⟨o, e⟩ := liftPrincipalSeg.mem_range_of_rel_top (by simpa only [liftPrincipalSeg_top])
    have := card_ord c
    rw [← e, liftPrincipalSeg_coe, ← lift_card] at this
    exact ⟨_, this.symm⟩, fun ⟨_, e⟩ => e.symm ▸ lift_lt_univ _⟩

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