---

Step * of Lemma continuous-monotone-function

∀[F:Type ⟶ Type]. ∀[A:Type]. ContinuousMonotone(T.A ⟶ F[T]) supposing ContinuousMonotone(T.F[T])
BY
{ (Auto THEN BLemma `continuous-monotone-depfunction` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type].  \mforall{}[A:Type].  ContinuousMonotone(T.A  {}\mrightarrow{}  F[T])  supposing  ContinuousMonotone(T.F[T])


By

---

Latex:
(Auto  THEN  BLemma  `continuous-monotone-depfunction`  THEN  Auto)

---

Home Index