---

Step * of Lemma fset-filter_wf

∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)].  ({x ∈ s | P[x]} ∈ fset(T))
BY
{ (Auto THEN (D -1 THENA Auto) THEN Unfold `fset-filter` 0 THEN EqTypeCD THEN Auto) }

1
.....antecedent..... 
1. T : Type
2. P : T ⟶ 𝔹
3. s : Base
4. s1 : Base
5. s = s1 ∈ pertype(λx,y. ((x ∈ T List) ∧ (y ∈ T List) ∧ set-equal(T;x;y)))
6. s ∈ T List
7. s1 ∈ T List
8. set-equal(T;s;s1)
⊢ set-equal(T;filter(λx.P[x];s);filter(λx.P[x];s1))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[s:fset(T)].    (\{x  \mmember{}  s  |  P[x]\}  \mmember{}  fset(T))


By

---

Latex:
(Auto  THEN  (D  -1  THENA  Auto)  THEN  Unfold  `fset-filter`  0  THEN  EqTypeCD  THEN  Auto)

---

Home Index