---

Step * of Lemma strong-continuity-test-bound-prop2

∀[T:Type]. ∀[M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕn?)]. ∀[n:ℕ]. ∀[f:ℕn ⟶ T]. ∀[b:ℕn].
  ((↑isl(strong-continuity-test-bound(M;n;f;b))) ⇒ (∀i:ℕ. (b < i ⇒ i < n ⇒ (↑isr(M i f)))))
BY
{ (RepeatFor 3 ((D 0 THENA Auto)) THEN NatInd (-1) THEN UnivCD THEN Try (CpltAuto)) }

1
1. T : Type
2. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕn?)
3. n : ℤ
4. 0 < n
5. ∀[f:ℕn - 1 ⟶ T]. ∀[b:ℕn - 1].
     ((↑isl(strong-continuity-test-bound(M;n - 1;f;b))) ⇒ (∀i:ℕ. (b < i ⇒ i < n - 1 ⇒ (↑isr(M i f)))))
6. f : ℕn ⟶ T
7. b : ℕn
8. ↑isl(strong-continuity-test-bound(M;n;f;b))@i
9. i : ℕ@i
10. b < i@i
11. i < n@i
⊢ ↑isr(M i f)

---

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].
    ((\muparrow{}isl(strong-continuity-test-bound(M;n;f;b)))  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}.  (b  <  i  {}\mRightarrow{}  i  <  n  {}\mRightarrow{}  (\muparrow{}isr(M  i  f)))))


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))  THEN  NatInd  (-1)  THEN  UnivCD  THEN  Try  (CpltAuto))

---

Home Index