---

Step * of Lemma nth_tl-partition

∀I:Interval
  (icompact(I)
  ⇒ (∀a:ℝ. ∀p:partition(I). ∀i:ℕ||p||.  ((a = p[i]) ⇒ (nth_tl(i + 1;p) ∈ partition([a, right-endpoint(I)])))))
BY
{ (Auto THEN DVar `p' THEN MemTypeCD THEN Auto THEN D 5 THEN D 6 THEN Auto) }

1
1. I : Interval
2. icompact(I)
3. a : ℝ
4. p : ℝ List
5. frs-non-dec(p)
6. i : ℕ||p||
7. a = p[i]
8. left-endpoint(I) ≤ p[0]
9. last(p) ≤ right-endpoint(I)
⊢ partitions([a, right-endpoint(I)];nth_tl(i + 1;p))

2
1. I : Interval
2. icompact(I)
3. a : ℝ
4. p : ℝ List
5. frs-non-dec(p)
6. i : ℕ||p||
7. a = p[i]
8. p1 : ℝ List
9. left-endpoint(I) ≤ p[0]
10. last(p) ≤ right-endpoint(I)
⊢ a ≤ right-endpoint(I)

---

Latex:

---

Latex:
\mforall{}I:Interval
    (icompact(I)
    {}\mRightarrow{}  (\mforall{}a:\mBbbR{}.  \mforall{}p:partition(I).  \mforall{}i:\mBbbN{}||p||.
                ((a  =  p[i])  {}\mRightarrow{}  (nth\_tl(i  +  1;p)  \mmember{}  partition([a,  right-endpoint(I)])))))


By

---

Latex:
(Auto  THEN  DVar  `p'  THEN  MemTypeCD  THEN  Auto  THEN  D  5  THEN  D  6  THEN  Auto)

---

Home Index