¶Intersection of s₁ ≤ and s₂ ≤
The intersection of two lower bounds is a lower bound of the join (or union) of the two types.
(s₁ ≤) ∧ (s₂ ≤) = (s₁ ∪ s₂) ≤
¶Equationally
⟦s₁ ≤⟧ = {x | s₁ ⊆ x}
⟦s₂ ≤⟧ = {x | s₂ ⊆ x}
⟦(s₁ ≤) ∧ (s₂ ≤)⟧
= {x | s₁ ⊆ x} ∩ {x | s₂ ⊆ x}
= {x | s₁ ⊆ x ∧ s₂ ⊆ x}
= {x | (s₁ ∪ s₂) ⊆ x}
= ⟦(s₁ ∪ s₂) ≤⟧
¶Graphically
If s₁ = {0} and s₂ = {2}, then the initial constraints are
s₁ ≤
┏━━━━━━━━━┓
🮣──╼┫ {0,1,2} ┣╾──🮢
🮣🮠 ┗━━━━┳━━━━┛ 🮡🮢
┏━━━┷━━━┓ ┏━━━┷━━━┓ ╵
┃ {0,1} ┃ ┃ {0,2} ┃ 🮣╸{1,2}
┗━━━┳━━━┫ ┣━━━━━━━┫🮣🮠 ╻
┏━━┷━━┓🮡🮦🮠 🮥🮤 ╵
┃ {0} ┠─🮧──╴{1}╶─🮠🮡──╴{2}
┗━━┳━━┛ ╻ ╻
🮡🮢 ╵ 🮣🮠
🮡──────╴{ }╶──────🮠
and
s₂ ≤
┏━━━━━━━━━┓
🮣──╼┫ {0,1,2} ┣╾──🮢
🮣🮠 ┗━━━━┳━━━━┛ 🮡🮢
╵ ┏━━━┷━━━┓ ┏━━━┷━━━┓
{0,1}╺🮢 ┃ {0,2} ┃ ┃ {1,2} ┃
╻ 🮡🮢┣━━━━━━━┫ ┣━━━┳━━━┛
╵ 🮥🮤 🮡🮦🮠┏━━┷━━┓
{0}╶──🮠🮡─╴{1}╶──🮧─┨ {2} ┃
╻ ╻ ┗━━┳━━┛
🮡🮢 ╵ 🮣🮠
🮡──────╴{ }╶──────🮠
The intersection should be
(s₁ ≤) ∧ (s₂ ≤)
┏━━━━━━━━━┓
🮣──╼┫ {0,1,2} ┣╾──🮢
🮣🮠 ┗━━━━┳━━━━┛ 🮡🮢
╵ ┏━━━┷━━━┓ ╵
{0,1}╺🮢 ┃ {0,2} ┃ 🮣╸{1,2}
╻ 🮡🮢┣━━━━━━━┫🮣🮠 ╻
╵ 🮥🮤 🮥🮤 ╵
{0}╶──🮠🮡─╴{1}╶─🮠🮡──╴{2}
╻ ╻ ╻
🮡🮢 ╵ 🮣🮠
🮡──────╴{ }╶──────🮠
Since the join (union) of s₁ and s₂ is {0,2}, we can write this as
(s₁ ≤) ∧ (s₂ ≤) = (s₁ ∪ s₂) ≤