lift_lt_univ — Mathlib

English

For any cardinal c, lift^{u+1,u} c is strictly less than univ^{u,u+1}.

Русский

Для любого кардинала c, lift^{u+1,u} c строго меньше univ^{u,u+1}.

LaTeX

$$$\\mathrm{lift}^{u+1,u} c < \\mathrm{univ}^{u,u+1}$$$

Lean4

theorem lift_lt_univ (c : Cardinal) : lift.{u + 1, u} c < univ.{u, u + 1} := by
  simpa only [liftPrincipalSeg_coe, lift_ord, lift_succ, ord_le, succ_le_iff] using
    le_of_lt (liftPrincipalSeg.{u, u + 1}.lt_top (succ c).ord)

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