id_le

Mathlib.SetTheory.Ordinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Ordinal.IsNormal.id_le

English

For a normal f, id ≤ f holds, i.e., a ≤ f(a) for every a.

Русский

Для нормальной f верно id ≤ f, то есть ∀a: a ≤ f(a).

LaTeX

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

Lean4

theorem id_le {f} (H : IsNormal f) : id ≤ f :=
  H.strictMono.id_le

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

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

Разделы

Аффилиация

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