---

Step * of Lemma uniform-partition-increasing

∀a,b:ℝ.  ((a < b) ⇒ (∀k:ℕ+. frs-increasing(uniform-partition([a, b];k))))
BY
{ (Auto THEN (Assert icompact([a, b]) BY EAuto 1)) }

1
1. a : ℝ
2. b : ℝ
3. a < b
4. k : ℕ+
5. icompact([a, b])
⊢ frs-increasing(uniform-partition([a, b];k))

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.    ((a  <  b)  {}\mRightarrow{}  (\mforall{}k:\mBbbN{}\msupplus{}.  frs-increasing(uniform-partition([a,  b];k))))


By

---

Latex:
(Auto  THEN  (Assert  icompact([a,  b])  BY  EAuto  1))

---

Home Index