---

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

∀T:Type. ∀eq:EqDecider(T). ∀u,x,y,z:Point(face-lattice(T;eq)).
  ((∀s:fset(T + T)
      (s ∈ z
      ⇒ ((↓∃t:fset(T + T). (t ∈ u ∧ t ⊆ s))
         ∨ (↓∃t:fset(T + T). (t ∈ x ∧ t ⊆ s))
         ∨ (↓∃t:fset(T + T). (t ∈ y ∧ t ⊆ s)))))
  ⇒ z ≤ u ∨ x ∨ y)
BY
{ (RepeatFor 2 (Intro)
   THEN (Assert Point(face-lattice(T;eq)) ⊆r fset(fset(T + T)) BY
               (RWO "fl-point-sq" 0 THEN Auto))
   THEN Auto
   THEN BLemma `face-lattice-le` 
   THEN Auto
   THEN (RWO "assert-ac-covers<" 0 THENA Auto)
   THEN (RWO "assert-ac-covers<" (-3) THENA Auto)) }

1
1. T : Type@i'
2. eq : EqDecider(T)@i
3. Point(face-lattice(T;eq)) ⊆r fset(fset(T + T))
4. u : Point(face-lattice(T;eq))@i
5. x : Point(face-lattice(T;eq))@i
6. y : Point(face-lattice(T;eq))@i
7. z : Point(face-lattice(T;eq))@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
⊢ ↑ac-covers(union-deq(T;T;eq;eq);u ∨ x ∨ y;s)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).  \mforall{}u,x,y,z:Point(face-lattice(T;eq)).
    ((\mforall{}s:fset(T  +  T)
            (s  \mmember{}  z
            {}\mRightarrow{}  ((\mdownarrow{}\mexists{}t:fset(T  +  T).  (t  \mmember{}  u  \mwedge{}  t  \msubseteq{}  s))
                  \mvee{}  (\mdownarrow{}\mexists{}t:fset(T  +  T).  (t  \mmember{}  x  \mwedge{}  t  \msubseteq{}  s))
                  \mvee{}  (\mdownarrow{}\mexists{}t:fset(T  +  T).  (t  \mmember{}  y  \mwedge{}  t  \msubseteq{}  s)))))
    {}\mRightarrow{}  z  \mleq{}  u  \mvee{}  x  \mvee{}  y)


By

---

Latex:
(RepeatFor  2  (Intro)
  THEN  (Assert  Point(face-lattice(T;eq))  \msubseteq{}r  fset(fset(T  +  T))  BY
                          (RWO  "fl-point-sq"  0  THEN  Auto))
  THEN  Auto
  THEN  BLemma  `face-lattice-le` 
  THEN  Auto
  THEN  (RWO  "assert-ac-covers<"  0  THENA  Auto)
  THEN  (RWO  "assert-ac-covers<"  (-3)  THENA  Auto))

---

Home Index