---

Step * of Lemma partition-choice-ap_wf

∀I:Interval
  (icompact(I) ⇒ (∀p:partition(I). ∀x:partition-choice(full-partition(I;p)). ∀i:ℕ||p|| + 1.  (x[i] ∈ {x:ℝ| x ∈ I} )))
BY
{ (InstLemma `partition-choice-member` []
   THEN RepeatFor 4 ((ParallelLast' THENA Auto))
   THEN NthHypSq (-1)
   THEN RepeatFor 2 (EqCD)
   THEN Try (Trivial)) }

1
1. I : Interval
2. icompact(I)
3. p : partition(I)
4. x : partition-choice(full-partition(I;p))
5. ∀i:ℕ||full-partition(I;p)|| - 1. (x i ∈ {x:ℝ| x ∈ I} )
⊢ ||p|| + 1 ~ ||full-partition(I;p)|| - 1

2
1. I : Interval
2. icompact(I)
3. p : partition(I)
4. x : partition-choice(full-partition(I;p))
5. ∀i:ℕ||full-partition(I;p)|| - 1. (x i ∈ {x:ℝ| x ∈ I} )
6. i : Base
⊢ x[i] ~ x i

---

Latex:

---

Latex:
\mforall{}I:Interval
    (icompact(I)
    {}\mRightarrow{}  (\mforall{}p:partition(I).  \mforall{}x:partition-choice(full-partition(I;p)).  \mforall{}i:\mBbbN{}||p||  +  1.
                (x[i]  \mmember{}  \{x:\mBbbR{}|  x  \mmember{}  I\}  )))


By

---

Latex:
(InstLemma  `partition-choice-member`  []
  THEN  RepeatFor  4  ((ParallelLast'  THENA  Auto))
  THEN  NthHypSq  (-1)
  THEN  RepeatFor  2  (EqCD)
  THEN  Try  (Trivial))

---

Home Index