ext_inf — Mathlib

English

Two SemilatticeInf structures on α that have the same comparison relation are equal; in particular, if the order is the same, then the meet operation is identical.

Русский

Две структуры SemilatticeInf на том же множестве с одинаковым отношением порядка равны; в частности, если порядок совпадает, то операция meet совпадает.

LaTeX

$$$ \forall A,B : SemilatticeInf(\alpha),\ (\forall x,y : \alpha,\ (A \le x y) \leftrightarrow (B \le x y)) \Rightarrow A = B $$$

Lean4

theorem ext_inf {α} {A B : SemilatticeInf α}
    (H :
      ∀ x y : α,
        (haveI := A;
          x ≤ y) ↔
          x ≤ y)
    (x y : α) :
    (haveI := A;
      x ⊓ y) =
      x ⊓ y :=
  eq_of_forall_le_iff fun c => by simp only [le_inf_iff]; rw [← H, @le_inf_iff α A, H, H]

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