---

Step * of Lemma strong-continuity-test-bound_wf

∀[T:Type]. ∀[M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕn?)]. ∀[n:ℕ]. ∀[f:ℕn ⟶ T]. ∀[b:ℕn].  (strong-continuity-test-bound(M;n;f;b) ∈ ℕn?)
BY
{ (UnivCD THENA Auto) }

1
1. T : Type
2. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕn?)
3. n : ℕ
4. f : ℕn ⟶ T
5. b : ℕn
⊢ strong-continuity-test-bound(M;n;f;b) ∈ ℕn?

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[M:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  (\mBbbN{}n?)].  \mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  T].  \mforall{}[b:\mBbbN{}n].
    (strong-continuity-test-bound(M;n;f;b)  \mmember{}  \mBbbN{}n?)


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index