enum_lt_enum

Mathlib.SetTheory.Ordinal.Basic

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

English

For o1,o2 in Iio(type r), r(enum r o1) (enum r o2) iff o1 < o2.

Русский

Для o1, o2 ∈ Iio(type r) верно: r(enum r o1) (enum r o2) тогда как o1 < o2.

LaTeX

$$$r\\big(\\mathrm{enum}_r(o_1), \\mathrm{enum}_r(o_2)\\big) \\iff o_1 < o_2$$$

Lean4

theorem enum_lt_enum {r : α → α → Prop} [IsWellOrder α r] {o₁ o₂ : Iio (type r)} :
    r (enum r o₁) (enum r o₂) ↔ o₁ < o₂ :=
  (enum _).map_rel_iff

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

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

Разделы

Аффилиация

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