---

Step * 2 1 of Lemma iseg-mapfilter


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))
8. L2 : T List
9. [u / v] ≤ L2
⊢ map(f;if P u then [u / filter(P;v)] else filter(P;v) fi ) ≤ mapfilter(f;P;L2)
BY
{ D -2 }

1
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))
8. [u / v] ≤ []
⊢ map(f;if P u then [u / filter(P;v)] else filter(P;v) fi ) ≤ mapfilter(f;P;[])

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))
8. u1 : T
9. v1 : T List
10. [u / v] ≤ [u1 / v1]
⊢ map(f;if P u then [u / filter(P;v)] else filter(P;v) fi ) ≤ mapfilter(f;P;[u1 / v1])

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  [T']  :  Type
4.  f  :  \{x:T|  \muparrow{}(P  x)\}    {}\mrightarrow{}  T'
5.  u  :  T
6.  v  :  T  List
7.  \mforall{}L2:T  List.  (v  \mleq{}  L2  {}\mRightarrow{}  mapfilter(f;P;v)  \mleq{}  mapfilter(f;P;L2))
8.  L2  :  T  List
9.  [u  /  v]  \mleq{}  L2
\mvdash{}  map(f;if  P  u  then  [u  /  filter(P;v)]  else  filter(P;v)  fi  )  \mleq{}  mapfilter(f;P;L2)


By

---

Latex:
D  -2

---

Home Index