toENat_lift — Mathlib

English

For any cardinal a, toENat(lift a) = toENat a.

Русский

Для любого кардинала a значение toENat сохраняется под подъемом по вселенной: toENat(lift(a)) = toENat(a).

LaTeX

$$$\\mathrm{toENat}(\\mathrm{lift}(a)) = \\mathrm{toENat}(a)$$$

Lean4

@[simp]
theorem toENat_lift {a : Cardinal.{v}} : toENat (lift.{u} a) = toENat a := by
  cases le_total a ℵ₀ with
  | inl ha => lift a to ℕ∞ using ha; simp
  | inr ha => simp [toENat_eq_top.2, ha]

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