---

Step * of Lemma strong-continuity-test-prop2

∀[T:Type]
  ∀M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?). ∀n:ℕ. ∀f:ℕn ⟶ T. ∀b:ℕ?.
    ((↑isl(b))
    ⇒ (↑isr(strong-continuity-test(M;n;f;b)))
    ⇒ (∃m:ℕ. (m < n ∧ (↑isl(strong-continuity-test(M;m;f;M m f))))))
BY
{ (UnivCD THENA Auto) }

1
1. [T] : Type
2. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)
3. n : ℕ
4. f : ℕn ⟶ T
5. b : ℕ?
6. ↑isl(b)
7. ↑isr(strong-continuity-test(M;n;f;b))
⊢ ∃m:ℕ. (m < n ∧ (↑isl(strong-continuity-test(M;m;f;M m f))))

---

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{}?.
        ((\muparrow{}isl(b))
        {}\mRightarrow{}  (\muparrow{}isr(strong-continuity-test(M;n;f;b)))
        {}\mRightarrow{}  (\mexists{}m:\mBbbN{}.  (m  <  n  \mwedge{}  (\muparrow{}isl(strong-continuity-test(M;m;f;M  m  f))))))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index