veblen_zero_le_veblen_zero

Mathlib.SetTheory.Ordinal.Veblen

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

English

For all o1, o2, veblen(o1,0) ≤ veblen(o2,0) iff o1 ≤ o2.

Русский

Для всех o1, o2 верно veblen(o1,0) ≤ veblen(o2,0) тогда и только тогда, когда o1 ≤ o2.

LaTeX

$$$$\\operatorname{veblen}(o_1,0) \\le \\operatorname{veblen}(o_2,0) \\iff o_1 \\le o_2.$$$$

Lean4

@[simp]
theorem veblen_zero_le_veblen_zero : veblen o₁ 0 ≤ veblen o₂ 0 ↔ o₁ ≤ o₂ :=
  veblen_zero_strictMono.le_iff_le

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

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

Разделы

Аффилиация

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