---

Step * of Lemma strong-continuous-product

∀[F,G:Type ⟶ Type].  (Continuous+(T.F[T] × G[T])) supposing (Continuous+(T.G[T]) and Continuous+(T.F[T]))
BY
{ (Unfold `so_apply` 0
   THEN Auto
   THEN Repeat ((D 0 THEN Auto))
   THEN Try (Complete ((SubsumeC ⌜⋂n:ℕ. (F (X n))⌝⋅
                        THEN Try ((DoSubsume THEN Auto THEN BackThruSomeHyp')⋅)
                        THEN (D 0 THEN Auto)
                        THEN With ⌜n⌝ (D (-1))⋅
                        THEN Auto)))
   THEN Try (Complete ((SubsumeC ⌜⋂n:ℕ. (G (X n))⌝⋅
                        THEN Try ((DoSubsume THEN Auto THEN BackThruSomeHyp')⋅)
                        THEN (D 0 THEN Auto)
                        THEN With ⌜n⌝ (D (-1))⋅
                        THEN Auto)))) }

1
.....subterm..... T:t
1:n
1. F : Type ⟶ Type
2. G : Type ⟶ Type
3. Continuous+(T.F T)
4. Continuous+(T.G T)
5. X : ℕ ⟶ Type
6. x : ⋂n:ℕ. (F (X n) × (G (X n)))
⊢ x ∈ F (⋂n:ℕ. (X n)) × (G (⋂n:ℕ. (X n)))

---

Latex:

---

Latex:
\mforall{}[F,G:Type  {}\mrightarrow{}  Type].
    (Continuous+(T.F[T]  \mtimes{}  G[T]))  supposing  (Continuous+(T.G[T])  and  Continuous+(T.F[T]))


By

---

Latex:
(Unfold  `so\_apply`  0
  THEN  Auto
  THEN  Repeat  ((D  0  THEN  Auto))
  THEN  Try  (Complete  ((SubsumeC  \mkleeneopen{}\mcap{}n:\mBbbN{}.  (F  (X  n))\mkleeneclose{}\mcdot{}
                                            THEN  Try  ((DoSubsume  THEN  Auto  THEN  BackThruSomeHyp')\mcdot{})
                                            THEN  (D  0  THEN  Auto)
                                            THEN  With  \mkleeneopen{}n\mkleeneclose{}  (D  (-1))\mcdot{}
                                            THEN  Auto)))
  THEN  Try  (Complete  ((SubsumeC  \mkleeneopen{}\mcap{}n:\mBbbN{}.  (G  (X  n))\mkleeneclose{}\mcdot{}
                                            THEN  Try  ((DoSubsume  THEN  Auto  THEN  BackThruSomeHyp')\mcdot{})
                                            THEN  (D  0  THEN  Auto)
                                            THEN  With  \mkleeneopen{}n\mkleeneclose{}  (D  (-1))\mcdot{}
                                            THEN  Auto))))

---

Home Index