Step * 2 of Lemma finite-union


1. Type
2. Type
3. : ℕ
4. ~ ℕn
⊢ ∃n:ℕ~ ℕn
BY
((RWO "equipollent-iff-list" (-1) THENA Auto)
   THEN ExRepD
   THEN (Assert mapfilter(λx.outl(x);λx.isl(x);L) ∈ List BY
               (Using [`T',⌜T⌝MemCD⋅ THEN Reduce 0⋅ THEN Auto))) }

1
1. Type
2. Type
3. : ℕ
4. (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) ∈ List
⊢ ∃n:ℕ~ ℕn


Latex:


Latex:

1.  S  :  Type
2.  T  :  Type
3.  n  :  \mBbbN{}
4.  S  +  T  \msim{}  \mBbbN{}n
\mvdash{}  \mexists{}n:\mBbbN{}.  S  \msim{}  \mBbbN{}n


By


Latex:
((RWO  "equipollent-iff-list"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  (Assert  mapfilter(\mlambda{}x.outl(x);\mlambda{}x.isl(x);L)  \mmember{}  S  List  BY
                          (Using  [`T',\mkleeneopen{}S  +  T\mkleeneclose{}]  MemCD\mcdot{}  THEN  Reduce  0\mcdot{}  THEN  Auto)))




Home Index