---

Step * of Lemma face-lattice-basis

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:Point(face-lattice(T;eq))].
  (x = \/(λs./\(λu.{{u}}"(s))"(x)) ∈ Point(face-lattice(T;eq)))
BY
{ (Intros
   THEN (InstLemma `free-dlwc-basis` [⌜T + T⌝;⌜union-deq(T;T;eq;eq)⌝;⌜λ2x.face-lattice-constraints(x)⌝;⌜x⌝]⋅ THENA Auto)
   THEN Fold `face-lattice` (-1)
   THEN NthHypEq (-1)
   THEN EqCD
   THEN Auto
   THEN Thin (-1)
   THEN (RWO  "fl-point-sq" (-1) THENA Auto)
   THEN D -1
   THEN RepeatFor 6 ((EqCD THEN RWW "fl-point-sq" 0 THEN Auto))
   THEN RepUR ``free-dlwc-inc`` 0
   THEN AutoSplit) }

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. s : fset(T + T)
7. u : T + T
8. ↑fset-null({c ∈ face-lattice-constraints(u) | deq-f-subset(union-deq(T;T;eq;eq)) c {u}})
⊢ {{u}}
= {{u}}
∈ {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)))} 

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. fset-all(x;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))
6. s : fset(T + T)
7. u : T + T
8. ¬↑fset-null({c ∈ face-lattice-constraints(u) | deq-f-subset(union-deq(T;T;eq;eq)) c {u}})
⊢ {{u}}
= {}
∈ {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)))} 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:Point(face-lattice(T;eq))].    (x  =  \mbackslash{}/(\mlambda{}s./\mbackslash{}(\mlambda{}u.\{\{u\}\}"(s))"(x)))


By

---

Latex:
(Intros
  THEN  (InstLemma  `free-dlwc-basis`  [\mkleeneopen{}T  +  T\mkleeneclose{};\mkleeneopen{}union-deq(T;T;eq;eq)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.face-lattice-constraints(x)\mkleeneclose{}
              ;\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Fold  `face-lattice`  (-1)
  THEN  NthHypEq  (-1)
  THEN  EqCD
  THEN  Auto
  THEN  Thin  (-1)
  THEN  (RWO    "fl-point-sq"  (-1)  THENA  Auto)
  THEN  D  -1
  THEN  RepeatFor  6  ((EqCD  THEN  RWW  "fl-point-sq"  0  THEN  Auto))
  THEN  RepUR  ``free-dlwc-inc``  0
  THEN  AutoSplit)

---

Home Index