toLE_injective — Mathlib

English

Two Preorder structures on the same set are equal if their ≤ relations are the same.

Русский

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

LaTeX

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

Lean4

@[ext]
theorem toLE_injective : Function.Injective (@Preorder.toLE α) := fun
  | { lt := A_lt, lt_iff_le_not_ge := A_iff, .. }, { lt := B_lt, lt_iff_le_not_ge := B_iff, .. } =>
    by
    rintro ⟨⟩
    have : A_lt = B_lt := by
      funext a b
      rw [A_iff, B_iff]
    cases this
    congr

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