Step
*
1
1
1
2
1
1
of Lemma
strong-continuity2-implies-uniform-continuity2-int
1. F : (ℕ ⟶ 𝔹) ⟶ ℤ
2. ⇃(∃n:ℕ. ucpB(ℤ;F;n))
3. a : ∃n:ℕ. ucpB(ℤ;F;n)
4. b : ∃n:ℕ. ucpB(ℤ;F;n)
⊢ a = b ∈ (∃n:ℕ. ucpB(ℤ;F;n))
BY
{ TACTIC:ExRepD }
1
1. F : (ℕ ⟶ 𝔹) ⟶ ℤ
2. ⇃(∃n:ℕ. ucpB(ℤ;F;n))
3. n1 : ℕ
4. a1 : ucpB(ℤ;F;n1)
5. n : ℕ
6. b1 : ucpB(ℤ;F;n)
⊢ <n1, a1> = <n, b1> ∈ (∃n:ℕ. ucpB(ℤ;F;n))
Latex:
Latex:
1. F : (\mBbbN{} {}\mrightarrow{} \mBbbB{}) {}\mrightarrow{} \mBbbZ{}
2. \00D9(\mexists{}n:\mBbbN{}. ucpB(\mBbbZ{};F;n))
3. a : \mexists{}n:\mBbbN{}. ucpB(\mBbbZ{};F;n)
4. b : \mexists{}n:\mBbbN{}. ucpB(\mBbbZ{};F;n)
\mvdash{} a = b
By
Latex:
TACTIC:ExRepD
Home
Index