---

Step * of Lemma disjoint_increasing_onto

∀[m,n,k:ℕ]. ∀[f:ℕn ⟶ ℕm]. ∀[g:ℕk ⟶ ℕm].
  (m = (n + k) ∈ ℕ) supposing 
     ((∀j1:ℕn. ∀j2:ℕk.  (¬((f j1) = (g j2) ∈ ℤ))) and 
     (∀i:ℕm. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))) and 
     increasing(g;k) and 
     increasing(f;n))
BY
{ 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) ∈ ℤ))
⊢ m = (n + k) ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[m,n,k:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}m].  \mforall{}[g:\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}m].
    (m  =  (n  +  k))  supposing 
          ((\mforall{}j1:\mBbbN{}n.  \mforall{}j2:\mBbbN{}k.    (\mneg{}((f  j1)  =  (g  j2))))  and 
          (\mforall{}i:\mBbbN{}m.  ((\mexists{}j:\mBbbN{}n.  (i  =  (f  j)))  \mvee{}  (\mexists{}j:\mBbbN{}k.  (i  =  (g  j)))))  and 
          increasing(g;k)  and 
          increasing(f;n))


By

---

Latex:
Auto

---

Home Index