Nuprl Definition : s-group-structure
s-GroupStructure ==
SeparationSpace
"id":Point
"inv":Point ⟶ Point
"op":Point ⟶ Point ⟶ Point
"opsep":∀x,x',y,y':Point. (self."op" x y # self."op" x' y' ⇒ (x # x' ∨ y # y'))
"invsep":∀x,y:Point. (self."inv" x # self."inv" y ⇒ x # y)
Definitions occuring in Statement :
ss-sep: x # y,
ss-point: Point,
separation-space: SeparationSpace,
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
apply: f a,
function: x:A ⟶ B[x],
token: "$token",
record-select: r.x,
record+: record+
Definitions occuring in definition :
record+: record+,
separation-space: SeparationSpace,
function: x:A ⟶ B[x],
or: P ∨ Q,
all: ∀x:A. B[x],
ss-point: Point,
implies: P ⇒ Q,
apply: f a,
record-select: r.x,
token: "$token",
ss-sep: x # y
FDL editor aliases :
s-group-structure
Latex:
s-GroupStructure ==
SeparationSpace
"id":Point
"inv":Point {}\mrightarrow{} Point
"op":Point {}\mrightarrow{} Point {}\mrightarrow{} Point
"opsep":\mforall{}x,x',y,y':Point. (self."op" x y \# self."op" x' y' {}\mRightarrow{} (x \# x' \mvee{} y \# y'))
"invsep":\mforall{}x,y:Point. (self."inv" x \# self."inv" y {}\mRightarrow{} x \# y)
Date html generated:
2017_10_02-PM-03_24_25
Last ObjectModification:
2017_06_23-AM-11_08_26
Theory : constructive!algebra
Home
Index