ext — Mathlib

English

If two Preorder structures have the same ≤ relation, they are equal.

Русский

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

LaTeX

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

Lean4

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

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