---

Step * of Lemma fl-filter_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Q:{x:fset(T + T)| 
                                    ↑fset-contains-none(union-deq(T;T;eq;eq);x;x.face-lattice-constraints(x))}  ⟶ 𝔹].
∀[s:Point(face-lattice(T;eq))].
  (fl-filter(s;x.Q[x]) ∈ Point(face-lattice(T;eq)))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].
\mforall{}[Q:\{x:fset(T  +  T)|  \muparrow{}fset-contains-none(union-deq(T;T;eq;eq);x;x.face-lattice-constraints(x))\} 
        {}\mrightarrow{}  \mBbbB{}].  \mforall{}[s:Point(face-lattice(T;eq))].
    (fl-filter(s;x.Q[x])  \mmember{}  Point(face-lattice(T;eq)))


By

---

Latex:
ProveWfLemma

---

Home Index