---

Step * of Lemma pairwise-filter

∀[T:Type]. ∀L:T List. ∀[P:T ⟶ T ⟶ ℙ']. ((∀x,y∈L.  P[x;y]) ⇒ (∀Q:T ⟶ 𝔹. (∀x,y∈filter(Q;L).  P[x;y])))
BY
{ Auto }

1
1. [T] : Type
2. L : T List@i
3. [P] : T ⟶ T ⟶ ℙ'
4. (∀x,y∈L.  P[x;y])@i'
5. Q : T ⟶ 𝔹@i
⊢ (∀x,y∈filter(Q;L).  P[x;y])

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L:T  List.  \mforall{}[P:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}'].  ((\mforall{}x,y\mmember{}L.    P[x;y])  {}\mRightarrow{}  (\mforall{}Q:T  {}\mrightarrow{}  \mBbbB{}.  (\mforall{}x,y\mmember{}filter(Q;L).    P[x;y])))


By

---

Latex:
Auto

---

Home Index