veblenWith_lt_veblenWith_iff_right

Mathlib.SetTheory.Ordinal.Veblen

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

English

For normal f, veblenWith f o a < veblenWith f o b if and only if a < b.

Русский

Для нормальной f верна эквивалентность: veblenWith f o a < veblenWith f o b ⇔ a < b.

LaTeX

$$theorem veblenWith_lt_veblenWith_iff_right : veblenWith f o a < veblenWith f o b ↔ a < b$$

Lean4

@[simp]
theorem veblenWith_lt_veblenWith_iff_right : veblenWith f o a < veblenWith f o b ↔ a < b :=
  (veblenWith_right_strictMono hf o).lt_iff_lt

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

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

Разделы

Аффилиация

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