fst_ofNat — Mathlib

English

If n is a Nat and AtLeastTwo, then the first projection of the OfNat embedding of n into α × β is the natural embedding into α.

Русский

Пусть n — натуральное число с условием AtLeastTwo; первая проекция элемента OfNat(n) в α × β равна OfNat(n) в α.

LaTeX

$$$ (\mathrm{ofNat}(n) : \alpha \times \beta).1 = (\mathrm{ofNat}(n) : \alpha) $$$

Lean4

@[simp]
theorem fst_ofNat (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : α × β).1 = (ofNat(n) : α) :=
  rfl

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