---

Step * of Lemma l_all-mapfilter

∀[T,A:Type].
  ∀as:T List. ∀p:{a:T| (a ∈ as)}  ⟶ 𝔹. ∀f:{a:T| (a ∈ as) ∧ (↑(p a))}  ⟶ A. ∀P:A ⟶ ℙ.
    ((∀x∈mapfilter(f;p;as).P[x]) ⇐⇒ (∀x∈as.(↑(p x)) ⇒ P[f x]))
BY
{ TACTIC:((UnivCD THENA Auto)
          THEN (InstLemma `l_all_wf` [⌜A⌝;⌜mapfilter(f;p;as)⌝;⌜P⌝]⋅ THENA Auto)
          THEN Auto
          THEN All(RWO "l_all_iff")
          THEN Auto) }

1
1. [T] : Type
2. [A] : Type
3. as : T List
4. p : {a:T| (a ∈ as)}  ⟶ 𝔹
5. f : {a:T| (a ∈ as) ∧ (↑(p a))}  ⟶ A
6. P : A ⟶ ℙ
7. (∀x∈mapfilter(f;p;as).P[x]) ∈ ℙ
8. (∀x∈mapfilter(f;p;as).P[x])
9. x : T
10. (x ∈ as)
11. ↑(p x)
⊢ P[f x]

2
1. [T] : Type
2. [A] : Type
3. as : T List
4. p : {a:T| (a ∈ as)}  ⟶ 𝔹
5. f : {a:T| (a ∈ as) ∧ (↑(p a))}  ⟶ A
6. P : A ⟶ ℙ
7. (∀x∈mapfilter(f;p;as).P[x]) ∈ ℙ
8. ∀x:T. ((x ∈ as) ⇒ (↑(p x)) ⇒ P[f x])
⊢ (∀x∈mapfilter(f;p;as).P[x])

---

Latex:

---

Latex:
\mforall{}[T,A:Type].
    \mforall{}as:T  List.  \mforall{}p:\{a:T|  (a  \mmember{}  as)\}    {}\mrightarrow{}  \mBbbB{}.  \mforall{}f:\{a:T|  (a  \mmember{}  as)  \mwedge{}  (\muparrow{}(p  a))\}    {}\mrightarrow{}  A.  \mforall{}P:A  {}\mrightarrow{}  \mBbbP{}.
        ((\mforall{}x\mmember{}mapfilter(f;p;as).P[x])  \mLeftarrow{}{}\mRightarrow{}  (\mforall{}x\mmember{}as.(\muparrow{}(p  x))  {}\mRightarrow{}  P[f  x]))


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)
                THEN  (InstLemma  `l\_all\_wf`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}mapfilter(f;p;as)\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  Auto
                THEN  All(RWO  "l\_all\_iff")
                THEN  Auto)

---

Home Index