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