English
The set E carries a lattice structure with join defined by an explicit formula in the coordinates, turning E into a lattice-ordered set under the induced order.
Русский
Множество E обладает структурой решетки: операция наивысшей верхней границы задаётся явной формулой по координатам, образуя упорядоченное полишность множество.
LaTeX
$$$E = \{(a,b) \mid ab=0, a+b=1\},\quad a \vee b = \text{explicit formula in coordinates}$$$
Lean4
instance : SemilatticeSup { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
where
sup a
b :=
⟨(a.1.1 + a.1.2 * b.1.1, a.1.2 * b.1.2), by
simp_rw [add_mul, mul_mul_mul_comm _ b.1.1, b.2.1, mul_zero, ← mul_assoc, a.2.1, zero_mul, add_zero], by
simp_rw [add_assoc, ← mul_add, b.2.2, mul_one, a.2.2]⟩
le_sup_left a
b := by
simp_rw [(· ≤ ·), mul_add, ← mul_assoc, a.2.1, zero_mul, add_zero, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1.eq]
le_sup_right a
b := by
simp_rw [(· ≤ ·), mul_add, mul_comm a.1.2, ← mul_assoc, (IsIdempotentElem.of_mul_add b.2.1 b.2.2).1.eq, ← mul_add,
a.2.2, mul_one]
sup_le a b c hac hbc := by simp_rw [(· ≤ ·), add_mul, mul_assoc]; rw [hac, hbc]
