enum_le_enum — Mathlib

English

The negation of r(enum r o1, enum r o2) is equivalent to o2 ≤ o1.

Русский

Отрицание равенства или порядка между образами эквивалентно неравенству между o1 и o2: o2 ≤ o1.

LaTeX

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

Lean4

theorem enum_le_enum (r : α → α → Prop) [IsWellOrder α r] {o₁ o₂ : Iio (type r)} :
    ¬r (enum r o₁) (enum r o₂) ↔ o₂ ≤ o₁ := by
  rw [enum_lt_enum (r := r), not_lt]
    -- TODO: generalize to other well-orders

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