---

Step * of Lemma fl-point-sq

∀[T,eq:Top].
  (Point(face-lattice(T;eq)) ~ {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)))} )
BY
{ (Auto THEN Unfold `face-lattice` 0 THEN RWO "free-dlwc-point" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,eq:Top].
    (Point(face-lattice(T;eq)) 
    \msim{}  \{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)))\}  )


By

---

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

---

Home Index