---

Step * of Lemma l_all_filter

∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].  (∀x∈filter(P;L).↑(P x))
BY
{ (Auto THEN ((RWO "l_all_iff" 0 THEN Auto) THEN RWO "member_filter" (-1)) THEN Auto{1,3}-1) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].    (\mforall{}x\mmember{}filter(P;L).\muparrow{}(P  x))


By

---

Latex:
(Auto  THEN  ((RWO  "l\_all\_iff"  0  THEN  Auto)  THEN  RWO  "member\_filter"  (-1))  THEN  Auto\{1,3\}-1)

---

Home Index