lift_cof — Mathlib

English

For any ordinal o, lift(cof o) equals cof(lift o).

Русский

Для любого ординала o: lift(cof o) = cof(lift o).

LaTeX

$$$\\operatorname{lift}\\big(\\operatorname{cof} o\\big) = \\operatorname{cof}(\\operatorname{lift} o)$$$

Lean4

@[simp]
theorem lift_cof (o) : Cardinal.lift.{u, v} (cof o) = cof (Ordinal.lift.{u, v} o) :=
  by
  refine inductionOn o fun α r _ ↦ ?_
  rw [← type_uLift, cof_type, cof_type, ← Cardinal.lift_id'.{v, u} (Order.cof _), ← Cardinal.lift_umax]
  apply RelIso.cof_eq_lift ⟨Equiv.ulift.symm, _⟩
  simp [swap]

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