---

Step * of Lemma fset-filter-subset

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)].  {x ∈ s | P[x]} ⊆ s
BY
{ (Auto THEN D 0 THEN Auto THEN RWO "member-fset-filter" (-1) THEN Auto) }

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  RWO  "member-fset-filter"  (-1)  THEN  Auto)

---

Home Index