---

Step * of Lemma assert-fset-contains-none-of

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[cs:fset(fset(T))].
  uiff(↑fset-contains-none-of(eq;s;cs);∀c:fset(T). (c ∈ cs ⇒ (¬c ⊆ s)))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `fset-contains-none-of` 0
   THEN (InstLemma `fset-filter-is-empty` [⌜fset(T)⌝;⌜deq-fset(eq)⌝]⋅ THENA Auto)
   THEN (RWO "assert-fset-null" 0 THENA Auto)
   THEN RWO "-1" 0
   THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. s : fset(T)
4. cs : fset(fset(T))
5. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))].  uiff({x ∈ s | P[x]} = {} ∈ fset(fset(T));¬(∃x:fset(T). (x ∈ s ∧ (↑P[x]))))
6. ∀c:fset(T). (c ∈ cs ⇒ (¬c ⊆ s))
⊢ ¬(∃c:fset(T). (c ∈ cs ∧ (↑(deq-f-subset(eq) c s))))

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `fset-contains-none-of`  0
  THEN  (InstLemma  `fset-filter-is-empty`  [\mkleeneopen{}fset(T)\mkleeneclose{};\mkleeneopen{}deq-fset(eq)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "assert-fset-null"  0  THENA  Auto)
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index