---

Step * of Lemma strong-continuity-test_wf

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

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

---

Latex:

---

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


By

---

Latex:
TACTIC:(UnivCD  THENA  Auto)

---

Home Index