pred_to_nat — Mathlib

English

For all n : Num, (pred n : ℕ) = Nat.pred n, with base case and a positive-case reduction.

Русский

Для всех n : Num, (pred n : ℕ) = Nat.pred n, базовый случай и переход к положительному случаю.

LaTeX

$$$\\forall n : \\text{Num}, (\\operatorname{pred} n : \\mathbb{N}) = \\operatorname{Nat.pred} n$$$

Lean4

theorem pred_to_nat : ∀ n : Num, (pred n : ℕ) = Nat.pred n
  | 0 => rfl
  | pos p => by rw [pred, PosNum.pred'_to_nat]; rfl

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