---

Step * of Lemma uniform-continuity-pi-dec

∀T:Type. ∀F:(ℕ ⟶ 𝔹) ⟶ T. ∀n:ℕ.  ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ ucA(T;F;n) ⇒ (∀m:ℕ. (m < n ⇒ Dec(ucA(T;F;m)))))
BY
{ TACTIC:TACTIC:(UnivCD THENA Auto) }

1
1. T : Type
2. F : (ℕ ⟶ 𝔹) ⟶ T
3. n : ℕ
4. ∀x,y:T.  Dec(x = y ∈ T)
5. ucA(T;F;n)
6. m : ℕ
7. m < n
⊢ Dec(ucA(T;F;m))

---

Latex:

---

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


By

---

Latex:
TACTIC:TACTIC:(UnivCD  THENA  Auto)

---

Home Index