---

Step * 1 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-all(s;x.inr i  ∈b x)
⊢ fset-ac-le(union-deq(T;T;eq;eq);s;(i=1))
BY
{ ((InstLemma `fset-all-iff` [⌜fset(T + T)⌝;⌜deq-fset(union-deq(T;T;eq;eq))⌝]⋅ THENA Auto)
   THEN (RWO  "-1" (-2) THENA Auto)
   THEN Unfold `fset-ac-le` 0
   THEN (RWO "-1" 0 THENA Auto)
   THEN Thin (-1)
   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. ∀[x:fset(T + T)]. ↑inr i  ∈b x supposing x ∈ s
7. x : fset(T + T)
8. x ∈ s
⊢ ¬↑fset-null({y ∈ (i=1) | deq-f-subset(union-deq(T;T;eq;eq)) y x})

---

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-all(s;x.inr  i    \mmember{}\msubb{}  x)
\mvdash{}  fset-ac-le(union-deq(T;T;eq;eq);s;(i=1))


By

---

Latex:
((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"  (-2)  THENA  Auto)
  THEN  Unfold  `fset-ac-le`  0
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Auto)

---

Home Index