---

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


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)
BY
{ ((FLemma `fset-ac-le-implies2` [-1] THENA Auto)
   THEN (InstLemma `fset-all-iff` [⌜fset(T + T)⌝;⌜deq-fset(union-deq(T;T;eq;eq))⌝]⋅ THENA Auto)
   THEN (RWO  "-1" 0 THENA Auto)
   THEN Thin (-1)) }

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-ac-le(union-deq(T;T;eq;eq);s;(i=1))
7. ∀a:fset(T + T). (a ∈ s ⇒ (↓∃b:fset(T + T). (b ∈ (i=1) ∧ b ⊆ a)))
⊢ ∀[x:fset(T + T)]. ↑inr i  ∈b x supposing x ∈ s

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  i  :  T
4.  s  :  fset(fset(T  +  T))
5.  Point(face-lattice(T;eq))  \msubseteq{}r  fset(fset(T  +  T))
6.  fset-ac-le(union-deq(T;T;eq;eq);s;(i=1))
\mvdash{}  fset-all(s;x.inr  i    \mmember{}\msubb{}  x)


By

---

Latex:
((FLemma  `fset-ac-le-implies2`  [-1]  THENA  Auto)
  THEN  (InstLemma  `fset-all-iff`  [\mkleeneopen{}fset(T  +  T)\mkleeneclose{};\mkleeneopen{}deq-fset(union-deq(T;T;eq;eq))\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO    "-1"  0  THENA  Auto)
  THEN  Thin  (-1))

---

Home Index