English
If two SemilatticeSup structures on the same set have identical order relations, then their suprema agree for all pairs of elements.
Русский
Если две структуры SemilatticeSup на одном и том же множестве имеют идентичные отношения порядка, то их объединения верхних границ совпадают для всех пар элементов.
LaTeX
$$$ \forall A,B:\SemilatticeSup(\alpha),\; \big(\forall x,y:\alpha,\ A.le\,x\,y \iff B.le\,x\,y\big) \Rightarrow \forall x,y:\alpha,\ x \sqcup_A y = x \sqcup_B y$$$
Lean4
theorem ext_sup {α} {A B : SemilatticeSup α}
(H :
∀ x y : α,
(haveI := A;
x ≤ y) ↔
x ≤ y)
(x y : α) :
(haveI := A;
x ⊔ y) =
x ⊔ y :=
eq_of_forall_ge_iff fun c => by simp only [sup_le_iff]; rw [← H, @sup_le_iff α A, H, H]
