Step * 1 1 of Lemma disjoint_increasing_onto

.....assertion..... 
1. : ℕ
2. : ℕ
3. : ℕ
4. : ℕn ⟶ ℕm
5. : ℕk ⟶ ℕm
6. increasing(f;n)
7. increasing(g;k)
8. ∀i:ℕm. ((∃j:ℕn. (i (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i (g j) ∈ ℤ)))
9. ∀j1:ℕn. ∀j2:ℕk.  ((f j1) (g j2) ∈ ℤ))
⊢ m ≤ (n k)
BY
(BackThruLemma `injection_le` THEN Auto') }

1
1. : ℕ
2. : ℕ
3. : ℕ
4. : ℕn ⟶ ℕm
5. : ℕk ⟶ ℕm
6. increasing(f;n)
7. increasing(g;k)
8. ∀i:ℕm. ((∃j:ℕn. (i (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i (g j) ∈ ℤ)))
9. ∀j1:ℕn. ∀j2:ℕk.  ((f j1) (g j2) ∈ ℤ))
⊢ ∃f:ℕm ⟶ ℕk. Inj(ℕm;ℕk;f)


Latex:


Latex:
.....assertion..... 
1.  m  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  k  :  \mBbbN{}
4.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}m
5.  g  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbN{}m
6.  increasing(f;n)
7.  increasing(g;k)
8.  \mforall{}i:\mBbbN{}m.  ((\mexists{}j:\mBbbN{}n.  (i  =  (f  j)))  \mvee{}  (\mexists{}j:\mBbbN{}k.  (i  =  (g  j))))
9.  \mforall{}j1:\mBbbN{}n.  \mforall{}j2:\mBbbN{}k.    (\mneg{}((f  j1)  =  (g  j2)))
\mvdash{}  m  \mleq{}  (n  +  k)


By


Latex:
(BackThruLemma  `injection\_le`  THEN  Auto')




Home Index