---

Step * of Lemma permutation-ss-point

∀[rv:Top]
  (Point ~ {fg:Point ⟶ Point × (Point ⟶ Point)| 
            let f,g = fg 
            in (∀x:Point. f (g x) ≡ x)
               ∧ (∀x:Point. g (f x) ≡ x)
               ∧ (∀x,y:Point.  (f x # f y ⇒ x # y))
               ∧ (∀x,y:Point.  (g x # g y ⇒ x # y))} )
BY
{ ((RepUR ``ss-point permutation-ss set-ss mk-ss`` 0 THEN Auto)
   THEN (RepUR ``prod-ss mk-ss`` 0 THEN Auto)
   THEN RepUR ``fun-ss mk-ss ss-point`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[rv:Top]
    (Point  \msim{}  \{fg:Point  {}\mrightarrow{}  Point  \mtimes{}  (Point  {}\mrightarrow{}  Point)| 
                        let  f,g  =  fg 
                        in  (\mforall{}x:Point.  f  (g  x)  \mequiv{}  x)
                              \mwedge{}  (\mforall{}x:Point.  g  (f  x)  \mequiv{}  x)
                              \mwedge{}  (\mforall{}x,y:Point.    (f  x  \#  f  y  {}\mRightarrow{}  x  \#  y))
                              \mwedge{}  (\mforall{}x,y:Point.    (g  x  \#  g  y  {}\mRightarrow{}  x  \#  y))\}  )


By

---

Latex:
((RepUR  ``ss-point  permutation-ss  set-ss  mk-ss``  0  THEN  Auto)
  THEN  (RepUR  ``prod-ss  mk-ss``  0  THEN  Auto)
  THEN  RepUR  ``fun-ss  mk-ss  ss-point``  0
  THEN  Auto)

---

Home Index