---

Step * 1 2 1 1 1 of Lemma general-cantor-to-int-uniform-continuity


1. n : ℕ
2. B : ℕ ⟶ ℕ+
3. F : (k:ℕ ⟶ ℕB[k]) ⟶ ℤ
4. ⇃(∃n:ℕ. (f:(i:ℕ ⟶ ℕB[i]) ⟶ g:(i:ℕ ⟶ ℕB[i]) ⟶ (f = g ∈ (i:ℕn ⟶ ℕB[i])) ⟶ ((F f) = (F g) ∈ ℤ)))
5. ⇃(∃n:ℕ
      ((f:(i:ℕ ⟶ ℕB[i]) ⟶ g:(i:ℕ ⟶ ℕB[i]) ⟶ (f = g ∈ (i:ℕn ⟶ ℕB[i])) ⟶ ((F f) = (F g) ∈ ℤ))
      ∧ (j:ℕ ⟶ (f:(i:ℕ ⟶ ℕB[i]) ⟶ g:(i:ℕ ⟶ ℕB[i]) ⟶ (f = g ∈ (i:ℕj ⟶ ℕB[i])) ⟶ ((F f) = (F g) ∈ ℤ)) ⟶ (n ≤ j))))
6. a2 : f:(i:ℕ ⟶ ℕB[i]) ⟶ g:(i:ℕ ⟶ ℕB[i]) ⟶ (f = g ∈ (i:ℕn ⟶ ℕB[i])) ⟶ ((F f) = (F g) ∈ ℤ)
7. a3 : j:ℕ ⟶ (f:(i:ℕ ⟶ ℕB[i]) ⟶ g:(i:ℕ ⟶ ℕB[i]) ⟶ (f = g ∈ (i:ℕj ⟶ ℕB[i])) ⟶ ((F f) = (F g) ∈ ℤ)) ⟶ (n ≤ j)
8. b2 : f:(i:ℕ ⟶ ℕB[i]) ⟶ g:(i:ℕ ⟶ ℕB[i]) ⟶ (f = g ∈ (i:ℕn ⟶ ℕB[i])) ⟶ ((F f) = (F g) ∈ ℤ)
9. b3 : j:ℕ ⟶ (f:(i:ℕ ⟶ ℕB[i]) ⟶ g:(i:ℕ ⟶ ℕB[i]) ⟶ (f = g ∈ (i:ℕj ⟶ ℕB[i])) ⟶ ((F f) = (F g) ∈ ℤ)) ⟶ (n ≤ j)
10. f : i:ℕ ⟶ ℕB[i]
11. g : i:ℕ ⟶ ℕB[i]
12. x : f = g ∈ (i:ℕn ⟶ ℕB[i])
13. v : (F f) = (F g) ∈ ℤ
14. (a2 f g x) = v ∈ ((F f) = (F g) ∈ ℤ)
15. v1 : (F f) = (F g) ∈ ℤ
16. (b2 f g x) = v1 ∈ ((F f) = (F g) ∈ ℤ)
⊢ v = v1 ∈ ((F f) = (F g) ∈ ℤ)
BY
{ ((D -4 THEN D -2) THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  B  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
3.  F  :  (k:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[k])  {}\mrightarrow{}  \mBbbZ{}
4.  \00D9(\mexists{}n:\mBbbN{}.  (f:(i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  g:(i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  (f  =  g)  {}\mrightarrow{}  ((F  f)  =  (F  g))))
5.  \00D9(\mexists{}n:\mBbbN{}
            ((f:(i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  g:(i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  (f  =  g)  {}\mrightarrow{}  ((F  f)  =  (F  g)))
            \mwedge{}  (j:\mBbbN{}  {}\mrightarrow{}  (f:(i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  g:(i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  (f  =  g)  {}\mrightarrow{}  ((F  f)  =  (F  g)))  {}\mrightarrow{}  (n  \mleq{}  j))))
6.  a2  :  f:(i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  g:(i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  (f  =  g)  {}\mrightarrow{}  ((F  f)  =  (F  g))
7.  a3  :  j:\mBbbN{}  {}\mrightarrow{}  (f:(i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  g:(i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  (f  =  g)  {}\mrightarrow{}  ((F  f)  =  (F  g)))  {}\mrightarrow{}  (n  \mleq{}  j)
8.  b2  :  f:(i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  g:(i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  (f  =  g)  {}\mrightarrow{}  ((F  f)  =  (F  g))
9.  b3  :  j:\mBbbN{}  {}\mrightarrow{}  (f:(i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  g:(i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  (f  =  g)  {}\mrightarrow{}  ((F  f)  =  (F  g)))  {}\mrightarrow{}  (n  \mleq{}  j)
10.  f  :  i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i]
11.  g  :  i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i]
12.  x  :  f  =  g
13.  v  :  (F  f)  =  (F  g)
14.  (a2  f  g  x)  =  v
15.  v1  :  (F  f)  =  (F  g)
16.  (b2  f  g  x)  =  v1
\mvdash{}  v  =  v1


By

---

Latex:
((D  -4  THEN  D  -2)  THEN  Auto)

---

Home Index