veblen_eq_self_of_le

Mathlib.SetTheory.Ordinal.Veblen

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

English

If o1 ≤ o2 and veblen o2 a = a, then veblen o1 a = a.

Русский

Если o1 ≤ o2 и veblen o2 a = a, то veblen o1 a = a.

LaTeX

$$$\forall o1,o2,a:\operatorname{Ordinal},\ o1 \le o2 \Rightarrow ( \operatorname{veblen}(o2,a) = a \Rightarrow \operatorname{veblen}(o1,a) = a)$$$

Lean4

theorem veblen_eq_self_of_le (h : o₁ ≤ o₂) (h' : veblen o₂ a = a) : veblen o₁ a = a :=
  veblenWith_eq_self_of_le (isNormal_opow one_lt_omega0) h h'

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

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

Разделы

Аффилиация

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