---

Step * 1 1 1 1 of Lemma implies-le-face-lattice-join3


1. T : Type@i'
2. eq : EqDecider(T)@i
3. {ac:fset(fset(T + T))| 
    (↑fset-antichain(union-deq(T;T;eq;eq);ac))
    ∧ fset-all(ac;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))}  ⊆r fset(fset(T + T))
4. u : {ac:fset(fset(T + T))| 
        (↑fset-antichain(union-deq(T;T;eq;eq);ac))
        ∧ fset-all(ac;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))} @i
5. x : {ac:fset(fset(T + T))| 
        (↑fset-antichain(union-deq(T;T;eq;eq);ac))
        ∧ fset-all(ac;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))} @i
6. y : {ac:fset(fset(T + T))| 
        (↑fset-antichain(union-deq(T;T;eq;eq);ac))
        ∧ fset-all(ac;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))} @i
7. z : {ac:fset(fset(T + T))| 
        (↑fset-antichain(union-deq(T;T;eq;eq);ac))
        ∧ fset-all(ac;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))} @i
8. ∀s:fset(T + T)
     (s ∈ z
     ⇒ ((↑ac-covers(union-deq(T;T;eq;eq);u;s))
        ∨ (↑ac-covers(union-deq(T;T;eq;eq);x;s))
        ∨ (↑ac-covers(union-deq(T;T;eq;eq);y;s))))@i
9. s : fset(T + T)@i
10. s ∈ z@i
11. (↑ac-covers(union-deq(T;T;eq;eq);u;s))
∨ (↑ac-covers(union-deq(T;T;eq;eq);x;s))
∨ (↑ac-covers(union-deq(T;T;eq;eq);y;s))
⊢ (↑ac-covers(union-deq(T;T;eq;eq);u;s)) ∨ (↑ac-covers(union-deq(T;T;eq;eq);fset-ac-lub(union-deq(T;T;eq;eq);x;y);s))
BY
{ (ParallelLast THEN BLemma `fset-ac-lub-covers` THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type@i'
2.  eq  :  EqDecider(T)@i
3.  \{ac:fset(fset(T  +  T))| 
        (\muparrow{}fset-antichain(union-deq(T;T;eq;eq);ac))
        \mwedge{}  fset-all(ac;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))\} 
          \msubseteq{}r  fset(fset(T  +  T))
4.  u  :  \{ac:fset(fset(T  +  T))| 
                (\muparrow{}fset-antichain(union-deq(T;T;eq;eq);ac))
                \mwedge{}  fset-all(ac;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))\}  @\000Ci
5.  x  :  \{ac:fset(fset(T  +  T))| 
                (\muparrow{}fset-antichain(union-deq(T;T;eq;eq);ac))
                \mwedge{}  fset-all(ac;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))\}  @\000Ci
6.  y  :  \{ac:fset(fset(T  +  T))| 
                (\muparrow{}fset-antichain(union-deq(T;T;eq;eq);ac))
                \mwedge{}  fset-all(ac;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))\}  @\000Ci
7.  z  :  \{ac:fset(fset(T  +  T))| 
                (\muparrow{}fset-antichain(union-deq(T;T;eq;eq);ac))
                \mwedge{}  fset-all(ac;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))\}  @\000Ci
8.  \mforall{}s:fset(T  +  T)
          (s  \mmember{}  z
          {}\mRightarrow{}  ((\muparrow{}ac-covers(union-deq(T;T;eq;eq);u;s))
                \mvee{}  (\muparrow{}ac-covers(union-deq(T;T;eq;eq);x;s))
                \mvee{}  (\muparrow{}ac-covers(union-deq(T;T;eq;eq);y;s))))@i
9.  s  :  fset(T  +  T)@i
10.  s  \mmember{}  z@i
11.  (\muparrow{}ac-covers(union-deq(T;T;eq;eq);u;s))
\mvee{}  (\muparrow{}ac-covers(union-deq(T;T;eq;eq);x;s))
\mvee{}  (\muparrow{}ac-covers(union-deq(T;T;eq;eq);y;s))
\mvdash{}  (\muparrow{}ac-covers(union-deq(T;T;eq;eq);u;s))
\mvee{}  (\muparrow{}ac-covers(union-deq(T;T;eq;eq);fset-ac-lub(union-deq(T;T;eq;eq);x;y);s))


By

---

Latex:
(ParallelLast  THEN  BLemma  `fset-ac-lub-covers`  THEN  Auto)

---

Home Index