psub_eq_some

Mathlib.Data.Nat.PSub

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

← MathLib Explorer

English

For all m,n,k, psub m n = some k iff k+n = m.

Русский

Для всех m,n,k: psub m n = some k ⇔ k+n = m.

LaTeX

$$$$ \forall {m n k}: \mathrm{Nat}, \ psub(m,n) = \mathrm{some} k \iff k+n = m. $$$$

Lean4

theorem psub_eq_some {m : ℕ} : ∀ {n k}, psub m n = some k ↔ k + n = m
  | 0, k => by simp [eq_comm]
  | n + 1, k => by
    apply Option.bind_eq_some_iff.trans
    simp only [psub_eq_some, ppred_eq_some]
    simp [add_comm, add_left_comm]

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

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

Разделы

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

Аффилиация

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