dcreager.net

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₂) ≤

» Theory » Constraints on sets