---

Step * 1 2 1 1 1 of Lemma disjoint_increasing_onto


1. m : ℕ
2. n : ℕ
3. k : ℕ
4. f : ℕn ⟶ ℕm
5. g : ℕ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) ∈ ℤ))
10. m ≤ (n + k)
⊢ Inj(ℕn + k;ℕm;λi.if i <z n then f i else g (i - n) fi )
BY
{ (((AllHyps (\i. FwdThruLemma `increasing_inj` [i]))⋅ THEN Auto)
   THEN (All (Unfold `inject`))
   THEN Reduce 0
   THEN (D 0 THENA Auto)
   THEN (D 0 THENA Auto)
   THEN (SplitOnConclITE THENA Complete (Auto))
   THEN (SplitOnConclITE THENA Complete (Auto))
   THEN Auto'
   THEN (AllHyps (\i. ((FwdThruHyp i [(-1)]) THEN Complete (Auto'))))⋅) }

1
1. m : ℕ
2. n : ℕ
3. k : ℕ
4. f : ℕn ⟶ ℕm
5. g : ℕ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) ∈ ℤ))
10. m ≤ (n + k)
11. ∀a1,a2:ℕk.  (((g a1) = (g a2) ∈ ℕm) ⇒ (a1 = a2 ∈ ℕk))
12. ∀a1,a2:ℕn.  (((f a1) = (f a2) ∈ ℕm) ⇒ (a1 = a2 ∈ ℕn))
13. a1 : ℕn + k
14. a2 : ℕn + k
15. a1 < n
16. n ≤ a2
17. (f a1) = (g (a2 - n)) ∈ ℕm
⊢ a1 = a2 ∈ ℕn + k

2
1. m : ℕ
2. n : ℕ
3. k : ℕ
4. f : ℕn ⟶ ℕm
5. g : ℕ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) ∈ ℤ))
10. m ≤ (n + k)
11. ∀a1,a2:ℕk.  (((g a1) = (g a2) ∈ ℕm) ⇒ (a1 = a2 ∈ ℕk))
12. ∀a1,a2:ℕn.  (((f a1) = (f a2) ∈ ℕm) ⇒ (a1 = a2 ∈ ℕn))
13. a1 : ℕn + k
14. a2 : ℕn + k
15. n ≤ a1
16. a2 < n
17. (g (a1 - n)) = (f a2) ∈ ℕm
⊢ a1 = a2 ∈ ℕn + k

---

Latex:

---

Latex:

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)))
10.  m  \mleq{}  (n  +  k)
\mvdash{}  Inj(\mBbbN{}n  +  k;\mBbbN{}m;\mlambda{}i.if  i  <z  n  then  f  i  else  g  (i  -  n)  fi  )


By

---

Latex:
(((AllHyps  (\mbackslash{}i.  FwdThruLemma  `increasing\_inj`  [i]))\mcdot{}  THEN  Auto)
  THEN  (All  (Unfold  `inject`))
  THEN  Reduce  0
  THEN  (D  0  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (SplitOnConclITE  THENA  Complete  (Auto))
  THEN  (SplitOnConclITE  THENA  Complete  (Auto))
  THEN  Auto'
  THEN  (AllHyps  (\mbackslash{}i.  ((FwdThruHyp  i  [(-1)])  THEN  Complete  (Auto'))))\mcdot{})

---

Home Index