---

Step * 2 1 2 of Lemma finite-union


1. S : Type
2. T : Type
3. n : ℕ
4. L : (S + T) List
5. no_repeats(S + T;L)
6. ||L|| = n ∈ ℤ
7. ∀x:S + T. (x ∈ L)
8. mapfilter(λx.outl(x);λx.isl(x);L) ∈ S List
9. no_repeats(S;mapfilter(λx.outl(x);λx.isl(x);L))
10. ||mapfilter(λx.outl(x);λx.isl(x);L)|| = ||mapfilter(λx.outl(x);λx.isl(x);L)|| ∈ ℤ
11. x : S
⊢ (x ∈ mapfilter(λx.outl(x);λx.isl(x);L))
BY
{ (BLemma `member-mapfilter` THEN Reduce 0 THEN Auto THEN D 0 With ⌜inl x⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  S  :  Type
2.  T  :  Type
3.  n  :  \mBbbN{}
4.  L  :  (S  +  T)  List
5.  no\_repeats(S  +  T;L)
6.  ||L||  =  n
7.  \mforall{}x:S  +  T.  (x  \mmember{}  L)
8.  mapfilter(\mlambda{}x.outl(x);\mlambda{}x.isl(x);L)  \mmember{}  S  List
9.  no\_repeats(S;mapfilter(\mlambda{}x.outl(x);\mlambda{}x.isl(x);L))
10.  ||mapfilter(\mlambda{}x.outl(x);\mlambda{}x.isl(x);L)||  =  ||mapfilter(\mlambda{}x.outl(x);\mlambda{}x.isl(x);L)||
11.  x  :  S
\mvdash{}  (x  \mmember{}  mapfilter(\mlambda{}x.outl(x);\mlambda{}x.isl(x);L))


By

---

Latex:
(BLemma  `member-mapfilter`  THEN  Reduce  0  THEN  Auto  THEN  D  0  With  \mkleeneopen{}inl  x\mkleeneclose{}    THEN  Auto)

---

Home Index