---

Step * of Lemma fl-filter-subset

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Q:fset(T + T) ⟶ 𝔹]. ∀[s:fset(fset(T + T))].  fl-filter(s;x.Q[x]) ⊆ s
BY
{ (Intros THEN Unfold `fl-filter` 0 THEN Unfold `cal-filter` 0 THEN BLemma `fset-filter-subset` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[Q:fset(T  +  T)  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[s:fset(fset(T  +  T))].
    fl-filter(s;x.Q[x])  \msubseteq{}  s


By

---

Latex:
(Intros
  THEN  Unfold  `fl-filter`  0
  THEN  Unfold  `cal-filter`  0
  THEN  BLemma  `fset-filter-subset`
  THEN  Auto)

---

Home Index