ext_lt — Mathlib

English

Two PartialOrders are equal if their strict orders coincide.

Русский

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

LaTeX

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

Lean4

theorem ext_lt {A B : PartialOrder α}
    (H :
      ∀ x y : α,
        (haveI := A;
          x < y) ↔
          x < y) :
    A = B := by ext x y; rw [le_iff_lt_or_eq, @le_iff_lt_or_eq _ A, H]

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