---

Step * of Lemma face-lattice-le

∀T:Type. ∀eq:EqDecider(T). ∀x,y:Point(face-lattice(T;eq)).
  (x ≤ y ⇐⇒ ∀s:fset(T + T). (s ∈ x ⇒ (↓∃t:fset(T + T). (t ∈ y ∧ t ⊆ s))))
BY
{ (InstLemma `face-lattice-le-1` []
   THEN RepeatFor 4 (ParallelLast')
   THEN RWO "-1" 0
   THEN Try ((MemCD' THEN Try (Declaration) THEN MemCD THEN Declaration))
   THEN All (RWO "fl-point-sq")
   THEN Auto
   THEN Try (((FLemma `fset-ac-le-implies2` [-3] THENA Auto) THEN InstHyp [⌜s⌝] (-1)⋅ THEN Auto))) }

1
1. T : Type
2. eq : EqDecider(T)
3. 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)))} 
4. 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)))} 
5. x ≤ y ⇒ fset-ac-le(union-deq(T;T;eq;eq);x;y)
6. x ≤ y ⇐ fset-ac-le(union-deq(T;T;eq;eq);x;y)
7. ∀s:fset(T + T). (s ∈ x ⇒ (↓∃t:fset(T + T). (t ∈ y ∧ t ⊆ s)))
⊢ fset-ac-le(union-deq(T;T;eq;eq);x;y)

---

Latex:

---

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


By

---

Latex:
(InstLemma  `face-lattice-le-1`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  RWO  "-1"  0
  THEN  Try  ((MemCD'  THEN  Try  (Declaration)  THEN  MemCD  THEN  Declaration))
  THEN  All  (RWO  "fl-point-sq")
  THEN  Auto
  THEN  Try  (((FLemma  `fset-ac-le-implies2`  [-3]  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}s\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)))

---

Home Index