---

Step * of Lemma last-full-partition

∀[I:Interval]. ∀[p:partition(I)]. (last(full-partition(I;p)) = right-endpoint(I) ∈ ℝ) supposing icompact(I)
BY
{ (Auto THEN Unfold `full-partition` 0 THEN (RWO "last_cons" 0 THENA Auto')) }

1
.....rewrite subgoal..... 
1. I : Interval
2. icompact(I)
3. p : partition(I)
⊢ ¬↑null(p @ [right-endpoint(I)])

2
1. I : Interval
2. icompact(I)
3. p : partition(I)
⊢ last(p @ [right-endpoint(I)]) = right-endpoint(I) ∈ ℝ

---

Latex:

---

Latex:
\mforall{}[I:Interval]
    \mforall{}[p:partition(I)].  (last(full-partition(I;p))  =  right-endpoint(I))  supposing  icompact(I)


By

---

Latex:
(Auto  THEN  Unfold  `full-partition`  0  THEN  (RWO  "last\_cons"  0  THENA  Auto'))

---

Home Index