---

Step * of Lemma compose_increasing

∀[k,m:ℕ]. ∀[f:ℕk ⟶ ℕm]. ∀[g:ℕm ⟶ ℤ].  (increasing(g o f;k)) supposing (increasing(g;m) and increasing(f;k))
BY
{ ((Auto THEN D 0) THEN Reduce 0 THEN Auto THEN FLemma `increasing_implies` [-2] THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k,m:\mBbbN{}].  \mforall{}[f:\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}m].  \mforall{}[g:\mBbbN{}m  {}\mrightarrow{}  \mBbbZ{}].
    (increasing(g  o  f;k))  supposing  (increasing(g;m)  and  increasing(f;k))


By

---

Latex:
((Auto  THEN  D  0)  THEN  Reduce  0  THEN  Auto  THEN  FLemma  `increasing\_implies`  [-2]  THEN  Auto)

---

Home Index