ext — Mathlib

English

Two LinearOrders are equal whenever they share the same ≤ relation.

Русский

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

LaTeX

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

Lean4

theorem ext {A B : LinearOrder α}
    (H :
      ∀ x y : α,
        (haveI := A;
          x ≤ y) ↔
          x ≤ y) :
    A = B := by ext x y; exact H x y

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