---

Step * of Lemma nearby-partitions_functionality

∀p,q:ℝ List. ∀e1,e2:ℝ.  ((e1 ≤ e2) ⇒ {nearby-partitions(e1;p;q) ⇒ nearby-partitions(e2;p;q)})
BY
{ (Auto THEN (D 0 THENA Auto)) }

1
1. p : ℝ List
2. q : ℝ List
3. e1 : ℝ
4. e2 : ℝ
5. e1 ≤ e2
6. nearby-partitions(e1;p;q)
⊢ nearby-partitions(e2;p;q)

---

Latex:

---

Latex:
\mforall{}p,q:\mBbbR{}  List.  \mforall{}e1,e2:\mBbbR{}.    ((e1  \mleq{}  e2)  {}\mRightarrow{}  \{nearby-partitions(e1;p;q)  {}\mRightarrow{}  nearby-partitions(e2;p;q)\})


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto))

---

Home Index