succ_unbot

Mathlib.Order.SuccPred.Basic

URI: https://scilib.ai/kg/mathlib#WithBot.succ_unbot

← MathLib Explorer

English

For any a, if a ≠ ⊥, then succ(a.unbot) = (succ(a)).unbot.

Русский

Для любого a, при a ≠ ⊥, succ(a.unbot) = (succ a).unbot.

LaTeX

$$$$ \operatorname{succ}(a.\mathrm{unbot}(ha)) = (\\operatorname{succ}(a)).\\unbot(\\text{proof}) $$$$

Lean4

@[simp]
theorem succ_unbot : ∀ (a : WithBot α) (ha : a ≠ ⊥), succ (a.unbot ha) = (succ a).unbot (by induction a <;> simp)
  | ⊥, ha => (ha rfl).elim
  | (a : α), _ => rfl

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

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

Разделы

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

Аффилиация

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