ext_lt — Mathlib

English

Two LinearOrders are equal if their strict orders coincide.

Русский

Два линейных порядка равны, если их строгие отношения совпадают.

LaTeX

$$$ \forall {A B : LinearOrder α},\ (\forall x y, A.lt x y \leftrightarrow B.lt x y) \rightarrow A = B $$$

Lean4

theorem ext_lt {A B : LinearOrder α}
    (H :
      ∀ x y : α,
        (haveI := A;
          x < y) ↔
          x < y) :
    A = B :=
  LinearOrder.toPartialOrder_injective (PartialOrder.ext_lt H)

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