ppred_eq_pred

Mathlib.Data.Nat.PSub

URI: https://scilib.ai/kg/mathlib#Nat.ppred_eq_pred

English

For n > 0, ppred n = some (pred n).

Русский

Для n > 0, ppred n = some (pred n).

LaTeX

$$$$ \forall {n} (h: 0

Lean4

theorem ppred_eq_pred {n} (h : 0 < n) : ppred n = some (pred n) :=
  ppred_eq_some.2 <| succ_pred_eq_of_pos h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru