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]