---

Step * of Lemma partition-split-cons

∀[I:Interval]
  ∀[a:ℝ]. ∀[bs:ℝ List].
    (partitions(I;[a / bs]) ⇒ (partitions([left-endpoint(I), a];[]) ∧ partitions([a, right-endpoint(I)];bs))) 
  supposing icompact(I)
BY
{ (Auto THEN RepUR ``i-finite`` 0 THEN Auto) }

1
1. I : Interval
2. icompact(I)
3. a : ℝ
4. bs : ℝ List
5. partitions(I;[a / bs])
⊢ partitions([left-endpoint(I), a];[])

2
1. I : Interval
2. icompact(I)
3. a : ℝ
4. bs : ℝ List
5. partitions(I;[a / bs])
6. partitions([left-endpoint(I), a];[])
⊢ partitions([a, right-endpoint(I)];bs)

---

Latex:

---

Latex:
\mforall{}[I:Interval]
    \mforall{}[a:\mBbbR{}].  \mforall{}[bs:\mBbbR{}  List].
        (partitions(I;[a  /  bs])
        {}\mRightarrow{}  (partitions([left-endpoint(I),  a];[])  \mwedge{}  partitions([a,  right-endpoint(I)];bs))) 
    supposing  icompact(I)


By

---

Latex:
(Auto  THEN  RepUR  ``i-finite``  0  THEN  Auto)

---

Home Index