---

Step * 1 of Lemma fl-deq_wf


1. T : Type
2. eq : EqDecider(T)
3. 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)))))} 
⊢ fl-deq(T;eq) ∈ EqDecider({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
{ ProveWfLemma }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  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)))))\} 
\mvdash{}  fl-deq(T;eq)  \mmember{}  EqDecider(\{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:
ProveWfLemma

---

Home Index