---

Step * of Lemma fl-point

∀[T:Type]. ∀[eq:EqDecider(T)].
  Point(face-lattice(T;eq)) ≡ {ac:fset(fset(T + T))| 
                               (↑fset-antichain(union-deq(T;T;eq;eq);ac))
                               ∧ (∀a:fset(T + T). (a ∈ ac ⇒ (∀z:T. (¬(inl z ∈ a ∧ inr z  ∈ a)))))} 
BY
{ (Auto
   THEN Unfold `face-lattice` 0
   THEN (RWO "free-dlwc-point" 0 THENA Auto)
   THEN (RepeatFor 2 (D 0) THENA Auto)
   THEN D -1
   THEN MemTypeCD
   THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. x : fset(fset(T + T))
4. ↑fset-antichain(union-deq(T;T;eq;eq);x)
5. fset-all(x;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))
6. ↑fset-antichain(union-deq(T;T;eq;eq);x)
7. a : fset(T + T)
8. a ∈ x
9. z : T
⊢ ¬(inl z ∈ a ∧ inr z  ∈ a)

2
1. T : Type
2. eq : EqDecider(T)
3. x : fset(fset(T + T))
4. ↑fset-antichain(union-deq(T;T;eq;eq);x)
5. ∀a:fset(T + T). (a ∈ x ⇒ (∀z:T. (¬(inl z ∈ a ∧ inr z  ∈ a))))
6. ↑fset-antichain(union-deq(T;T;eq;eq);x)
⊢ fset-all(x;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].
    Point(face-lattice(T;eq))  \mequiv{}  \{ac:fset(fset(T  +  T))| 
                                                              (\muparrow{}fset-antichain(union-deq(T;T;eq;eq);ac))
                                                              \mwedge{}  (\mforall{}a:fset(T  +  T).  (a  \mmember{}  ac  {}\mRightarrow{}  (\mforall{}z:T.  (\mneg{}(inl  z  \mmember{}  a  \mwedge{}  inr  z    \mmember{}  a)))))\} 


By

---

Latex:
(Auto
  THEN  Unfold  `face-lattice`  0
  THEN  (RWO  "free-dlwc-point"  0  THENA  Auto)
  THEN  (RepeatFor  2  (D  0)  THENA  Auto)
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index