---

Step * 2 of Lemma fl-point


1. T : Type
2. eq : EqDecider(T)
3. x : fset(fset(T + T))
4. ↑fset-antichain(union-deq(T;T;eq;eq);x)
5. ∀a:fset(T + T). (a ∈ x ⇒ (∀z:T. (¬(inl z ∈ a ∧ inr z  ∈ a))))
6. ↑fset-antichain(union-deq(T;T;eq;eq);x)
⊢ fset-all(x;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))
BY
{ (Using [`eq', ⌜deq-fset(union-deq(T;T;eq;eq))⌝] (BLemma `fset-all-iff`)⋅
   THEN Auto
   THEN RWO "assert-fset-contains-none" 0
   THEN Auto) }

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. ∀a:fset(T + T). (a ∈ x ⇒ (∀z:T. (¬(inl z ∈ a ∧ inr z  ∈ a))))
6. ↑fset-antichain(union-deq(T;T;eq;eq);x)
7. a : fset(T + T)
8. a ∈ x
9. x1 : T + T
10. x1 ∈ a
11. c : fset(T + T)
12. c ∈ face-lattice-constraints(x1)
⊢ ¬c ⊆ a

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  fset(fset(T  +  T))
4.  \muparrow{}fset-antichain(union-deq(T;T;eq;eq);x)
5.  \mforall{}a:fset(T  +  T).  (a  \mmember{}  x  {}\mRightarrow{}  (\mforall{}z:T.  (\mneg{}(inl  z  \mmember{}  a  \mwedge{}  inr  z    \mmember{}  a))))
6.  \muparrow{}fset-antichain(union-deq(T;T;eq;eq);x)
\mvdash{}  fset-all(x;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))


By

---

Latex:
(Using  [`eq',  \mkleeneopen{}deq-fset(union-deq(T;T;eq;eq))\mkleeneclose{}]  (BLemma  `fset-all-iff`)\mcdot{}
  THEN  Auto
  THEN  RWO  "assert-fset-contains-none"  0
  THEN  Auto)

---

Home Index