---

Step * of Lemma continuous'-monotone-product

∀[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 THENA Auto)
   THEN SubsumeC ⌜⋃n:ℕ.(F (X n)) × ⋃n:ℕ.(G (X n))⌝⋅
   THEN Auto
   THEN D 0
   THEN Auto
   THEN D (-1)
   THEN D_union (-2)
   THEN D_union (-1)
   THEN MemTypeCDUnion ⌜imax(n;n1)⌝⋅
   THEN (MemCD THENA Auto)
   THEN Try ((MemCD THEN DoSubsume THEN Try (Trivial) THEN BackThruSomeHyp))
   THEN Auto
   THEN BLemma `type-incr-chain-subtype`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[F,G:Type  {}\mrightarrow{}  Type].
    (continuous'-monotone\{i:l\}(T.F[T]  \mtimes{}  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  THENA  Auto)
  THEN  SubsumeC  \mkleeneopen{}\mcup{}n:\mBbbN{}.(F  (X  n))  \mtimes{}  \mcup{}n:\mBbbN{}.(G  (X  n))\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  D  (-1)
  THEN  D\_union  (-2)
  THEN  D\_union  (-1)
  THEN  MemTypeCDUnion  \mkleeneopen{}imax(n;n1)\mkleeneclose{}\mcdot{}
  THEN  (MemCD  THENA  Auto)
  THEN  Try  ((MemCD  THEN  DoSubsume  THEN  Try  (Trivial)  THEN  BackThruSomeHyp))
  THEN  Auto
  THEN  BLemma  `type-incr-chain-subtype`
  THEN  Auto)

---

Home Index