English
There is a lattice structure on E with meet defined by the infimum operation and join by the supremum, compatible with the coordinate structure.
Русский
На E существует структура латтис, где операция meet задаёт наименьшее, а join — наибольшее, совместимо с координатной структурой.
LaTeX
$$$E$ is a lattice with inf and sup defined by the coordinate rules.$$
Lean4
instance : Lattice { a : R // IsIdempotentElem a }
where
__ : SemilatticeInf _ := inferInstance
sup a b := ⟨_, a.2.add_sub_mul b.2⟩
le_sup_left a b := show _ = _ by simp_rw [mul_sub, mul_add]; rw [← mul_assoc, a.2, add_sub_cancel_right]
le_sup_right a
b := show _ = _ by simp_rw [mul_sub, mul_add]; rw [← mul_assoc, mul_right_comm, b.2, add_sub_cancel_left]
sup_le a b c hac hbc := show _ = _ by simp_rw [sub_mul, add_mul, mul_assoc]; rw [hbc, hac]
