rightInverse_nat — Mathlib

English

The embedding and projection are inverse in the other direction as well: for every w in the W-type, ofNat(toNat(w)) = w.

Русский

Встраивание и проекция образуют обратную пару и в обратном направлении: для каждого элемента w из WType, ofNat(toNat(w)) = w.

LaTeX

$$$$\forall w:\, WType(\mathrm{Nat},\beta),\ \mathrm{WType.ofNat}(\mathrm{toNat}(w))=w.$$$$

Lean4

theorem rightInverse_nat : Function.RightInverse ofNat toNat
  | Nat.zero => rfl
  | Nat.succ n => by rw [ofNat, toNat, rightInverse_nat n]

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