lift_ofENat — Mathlib

English

The lifting to a higher universes fixes ENat: lift m = m for all m ∈ ℕ∞, with the natural cases for finite and infinite values.

Русский

Переложение в более общую вселенную фиксирует ENat: lift m = m для всех m ∈ ℕ∞, имеются естественные случаи для конечных и бесконечных значений.

LaTeX

$$∀ m : \mathbb{N}_\infty, \mathrm{lift}(m) = m$$

Lean4

@[simp, norm_cast]
theorem lift_ofENat : ∀ m : ℕ∞, lift.{u, v} m = m
  | (m : ℕ) => lift_natCast m
  | ⊤ => lift_aleph0

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