English
Let α be a complete lattice and x,y ∈ α. Then the join x ∨ y equals the supremum over the two possibilities obtained by a boolean selector: x ∨ y = sup { cond(true, x, y), cond(false, x, y) }. Equivalently, x ∨ y is the least upper bound of {x, y}.
Русский
Пусть α — полная решетка и x, y ∈ α. Тогда их объединение x ∨ y равно верхней грани над двумя вариантами, получаемыми булевой функцией: x ∨ y = sup{cond(true, x, y), cond(false, x, y)}. Эквивалентно: x ∨ y — наименьшая верхняя граница множества {x, y}.
LaTeX
$$$x \lor y = \sup\{x,y\}$$$
Lean4
theorem sup_eq_iSup (x y : α) : x ⊔ y = ⨆ b : Bool, cond b x y := by rw [iSup_bool_eq, Bool.cond_true, Bool.cond_false]
