---

Step * 2 1 1 1 1 2 1 1 2 of Lemma bag-intersection


1. n : ℕ
2. m : ℕ
3. p : ℕ
4. q : ℕ
5. f : ℕp + q ⟶ ℕn + m
6. Inj(ℕp + q;ℕn + m;f)
7. (p + q) = (n + m) ∈ ℤ
8. m < n
9. q < p
10. ∀i:ℕp. (n ≤ f[i])
11. Inj(ℕp;{n..n + m-};f)
12. f ∈ ℕp ⟶ {n..n + m-}
⊢ ∃f:ℕp ⟶ ℕm. Inj(ℕp;ℕm;f)
BY
{ Assert ⌜{n..n + m-} ~ ℕm⌝⋅ }

1
.....assertion..... 
1. n : ℕ
2. m : ℕ
3. p : ℕ
4. q : ℕ
5. f : ℕp + q ⟶ ℕn + m
6. Inj(ℕp + q;ℕn + m;f)
7. (p + q) = (n + m) ∈ ℤ
8. m < n
9. q < p
10. ∀i:ℕp. (n ≤ f[i])
11. Inj(ℕp;{n..n + m-};f)
12. f ∈ ℕp ⟶ {n..n + m-}
⊢ {n..n + m-} ~ ℕm

2
1. n : ℕ
2. m : ℕ
3. p : ℕ
4. q : ℕ
5. f : ℕp + q ⟶ ℕn + m
6. Inj(ℕp + q;ℕn + m;f)
7. (p + q) = (n + m) ∈ ℤ
8. m < n
9. q < p
10. ∀i:ℕp. (n ≤ f[i])
11. Inj(ℕp;{n..n + m-};f)
12. f ∈ ℕp ⟶ {n..n + m-}
13. {n..n + m-} ~ ℕm
⊢ ∃f:ℕp ⟶ ℕm. Inj(ℕp;ℕm;f)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  p  :  \mBbbN{}
4.  q  :  \mBbbN{}
5.  f  :  \mBbbN{}p  +  q  {}\mrightarrow{}  \mBbbN{}n  +  m
6.  Inj(\mBbbN{}p  +  q;\mBbbN{}n  +  m;f)
7.  (p  +  q)  =  (n  +  m)
8.  m  <  n
9.  q  <  p
10.  \mforall{}i:\mBbbN{}p.  (n  \mleq{}  f[i])
11.  Inj(\mBbbN{}p;\{n..n  +  m\msupminus{}\};f)
12.  f  \mmember{}  \mBbbN{}p  {}\mrightarrow{}  \{n..n  +  m\msupminus{}\}
\mvdash{}  \mexists{}f:\mBbbN{}p  {}\mrightarrow{}  \mBbbN{}m.  Inj(\mBbbN{}p;\mBbbN{}m;f)


By

---

Latex:
Assert  \mkleeneopen{}\{n..n  +  m\msupminus{}\}  \msim{}  \mBbbN{}m\mkleeneclose{}\mcdot{}

---

Home Index