ppred_to_nat — Mathlib

English

The natural map of ppred through the Num functor coincides with Nat.ppred on Nat.

Русский

Преобразование ppred через функтор Num совпадает с Nat.ppred на Nat.

LaTeX

$$$\\forall n : \\text{Num}, \\operatorname{cast}\\ast(n.{\\text{ppred}}) = \\operatorname{Nat.ppred}(n)$$$

Lean4

theorem ppred_to_nat : ∀ n : Num, (↑) <$> ppred n = Nat.ppred n
  | 0 => rfl
  | pos p => by
    rw [ppred, Option.map_eq_map, Option.map_some, Nat.ppred_eq_some.2]
    rw [PosNum.pred'_to_nat, Nat.succ_pred_eq_of_pos (PosNum.to_nat_pos _)]
    rfl

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