---

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


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 - 1;f;b))@i
9. i : ℕ@i
10. b < i@i
11. i < n@i
12. ¬(n = 0 ∈ ℤ)
13. ¬n - 1 < b
14. ¬((n - 1) = b ∈ ℤ)
15. ¬↑isl(M (n - 1) f)
16. ∀i:ℕ. (b < i ⇒ i < n - 1 ⇒ (↑isr(M i f)))
⊢ ↑isr(M i f)
BY
{ ((FLemma `not-isl-assert-isr` [-2] THEN Auto) THEN Decide ⌜i = (n - 1) ∈ ℕ⌝⋅ THEN Try (CpltAuto)) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  M  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  (\mBbbN{}n?)
3.  n  :  \mBbbZ{}
4.  0  <  n
5.  \mforall{}[f:\mBbbN{}n  -  1  {}\mrightarrow{}  T].  \mforall{}[b:\mBbbN{}n  -  1].
          ((\muparrow{}isl(strong-continuity-test-bound(M;n  -  1;f;b)))
          {}\mRightarrow{}  (\mforall{}i:\mBbbN{}.  (b  <  i  {}\mRightarrow{}  i  <  n  -  1  {}\mRightarrow{}  (\muparrow{}isr(M  i  f)))))
6.  f  :  \mBbbN{}n  {}\mrightarrow{}  T
7.  b  :  \mBbbN{}n
8.  \muparrow{}isl(strong-continuity-test-bound(M;n  -  1;f;b))@i
9.  i  :  \mBbbN{}@i
10.  b  <  i@i
11.  i  <  n@i
12.  \mneg{}(n  =  0)
13.  \mneg{}n  -  1  <  b
14.  \mneg{}((n  -  1)  =  b)
15.  \mneg{}\muparrow{}isl(M  (n  -  1)  f)
16.  \mforall{}i:\mBbbN{}.  (b  <  i  {}\mRightarrow{}  i  <  n  -  1  {}\mRightarrow{}  (\muparrow{}isr(M  i  f)))
\mvdash{}  \muparrow{}isr(M  i  f)


By

---

Latex:
((FLemma  `not-isl-assert-isr`  [-2]  THEN  Auto)  THEN  Decide  \mkleeneopen{}i  =  (n  -  1)\mkleeneclose{}\mcdot{}  THEN  Try  (CpltAuto))

---

Home Index