---

Step * 2 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)))))} 
4. fl-deq(T;eq)
= 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)))))} )
⊢ 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)))))} ) ⊆r EqDecider(Point(face-lattice(T;eq\000C)))
BY
{ (FLemma `deq_functionality_wrt_ext-eq` [-2] THEN Auto) }

---

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)))))\} 
4.  fl-deq(T;eq)  =  fl-deq(T;eq)
\mvdash{}  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)))))\}  )
        \msubseteq{}r  EqDecider(Point(face-lattice(T;eq)))


By

---

Latex:
(FLemma  `deq\_functionality\_wrt\_ext-eq`  [-2]  THEN  Auto)

---

Home Index