ppred_eq_some

Mathlib.Data.Nat.PSub

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

← MathLib Explorer

English

ppred n = some m iff succ m = n.

Русский

ppred n = some m ⇔ succ m = n.

LaTeX

$$$$ \forall {n},\ ppred(n)=\mathrm{some} m \iff \operatorname{succ} m = n. $$$$

Lean4

@[simp]
theorem ppred_eq_some {m : ℕ} : ∀ {n}, ppred n = some m ↔ succ m = n
  | 0 => by constructor <;> intro h <;> contradiction
  | n + 1 => by constructor <;> intro h <;> injection h <;> subst m <;> rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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