ext — Mathlib

English

If two PartialOrder structures on α have the same ≤ relation, then they are equal.

Русский

Если два частичных порядка на α имеют одинаковое отношение ≤, то они равны.

LaTeX

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

Lean4

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

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