---

Step * 1 of Lemma finite-union


1. S : Type
2. T : Type
3. n1 : ℕ
4. S ~ ℕn1
5. n : ℕ
6. T ~ ℕn
⊢ ∃n:ℕ. S + T ~ ℕn
BY
{ ((D 0 With ⌜n1 + n⌝  THEN Auto) THEN (RWO "equipollent-add<" 0 THENA Auto)) }

1
1. S : Type
2. T : Type
3. n1 : ℕ
4. S ~ ℕn1
5. n : ℕ
6. T ~ ℕn
⊢ S + T ~ ℕn1 + ℕn

---

Latex:

---

Latex:

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


By

---

Latex:
((D  0  With  \mkleeneopen{}n1  +  n\mkleeneclose{}    THEN  Auto)  THEN  (RWO  "equipollent-add<"  0  THENA  Auto))

---

Home Index