---

Step * of Lemma fset-filter-subset2

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[P:{x:T| x ∈ s}  ⟶ 𝔹].  {x ∈ s | P[x]} ⊆ s
BY
{ (Intros
   THEN (D 0 THENA Auto)
   THEN D 0
   THEN Try (Complete (Auto))
   THEN Try ((RWO "member-fset-filter2" (-1) THEN Auto))
   THEN GenConcl ⌜{x ∈ s | P[x]} = t ∈ fset(T)⌝⋅
   THEN Try (Complete (Auto))) }

1
.....wf..... 
1. T : Type
2. eq : EqDecider(T)
3. s : fset(T)
4. P : {x:T| x ∈ s}  ⟶ 𝔹
5. a : T
6. {a ∈ s ∧ (↑P[a])}
⊢ {x ∈ s | P[x]} ∈ fset(T)

2
1. T : Type
2. eq : EqDecider(T)
3. s : fset(T)
4. P : {x:T| x ∈ s}  ⟶ 𝔹
5. a : T
6. {a ∈ s ∧ (↑P[a])}
7. t : fset(T)
8. {x ∈ s | P[x]} = t ∈ fset(T)
⊢ a ∈ s

3
.....wf..... 
1. T : Type
2. eq : EqDecider(T)
3. s : fset(T)
4. P : {x:T| x ∈ s}  ⟶ 𝔹
5. a : T
⊢ {x ∈ s | P[x]} ∈ fset(T)

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  (D  0  THENA  Auto)
  THEN  D  0
  THEN  Try  (Complete  (Auto))
  THEN  Try  ((RWO  "member-fset-filter2"  (-1)  THEN  Auto))
  THEN  GenConcl  \mkleeneopen{}\{x  \mmember{}  s  |  P[x]\}  =  t\mkleeneclose{}\mcdot{}
  THEN  Try  (Complete  (Auto)))

---

Home Index