---

Step * of Lemma iseg-mapfilter

∀[T:Type]
  ∀P:T ⟶ 𝔹. ∀[T':Type]. ∀f:{x:T| ↑(P x)}  ⟶ T'. ∀L1,L2:T List.  (L1 ≤ L2 ⇒ mapfilter(f;P;L1) ≤ mapfilter(f;P;L2))
BY
{ (InductionOnList THEN Unfold `mapfilter` 0 THEN Reduce 0 THEN Fold `mapfilter` 0) }

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

2
1. [T] : Type
2. P : T ⟶ 𝔹
3. [T'] : Type
4. f : {x:T| ↑(P x)}  ⟶ T'
5. u : T
6. v : T List
7. ∀L2:T List. (v ≤ L2 ⇒ mapfilter(f;P;v) ≤ mapfilter(f;P;L2))
⊢ ∀L2:T List. ([u / v] ≤ L2 ⇒ map(f;if P u then [u / filter(P;v)] else filter(P;v) fi ) ≤ mapfilter(f;P;L2))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}
        \mforall{}[T':Type]
            \mforall{}f:\{x:T|  \muparrow{}(P  x)\}    {}\mrightarrow{}  T'.  \mforall{}L1,L2:T  List.    (L1  \mleq{}  L2  {}\mRightarrow{}  mapfilter(f;P;L1)  \mleq{}  mapfilter(f;P;L2))


By

---

Latex:
(InductionOnList  THEN  Unfold  `mapfilter`  0  THEN  Reduce  0  THEN  Fold  `mapfilter`  0)

---

Home Index