---

Step * of Lemma rv-perm-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 ``rv-permutation-group permutation-s-group ss-point mk-s-group`` 0
   THEN Fold `ss-point` 0
   THEN RWO "permutation-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  ``rv-permutation-group  permutation-s-group  ss-point  mk-s-group``  0
  THEN  Fold  `ss-point`  0
  THEN  RWO  "permutation-ss-point"  0
  THEN  Auto)

---

Home Index