Step
*
of Lemma
fl-point-sq
No Annotations
∀[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:
No Annotations
\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