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 (-1)) }

1
1. Type
2. (ℕ ⟶ 𝔹) ⟶ T
3. : ℕ
4. : ℕ
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
⊢ m ∈ ℕ

2
1. Type
2. (ℕ ⟶ 𝔹) ⟶ T
3. : ℕ
4. : ℕ
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
⊢ 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