---

Step * of Lemma continuous'-monotone-constant

∀[A:Type]. continuous'-monotone{i:l}(T.A)
BY
{ (RepUR ``so_apply continuous\'-monotone`` 0
   THEN Auto
   THEN All UnfoldTopAb
   THEN Auto
   THEN D 0
   THEN Auto
   THEN MemTypeCDUnion ⌜0⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  continuous'-monotone\{i:l\}(T.A)


By

---

Latex:
(RepUR  ``so\_apply  continuous\mbackslash{}'-monotone``  0
  THEN  Auto
  THEN  All  UnfoldTopAb
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  MemTypeCDUnion  \mkleeneopen{}0\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index