add_sub_cancel_of_le

Mathlib.SetTheory.Ordinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Ordinal.add_sub_cancel_of_le

← MathLib Explorer

English

For a normal f, a ≤ f(a) for all a.

Русский

Для нормальной f: для всех a выполняется a ≤ f(a).

LaTeX

$$$\forall a,\; a \le f(a).$$$

Lean4

protected theorem add_sub_cancel_of_le {a b : Ordinal} (h : b ≤ a) : b + (a - b) = a :=
  by
  change b + dite _ _ _ = a
  rw [dif_pos h]
  exact (Classical.choose_spec (exists_add_of_le h)).symm

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

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

Разделы

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

Аффилиация

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