---

Step * of Lemma frs-increasing-sorted-by

∀[p:ℝ List]. (frs-increasing(p) ⇐⇒ sorted-by(λx,y. (x < y);p))
BY
{ (RepUR ``frs-increasing sorted-by`` 0 THEN Auto THEN BackThruSomeHyp THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p:\mBbbR{}  List].  (frs-increasing(p)  \mLeftarrow{}{}\mRightarrow{}  sorted-by(\mlambda{}x,y.  (x  <  y);p))


By

---

Latex:
(RepUR  ``frs-increasing  sorted-by``  0  THEN  Auto  THEN  BackThruSomeHyp  THEN  Auto)

---

Home Index