---

Step * of Lemma fset-ac-le-face-lattice1

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[i:T]. ∀[s:fset(fset(T + T))].
  (fset-all(s;x.inr i  ∈b x) ⇐⇒ fset-ac-le(union-deq(T;T;eq;eq);s;(i=1)))
BY
{ (Intros
   THEN (Assert ⌜Point(face-lattice(T;eq)) ⊆r fset(fset(T + T))⌝⋅ THENA (RWO "fl-point-sq" 0 THEN Auto))
   THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. i : T
4. s : fset(fset(T + T))
5. Point(face-lattice(T;eq)) ⊆r fset(fset(T + T))
6. fset-all(s;x.inr i  ∈b x)
⊢ fset-ac-le(union-deq(T;T;eq;eq);s;(i=1))

2
1. T : Type
2. eq : EqDecider(T)
3. i : T
4. s : fset(fset(T + T))
5. Point(face-lattice(T;eq)) ⊆r fset(fset(T + T))
6. fset-ac-le(union-deq(T;T;eq;eq);s;(i=1))
⊢ fset-all(s;x.inr i  ∈b x)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[i:T].  \mforall{}[s:fset(fset(T  +  T))].
    (fset-all(s;x.inr  i    \mmember{}\msubb{}  x)  \mLeftarrow{}{}\mRightarrow{}  fset-ac-le(union-deq(T;T;eq;eq);s;(i=1)))


By

---

Latex:
(Intros
  THEN  (Assert  \mkleeneopen{}Point(face-lattice(T;eq))  \msubseteq{}r  fset(fset(T  +  T))\mkleeneclose{}\mcdot{}
              THENA  (RWO  "fl-point-sq"  0  THEN  Auto)
              )
  THEN  Auto)

---

Home Index