Step
*
of Lemma
uniform-continuity-pi-pi-prop
∀[T:Type]. ∀[F:(ℕ ⟶ 𝔹) ⟶ T]. ∀[n,m:ℕ].  (n = m ∈ ℕ) supposing (ucpB(T;F;m) and ucpB(T;F;n))
BY
{ ((UnivCD THENA Auto)
   THEN All(Unfold `uniform-continuity-pi-pi`)
   THEN DProdsAndUnions
   THEN (Assert ⌜n < m ∨ (m ≤ n)⌝⋅ THENA Auto)
   THEN D (-1)) }
1
1. T : Type
2. F : (ℕ ⟶ 𝔹) ⟶ T
3. n : ℕ
4. m : ℕ
5. ucA(T;F;n)
6. ∀i:ℕ. (ucA(T;F;i) 
⇒ (n ≤ i))
7. ucA(T;F;m)
8. ∀i:ℕ. (ucA(T;F;i) 
⇒ (m ≤ i))
9. n < m
⊢ n = m ∈ ℕ
2
1. T : Type
2. F : (ℕ ⟶ 𝔹) ⟶ T
3. n : ℕ
4. m : ℕ
5. ucA(T;F;n)
6. ∀i:ℕ. (ucA(T;F;i) 
⇒ (n ≤ i))
7. ucA(T;F;m)
8. ∀i:ℕ. (ucA(T;F;i) 
⇒ (m ≤ i))
9. m ≤ n
⊢ n = m ∈ ℕ
Latex:
Latex:
\mforall{}[T:Type].  \mforall{}[F:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  T].  \mforall{}[n,m:\mBbbN{}].    (n  =  m)  supposing  (ucpB(T;F;m)  and  ucpB(T;F;n))
By
Latex:
((UnivCD  THENA  Auto)
  THEN  All(Unfold  `uniform-continuity-pi-pi`)
  THEN  DProdsAndUnions
  THEN  (Assert  \mkleeneopen{}n  <  m  \mvee{}  (m  \mleq{}  n)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  (-1))
Home
Index