Step
*
1
2
1
1
of Lemma
general-cantor-to-int-uniform-continuity
1. n : ℕ
2. B : ℕ ⟶ ℕ+
3. F : (k:ℕ ⟶ ℕB[k]) ⟶ ℤ
4. ⇃(∃n:ℕ. ∀f,g:i:ℕ ⟶ ℕB[i]. ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ)))
5. ⇃(∃n:ℕ
((∀f,g:i:ℕ ⟶ ℕB[i]. ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ)))
∧ (∀j:ℕ. ((∀f,g:i:ℕ ⟶ ℕB[i]. ((f = g ∈ (i:ℕj ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ))) ⇒ (n ≤ j)))))
6. a2 : ∀f,g:i:ℕ ⟶ ℕB[i]. ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ))
7. a3 : ∀j:ℕ. ((∀f,g:i:ℕ ⟶ ℕB[i]. ((f = g ∈ (i:ℕj ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ))) ⇒ (n ≤ j))
8. b2 : ∀f,g:i:ℕ ⟶ ℕB[i]. ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ))
9. b3 : ∀j:ℕ. ((∀f,g:i:ℕ ⟶ ℕB[i]. ((f = g ∈ (i:ℕj ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ))) ⇒ (n ≤ j))
⊢ <a2, a3>
= <b2, b3>
∈ ((∀f,g:i:ℕ ⟶ ℕB[i]. ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ)))
∧ (∀j:ℕ. ((∀f,g:i:ℕ ⟶ ℕB[i]. ((f = g ∈ (i:ℕj ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ))) ⇒ (n ≤ j))))
BY
{ (Unfold `and` 0
THEN EqCD
THEN All (Unfolds ``all implies``)
THEN Repeat ((FunExt THENW Auto))
THEN GenConclAtAddr [2]
THEN GenConclAtAddr [3]) }
1
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) ∈ ℤ)
2
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)
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{}. \mforall{}f,g:i:\mBbbN{} {}\mrightarrow{} \mBbbN{}B[i]. ((f = g) {}\mRightarrow{} ((F f) = (F g))))
5. \00D9(\mexists{}n:\mBbbN{}
((\mforall{}f,g:i:\mBbbN{} {}\mrightarrow{} \mBbbN{}B[i]. ((f = g) {}\mRightarrow{} ((F f) = (F g))))
\mwedge{} (\mforall{}j:\mBbbN{}. ((\mforall{}f,g:i:\mBbbN{} {}\mrightarrow{} \mBbbN{}B[i]. ((f = g) {}\mRightarrow{} ((F f) = (F g)))) {}\mRightarrow{} (n \mleq{} j)))))
6. a2 : \mforall{}f,g:i:\mBbbN{} {}\mrightarrow{} \mBbbN{}B[i]. ((f = g) {}\mRightarrow{} ((F f) = (F g)))
7. a3 : \mforall{}j:\mBbbN{}. ((\mforall{}f,g:i:\mBbbN{} {}\mrightarrow{} \mBbbN{}B[i]. ((f = g) {}\mRightarrow{} ((F f) = (F g)))) {}\mRightarrow{} (n \mleq{} j))
8. b2 : \mforall{}f,g:i:\mBbbN{} {}\mrightarrow{} \mBbbN{}B[i]. ((f = g) {}\mRightarrow{} ((F f) = (F g)))
9. b3 : \mforall{}j:\mBbbN{}. ((\mforall{}f,g:i:\mBbbN{} {}\mrightarrow{} \mBbbN{}B[i]. ((f = g) {}\mRightarrow{} ((F f) = (F g)))) {}\mRightarrow{} (n \mleq{} j))
\mvdash{} <a2, a3> = <b2, b3>
By
Latex:
(Unfold `and` 0
THEN EqCD
THEN All (Unfolds ``all implies``)
THEN Repeat ((FunExt THENW Auto))
THEN GenConclAtAddr [2]
THEN GenConclAtAddr [3])
Home
Index