English
If a is the least upper bound of s and b is the least upper bound of t in a SemilatticeSup, then a ⊔ b is the least upper bound of s ∪ t.
Русский
Если a является наименьшей верхней границей множества s, а b — наименьшей верхней границе множества t в полудисплинкованной полулине semilattice, то a ⊔ b является наименьшей верхней границей объединения s ∪ t.
LaTeX
$$$[SemilatticeSup \ γ] \; {a b : γ} {s t : Set γ} \; (hs : IsLUB s a) (ht : IsLUB t b) : IsLUB (s \cup t) (a \sqcup b)$$$
Lean4
/-- If `a` is the least upper bound of `s` and `b` is the least upper bound of `t`,
then `a ⊔ b` is the least upper bound of `s ∪ t`. -/
theorem union [SemilatticeSup γ] {a b : γ} {s t : Set γ} (hs : IsLUB s a) (ht : IsLUB t b) : IsLUB (s ∪ t) (a ⊔ b) :=
⟨fun _ h => h.casesOn (fun h => le_sup_of_le_left <| hs.left h) fun h => le_sup_of_le_right <| ht.left h, fun _ hc =>
sup_le (hs.right fun _ hd => hc <| Or.inl hd) (ht.right fun _ hd => hc <| Or.inr hd)⟩
