---

Step * 1 of Lemma iseg-mapfilter


1. [T] : Type
2. P : T ⟶ 𝔹
3. [T'] : Type
4. f : {x:T| ↑(P x)}  ⟶ T'
⊢ ∀L2:T List. ([] ≤ L2 ⇒ [] ≤ mapfilter(f;P;L2))
BY
{ Auto }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  [T']  :  Type
4.  f  :  \{x:T|  \muparrow{}(P  x)\}    {}\mrightarrow{}  T'
\mvdash{}  \mforall{}L2:T  List.  ([]  \mleq{}  L2  {}\mRightarrow{}  []  \mleq{}  mapfilter(f;P;L2))


By

---

Latex:
Auto

---

Home Index