Nuprl Definition : permutation-ss

permutation-ss(ss) ==
  set-ss(Point ⟶ ss × Point ⟶ ss;fg.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)))


Definitions occuring in Statement :  set-ss: set-ss(ss;x.P[x]),  prod-ss: ss1 × ss2,  fun-ss: A ⟶ ss,  ss-eq: x ≡ y,  ss-sep: x # y,  ss-point: Point,  all: ∀x:A. B[x],  implies: P ⇒ Q,  and: P ∧ Q,  apply: f a,  spread: spread def
Definitions occuring in definition :  set-ss: set-ss(ss;x.P[x]),  prod-ss: ss1 × ss2,  fun-ss: A ⟶ ss,  spread: spread def,  ss-eq: x ≡ y,  and: P ∧ Q,  all: ∀x:A. B[x],  ss-point: Point,  implies: P ⇒ Q,  apply: f a,  ss-sep: x # y
FDL editor aliases :  permutation-ss
Latex:
permutation-ss(ss)  ==
    set-ss(Point  {}\mrightarrow{}  ss  \mtimes{}  Point  {}\mrightarrow{}  ss;fg.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)))


Date html generated: 2017_10_02-PM-03_25_14
Last ObjectModification: 2017_06_22-PM-04_41_58

Theory : constructive!algebra


Home Index