le_apply

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem le_apply {f} (H : IsNormal f) {a} : a ≤ f a :=
  H.strictMono.le_apply

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

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

Разделы

Аффилиация

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