lift_ofNat — Mathlib

English

The lift of ofNat(n) equals the canonical nat-embedding of n, i.e. lift(ofNat(n)) = OfNat.ofNat(n).

Русский

Подъём ofNat(n) равен естественному отображению n как натурального числа: lift(ofNat(n)) = OfNat.ofNat(n).

LaTeX

$$$\\\\operatorname{lift}\\\\operatorname{ofNat}(n) = \\\\operatorname{OfNat}.ofNat(n).$$$

Lean4

@[simp]
theorem lift_ofNat (n : ℕ) [n.AtLeastTwo] : lift ofNat(n) (WithTop.coe_lt_top n) = OfNat.ofNat n :=
  rfl

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