---

Step * of Lemma ss-prod-prod

No Annotations
∀[X,Y,Z:SeparationSpace].  ss-homeo(X × Y × Z;X × Y × Z)
BY
{ (Auto
   THEN (Assert λt.let xy,z = t 
                   in let x,y = xy 
                      in <x, y, z> ∈ Point(X × Y × Z ⟶ X × Y × Z) BY
               ((RWW "ss-fun-point prod-ss-point" 0 THENA Auto)
                THEN MemTypeCD
                THEN Auto
                THEN D 0
                THEN Reduce 0
                THEN Auto
                THEN ((RWO "prod-ss-eq" (-1) THENA Auto) THEN (RWO "prod-ss-eq" 0 THENA Auto))
                THEN ∀h:hyp. ((RWO "prod-ss-point" h THENA Auto) THEN D h) 
                THEN All Reduce
                THEN (D -1 THEN (RWO "prod-ss-eq" (-2) THENA Auto) THEN (RWO "prod-ss-eq" 0 THENA Auto))
                THEN ∀h:hyp. ((RWO "prod-ss-point" h THENA Auto) THEN D h) 
                THEN All Reduce
                THEN Auto))
   THEN (Assert λt.let x,yz = t 
                   in let y,z = yz 
                      in <<x, y>, z> ∈ Point(X × Y × Z ⟶ X × Y × Z) BY
               ((RWW "ss-fun-point prod-ss-point" 0 THENA Auto)
                THEN MemTypeCD
                THEN Auto
                THEN D 0
                THEN Reduce 0
                THEN Auto
                THEN ((RWO "prod-ss-eq" (-1) THENA Auto) THEN (RWO "prod-ss-eq" 0 THENA Auto))
                THEN ∀h:hyp. ((RWO "prod-ss-point" h THENA Auto) THEN D h) 
                THEN All Reduce
                THEN D -1
                THEN ((RWO "prod-ss-eq" (-1) THENA Auto) THEN (RWO "prod-ss-eq" 0 THENA Auto))
                THEN ∀h:hyp. ((RWO "prod-ss-point" h THENA Auto) THEN D h) 
                THEN All Reduce
                THEN Auto))) }

1
1. [X] : SeparationSpace
2. [Y] : SeparationSpace
3. [Z] : SeparationSpace
4. λt.let xy,z = t 
      in let x,y = xy 
         in <x, y, z> ∈ Point(X × Y × Z ⟶ X × Y × Z)
5. λt.let x,yz = t 
      in let y,z = yz 
         in <<x, y>, z> ∈ Point(X × Y × Z ⟶ X × Y × Z)
⊢ ss-homeo(X × Y × Z;X × Y × Z)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,Y,Z:SeparationSpace].    ss-homeo(X  \mtimes{}  Y  \mtimes{}  Z;X  \mtimes{}  Y  \mtimes{}  Z)


By

---

Latex:
(Auto
  THEN  (Assert  \mlambda{}t.let  xy,z  =  t 
                                  in  let  x,y  =  xy 
                                        in  <x,  y,  z>  \mmember{}  Point(X  \mtimes{}  Y  \mtimes{}  Z  {}\mrightarrow{}  X  \mtimes{}  Y  \mtimes{}  Z)  BY
                          ((RWW  "ss-fun-point  prod-ss-point"  0  THENA  Auto)
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  D  0
                            THEN  Reduce  0
                            THEN  Auto
                            THEN  ((RWO  "prod-ss-eq"  (-1)  THENA  Auto)  THEN  (RWO  "prod-ss-eq"  0  THENA  Auto))
                            THEN  \mforall{}h:hyp.  ((RWO  "prod-ss-point"  h  THENA  Auto)  THEN  D  h) 
                            THEN  All  Reduce
                            THEN  (D  -1
                                        THEN  (RWO  "prod-ss-eq"  (-2)  THENA  Auto)
                                        THEN  (RWO  "prod-ss-eq"  0  THENA  Auto))
                            THEN  \mforall{}h:hyp.  ((RWO  "prod-ss-point"  h  THENA  Auto)  THEN  D  h) 
                            THEN  All  Reduce
                            THEN  Auto))
  THEN  (Assert  \mlambda{}t.let  x,yz  =  t 
                                  in  let  y,z  =  yz 
                                        in  <<x,  y>,  z>  \mmember{}  Point(X  \mtimes{}  Y  \mtimes{}  Z  {}\mrightarrow{}  X  \mtimes{}  Y  \mtimes{}  Z)  BY
                          ((RWW  "ss-fun-point  prod-ss-point"  0  THENA  Auto)
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  D  0
                            THEN  Reduce  0
                            THEN  Auto
                            THEN  ((RWO  "prod-ss-eq"  (-1)  THENA  Auto)  THEN  (RWO  "prod-ss-eq"  0  THENA  Auto))
                            THEN  \mforall{}h:hyp.  ((RWO  "prod-ss-point"  h  THENA  Auto)  THEN  D  h) 
                            THEN  All  Reduce
                            THEN  D  -1
                            THEN  ((RWO  "prod-ss-eq"  (-1)  THENA  Auto)  THEN  (RWO  "prod-ss-eq"  0  THENA  Auto))
                            THEN  \mforall{}h:hyp.  ((RWO  "prod-ss-point"  h  THENA  Auto)  THEN  D  h) 
                            THEN  All  Reduce
                            THEN  Auto)))

---

Home Index