---

Step * of Lemma partition-split-cons-mesh

∀[I:Interval]
  ∀[a:ℝ]. ∀[bs:ℝ List].
    (partitions(I;[a / bs])
    ⇒ (partitions([left-endpoint(I), a];[])
       ∧ partitions([a, right-endpoint(I)];bs)
       ∧ (left-endpoint(I) ≤ a)
       ∧ (a ≤ right-endpoint(I))
       ∧ (partition-mesh([left-endpoint(I), a];[]) ≤ partition-mesh(I;[a / bs]))
       ∧ (partition-mesh([a, right-endpoint(I)];bs) ≤ partition-mesh(I;[a / bs])))) 
  supposing icompact(I)
BY
{ (InstLemma `partition-split-cons` []
   THEN (Intros THEN (InstHyp [⌜I⌝;⌜a⌝;⌜bs⌝] 1⋅ THENA Auto) THEN Thin 1)
   THEN SplitAndHyps
   THEN Auto) }

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

2
1. [I] : Interval
2. [%] : icompact(I)
3. [a] : ℝ
4. [bs] : ℝ List
5. partitions(I;[a / bs])
6. partitions([left-endpoint(I), a];[])
7. partitions([a, right-endpoint(I)];bs)
8. partitions([left-endpoint(I), a];[])
9. partitions([a, right-endpoint(I)];bs)
10. left-endpoint(I) ≤ a
11. a ≤ right-endpoint(I)
⊢ partition-mesh([left-endpoint(I), a];[]) ≤ partition-mesh(I;[a / bs])

3
1. [I] : Interval
2. [%] : icompact(I)
3. [a] : ℝ
4. [bs] : ℝ List
5. partitions(I;[a / bs])
6. partitions([left-endpoint(I), a];[])
7. partitions([a, right-endpoint(I)];bs)
8. partitions([left-endpoint(I), a];[])
9. partitions([a, right-endpoint(I)];bs)
10. left-endpoint(I) ≤ a
11. a ≤ right-endpoint(I)
12. partition-mesh([left-endpoint(I), a];[]) ≤ partition-mesh(I;[a / bs])
⊢ partition-mesh([a, right-endpoint(I)];bs) ≤ partition-mesh(I;[a / 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)
              \mwedge{}  (left-endpoint(I)  \mleq{}  a)
              \mwedge{}  (a  \mleq{}  right-endpoint(I))
              \mwedge{}  (partition-mesh([left-endpoint(I),  a];[])  \mleq{}  partition-mesh(I;[a  /  bs]))
              \mwedge{}  (partition-mesh([a,  right-endpoint(I)];bs)  \mleq{}  partition-mesh(I;[a  /  bs])))) 
    supposing  icompact(I)


By

---

Latex:
(InstLemma  `partition-split-cons`  []
  THEN  (Intros  THEN  (InstHyp  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]  1\mcdot{}  THENA  Auto)  THEN  Thin  1)
  THEN  SplitAndHyps
  THEN  Auto)

---

Home Index