English
The extensional principle for SemilatticeInf: two structures are equal if they have the same order relation, and their infimum operation agrees pointwise.
Русский
Расширение для SemilatticeInf: две структуры равны, если совпадает отношение порядка и операция наименьшего действует одинаково на всех аргументах.
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 {α} {A B : SemilatticeInf α}
(H :
∀ x y : α,
(haveI := A;
x ≤ y) ↔
x ≤ y) :
A = B := by
cases A
cases B
cases PartialOrder.ext H
congr
ext; apply SemilatticeInf.ext_inf H
