---

Step * 1 2 2 2 of Lemma nearby-partition-choice


1. I : Interval@i
2. icompact(I)
3. p : partition(I)@i
4. q : partition(I)@i
5. e : {e:ℝ| r0 < e} @i
6. nearby-partitions(e;p;q)
7. x : partition-choice(full-partition(I;p))@i
8. nearby-partitions(e;full-partition(I;p);full-partition(I;q))
9. frs-non-dec(full-partition(I;p)) ∧ frs-non-dec(full-partition(I;q))
⊢ ∃y:partition-choice(full-partition(I;q)). ∀i:ℕ||full-partition(I;p)|| - 1. (|x[i] - y[i]| ≤ e)
BY
{ (RepeatFor 3 (MoveToConcl (-1))
   THEN (GenConcl ⌜full-partition(I;p) = P ∈ (ℝ List)⌝⋅ THENA Auto)
   THEN (GenConcl ⌜full-partition(I;q) = Q ∈ (ℝ List)⌝⋅ THENA Auto)
   THEN RepUR ``partition-choice-ap`` 0
   THEN All Thin
   THEN RepUR ``partition-choice nearby-partitions`` 0
   THEN Auto
   THEN Subst' ||Q|| ~ ||P|| 0
   THEN Auto) }

1
1. e : {e:ℝ| r0 < e} @i
2. P : ℝ List@i
3. Q : ℝ List@i
4. x : i:ℕ||P|| - 1 ⟶ {x:ℝ| (P[i] ≤ x) ∧ (x ≤ P[i + 1])} @i
5. ||P|| = ||Q|| ∈ ℤ
6. ∀i:ℕ||P||. (|P[i] - Q[i]| ≤ e)
7. frs-non-dec(P)
8. frs-non-dec(Q)
⊢ ∃y:i:ℕ||P|| - 1 ⟶ {x:ℝ| (Q[i] ≤ x) ∧ (x ≤ Q[i + 1])} . ∀i:ℕ||P|| - 1. (|(x i) - y i| ≤ e)

---

Latex:

---

Latex:

1.  I  :  Interval@i
2.  icompact(I)
3.  p  :  partition(I)@i
4.  q  :  partition(I)@i
5.  e  :  \{e:\mBbbR{}|  r0  <  e\}  @i
6.  nearby-partitions(e;p;q)
7.  x  :  partition-choice(full-partition(I;p))@i
8.  nearby-partitions(e;full-partition(I;p);full-partition(I;q))
9.  frs-non-dec(full-partition(I;p))  \mwedge{}  frs-non-dec(full-partition(I;q))
\mvdash{}  \mexists{}y:partition-choice(full-partition(I;q)).  \mforall{}i:\mBbbN{}||full-partition(I;p)||  -  1.  (|x[i]  -  y[i]|  \mleq{}  e)


By

---

Latex:
(RepeatFor  3  (MoveToConcl  (-1))
  THEN  (GenConcl  \mkleeneopen{}full-partition(I;p)  =  P\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}full-partition(I;q)  =  Q\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepUR  ``partition-choice-ap``  0
  THEN  All  Thin
  THEN  RepUR  ``partition-choice  nearby-partitions``  0
  THEN  Auto
  THEN  Subst'  ||Q||  \msim{}  ||P||  0
  THEN  Auto)

---

Home Index