ext — Mathlib

English

If two lattice structures on the same carrier have the same order relation, then the two structures are equal.

Русский

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

LaTeX

$$$\big(\forall x,y : \alpha, x \le_A y \iff x \le_B y\big) \Rightarrow A = B$$$

Lean4

theorem ext {α} {A B : Lattice α}
    (H :
      ∀ x y : α,
        (haveI := A;
          x ≤ y) ↔
          x ≤ y) :
    A = B := by
  cases A
  cases B
  cases SemilatticeSup.ext H
  cases SemilatticeInf.ext H
  congr

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