---

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


1. T : Type@i'
2. eq : EqDecider(T)@i
3. Point(face-lattice(T;eq)) ⊆r fset(fset(T + T))
4. x : Point(face-lattice(T;eq))@i
5. y : Point(face-lattice(T;eq))@i
6. z : Point(face-lattice(T;eq))@i
7. ∀s:fset(T + T). (s ∈ z ⇒ ((↑ac-covers(union-deq(T;T;eq;eq);x;s)) ∨ (↑ac-covers(union-deq(T;T;eq;eq);y;s))))
8. s : fset(T + T)@i
9. s ∈ z
10. (↑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);x ∨ y;s)
BY
{ (Unfold `face-lattice` 0 THEN (RWO  "free-dlwc-join" 0 THENA Auto)) }

1
1. T : Type@i'
2. eq : EqDecider(T)@i
3. Point(face-lattice(T;eq)) ⊆r fset(fset(T + T))
4. x : Point(face-lattice(T;eq))@i
5. y : Point(face-lattice(T;eq))@i
6. z : Point(face-lattice(T;eq))@i
7. ∀s:fset(T + T). (s ∈ z ⇒ ((↑ac-covers(union-deq(T;T;eq;eq);x;s)) ∨ (↑ac-covers(union-deq(T;T;eq;eq);y;s))))
8. s : fset(T + T)@i
9. s ∈ z
10. (↑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);lub(λs.fset-contains-none(union-deq(T;T;eq;
                                                                      eq);s;x.face-lattice-constraints(x));x;y);s)

---

Latex:

---

Latex:

1.  T  :  Type@i'
2.  eq  :  EqDecider(T)@i
3.  Point(face-lattice(T;eq))  \msubseteq{}r  fset(fset(T  +  T))
4.  x  :  Point(face-lattice(T;eq))@i
5.  y  :  Point(face-lattice(T;eq))@i
6.  z  :  Point(face-lattice(T;eq))@i
7.  \mforall{}s:fset(T  +  T)
          (s  \mmember{}  z  {}\mRightarrow{}  ((\muparrow{}ac-covers(union-deq(T;T;eq;eq);x;s))  \mvee{}  (\muparrow{}ac-covers(union-deq(T;T;eq;eq);y;s))))
8.  s  :  fset(T  +  T)@i
9.  s  \mmember{}  z
10.  (\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);x  \mvee{}  y;s)


By

---

Latex:
(Unfold  `face-lattice`  0  THEN  (RWO    "free-dlwc-join"  0  THENA  Auto))

---

Home Index