---

Step * 1 of Lemma ss-prod-prod


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)
BY
{ ((D 0 With ⌜λt.let xy,z = t in let x,y = xy in <x, y, z>⌝  THEN Auto)
   THEN D 0 With ⌜λt.let x,yz = t 
                     in let y,z = yz 
                        in <<x, y>, z>⌝ 
   THEN Auto
   THEN (RWW "prod-ss-point" (-1) THENA Auto)
   THEN DProds
   THEN RepUR ``ss-ap`` 0
   THEN RWW  "prod-ss-eq" 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  [X]  :  SeparationSpace
2.  [Y]  :  SeparationSpace
3.  [Z]  :  SeparationSpace
4.  \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)
5.  \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)
\mvdash{}  ss-homeo(X  \mtimes{}  Y  \mtimes{}  Z;X  \mtimes{}  Y  \mtimes{}  Z)


By

---

Latex:
((D  0  With  \mkleeneopen{}\mlambda{}t.let  xy,z  =  t  in  let  x,y  =  xy  in  <x,  y,  z>\mkleeneclose{}    THEN  Auto)
  THEN  D  0  With  \mkleeneopen{}\mlambda{}t.let  x,yz  =  t 
                                      in  let  y,z  =  yz 
                                            in  <<x,  y>,  z>\mkleeneclose{} 
  THEN  Auto
  THEN  (RWW  "prod-ss-point"  (-1)  THENA  Auto)
  THEN  DProds
  THEN  RepUR  ``ss-ap``  0
  THEN  RWW    "prod-ss-eq"  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index