---

Step * of Lemma uniform-continuity-pi-pi-prop2

∀T:Type. ∀F:(ℕ ⟶ 𝔹) ⟶ T.  ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ (∃n:ℕ. ucpB(T;F;n) ⇐⇒ ∃n:ℕ. ucA(T;F;n)))
BY
{ ((UnivCD THENA Auto) THEN D 0 THEN Auto) }

1
1. T : Type
2. F : (ℕ ⟶ 𝔹) ⟶ T
3. ∀x,y:T.  Dec(x = y ∈ T)
4. ∃n:ℕ. ucpB(T;F;n)
⊢ ∃n:ℕ. ucA(T;F;n)

2
1. T : Type
2. F : (ℕ ⟶ 𝔹) ⟶ T
3. ∀x,y:T.  Dec(x = y ∈ T)
4. ∃n:ℕ. ucA(T;F;n)
⊢ ∃n:ℕ. ucpB(T;F;n)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  T.    ((\mforall{}x,y:T.    Dec(x  =  y))  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  ucpB(T;F;n)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  ucA(T;F;n)))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  D  0  THEN  Auto)

---

Home Index