leftInverse_nat — Mathlib

English

The natural-number embedding and projection form a left-inverse pair: applying toNat after ofNat yields the original number. In symbols, toNat(ofNat n) = n for all n.

Русский

Встраивание в W-type и проекция образуют левую обратную пару: применяя toNat кOfNat(n) мы получаем n.

LaTeX

$$$$\forall n,\ \mathrm{toNat}(\mathrm{WType.ofNat}(n))=n.$$$$

Lean4

theorem leftInverse_nat : Function.LeftInverse ofNat toNat
  | WType.mk Natα.zero f => by
    rw [toNat, ofNat]
    congr
    ext x
    cases x
  | WType.mk Natα.succ f =>
    by
    simp only [toNat, ofNat, leftInverse_nat (f ()), mk.injEq, heq_eq_eq, true_and]
    rfl

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