ext — Mathlib

English

If two SemilatticeSup structures A and B on the same underlying set share exactly the same order (x ≤_A y iff x ≤_B y) then A = B.

Русский

Если две структуры SemilatticeSup на том же множестве имеют одинаковый порядок (x ≤_A y эквивалентно x ≤_B y для всех x,y), то A = B.

LaTeX

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

Lean4

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

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