enum_le_enum' — Mathlib

English

For any a, the order relation between enum r and enum s is equivalent to le between o1,o2 in the corresponding substructure.

Русский

Для произвольного a отношение порядка между enum_r и enum_s эквивалентно отношению ≤ между o1, o2 в соответствующей подструктуре.

LaTeX

$$$\\mathrm{enum}_r(o_1) \\le \\mathrm{enum}_r(o_2) \\iff o_1 \\le o_2$$$

Lean4

@[simp]
theorem enum_le_enum' (a : Ordinal) {o₁ o₂ : Iio (type (· < ·))} :
    enum (· < ·) o₁ ≤ enum (α := a.toType) (· < ·) o₂ ↔ o₁ ≤ o₂ := by rw [← enum_le_enum, not_lt]

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