---

Step * of Lemma continuous'-monotone-sum

∀[F,G:Type ⟶ Type].
  (continuous'-monotone{i:l}(T.F[T] + G[T])) supposing 
     (continuous'-monotone{i:l}(T.G[T]) and 
     continuous'-monotone{i:l}(T.F[T]))
BY
{ (RepUR ``so_apply continuous\'-monotone`` 0
   THEN Auto
   THEN All UnfoldTopAb
   THEN Auto
   THEN D 0
   THEN Auto
   THEN SubsumeC ⌜⋃n:ℕ.(F (X n)) + ⋃n:ℕ.(G (X n))⌝⋅
   THEN Auto
   THEN ((D 0 THEN Auto)
         THEN D (-1)
         THEN D_union (-1)
         THEN Unhide
         THEN (MemTypeCDUnion ⌜n⌝⋅ THEN Auto THEN DVar `X' THEN DoSubsume THEN Auto THEN BackThruSomeHyp)⋅)⋅) }

---

Latex:

---

Latex:
\mforall{}[F,G:Type  {}\mrightarrow{}  Type].
    (continuous'-monotone\{i:l\}(T.F[T]  +  G[T]))  supposing 
          (continuous'-monotone\{i:l\}(T.G[T])  and 
          continuous'-monotone\{i:l\}(T.F[T]))


By

---

Latex:
(RepUR  ``so\_apply  continuous\mbackslash{}'-monotone``  0
  THEN  Auto
  THEN  All  UnfoldTopAb
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  SubsumeC  \mkleeneopen{}\mcup{}n:\mBbbN{}.(F  (X  n))  +  \mcup{}n:\mBbbN{}.(G  (X  n))\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  ((D  0  THEN  Auto)
              THEN  D  (-1)
              THEN  D\_union  (-1)
              THEN  Unhide
              THEN  (MemTypeCDUnion  \mkleeneopen{}n\mkleeneclose{}\mcdot{}
                          THEN  Auto
                          THEN  DVar  `X'
                          THEN  DoSubsume
                          THEN  Auto
                          THEN  BackThruSomeHyp)\mcdot{})\mcdot{})

---

Home Index