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]