---

Step * 1 2 1 1 2 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. j : ℕ
11. x : f:(i:ℕ ⟶ ℕB[i]) ⟶ g:(i:ℕ ⟶ ℕB[i]) ⟶ (f = g ∈ (i:ℕj ⟶ ℕB[i])) ⟶ ((F f) = (F g) ∈ ℤ)
12. v : n ≤ j
13. (a3 j x) = v ∈ (n ≤ j)
14. v1 : n ≤ j
15. (b3 j x) = v1 ∈ (n ≤ j)
⊢ v = v1 ∈ (n ≤ j)
BY
{ ((InstLemma `le_witness` [⌜n⌝;⌜j⌝;⌜v⌝]⋅ THENA Auto) THEN InstLemma `le_witness` [⌜n⌝;⌜j⌝;⌜v1⌝]⋅ 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.  j  :  \mBbbN{}
11.  x  :  f:(i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  g:(i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  (f  =  g)  {}\mrightarrow{}  ((F  f)  =  (F  g))
12.  v  :  n  \mleq{}  j
13.  (a3  j  x)  =  v
14.  v1  :  n  \mleq{}  j
15.  (b3  j  x)  =  v1
\mvdash{}  v  =  v1


By

---

Latex:
((InstLemma  `le\_witness`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InstLemma  `le\_witness`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index