English
If a₁ is the greatest lower bound of s and a₂ is the greatest lower bound of t in a SemilatticeInf, then a₁ ⊓ a₂ is the greatest lower bound of s ∪ t.
Русский
Если a₁ — наибольшая нижняя граница множества s, а a₂ — наибольшая нижняя граница множества t в полулепладе SemilatticeInf, тогда a₁ ⊓ a₂ — наибольшая нижняя граница объединения s ∪ t.
LaTeX
$$$[SemilatticeInf γ] \; {a₁ a₂ : γ} {s t : Set γ} (hs : IsGLB s a₁) (ht : IsGLB t a₂) : IsGLB (s \cup t) (a₁ \inf a₂)$$$
Lean4
/-- If `a` is the greatest lower bound of `s` and `b` is the greatest lower bound of `t`,
then `a ⊓ b` is the greatest lower bound of `s ∪ t`. -/
theorem union [SemilatticeInf γ] {a₁ a₂ : γ} {s t : Set γ} (hs : IsGLB s a₁) (ht : IsGLB t a₂) :
IsGLB (s ∪ t) (a₁ ⊓ a₂) :=
hs.dual.union ht
