---

Step * of Lemma assert-fset-contains-none

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[Cs:T ⟶ fset(fset(T))].
  uiff(↑fset-contains-none(eq;s;x.Cs[x]);∀x:T. (x ∈ s ⇒ (∀c:fset(T). (c ∈ Cs[x] ⇒ (¬c ⊆ s)))))
BY
{ ((UnivCD THENA Auto) THEN Unfold `fset-contains-none` 0 THEN (RWO "assert-fset-contains-none-of" 0 THENA Auto)) }

1
1. T : Type
2. eq : EqDecider(T)
3. s : fset(T)
4. Cs : T ⟶ fset(fset(T))
⊢ uiff(∀c:fset(T). (c ∈ f-union(eq;deq-fset(eq);s;x.Cs[x]) ⇒ (¬c ⊆ s));∀x:T
                                                                          (x ∈ s
                                                                          ⇒ (∀c:fset(T). (c ∈ Cs[x] ⇒ (¬c ⊆ s)))))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[s:fset(T)].  \mforall{}[Cs:T  {}\mrightarrow{}  fset(fset(T))].
    uiff(\muparrow{}fset-contains-none(eq;s;x.Cs[x]);\mforall{}x:T.  (x  \mmember{}  s  {}\mRightarrow{}  (\mforall{}c:fset(T).  (c  \mmember{}  Cs[x]  {}\mRightarrow{}  (\mneg{}c  \msubseteq{}  s)))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `fset-contains-none`  0
  THEN  (RWO  "assert-fset-contains-none-of"  0  THENA  Auto))

---

Home Index