Nuprl Definition : sg-action
sg-action(g;n) ==
{a:Point ⟶ Point ⟶ Point| (∀x:Point. ∀f,h:Point. a f (a h x) ≡ a (f h) x) ∧ (∀x:Point. a 1 x ≡ x)}
Definitions occuring in Statement :
sg-op: (x y),
sg-id: 1,
ss-eq: x ≡ y,
ss-point: Point,
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x]
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
and: P ∧ Q,
sg-op: (x y),
all: ∀x:A. B[x],
ss-point: Point,
ss-eq: x ≡ y,
apply: f a,
sg-id: 1
FDL editor aliases :
sg-action
Latex:
sg-action(g;n) ==
\{a:Point {}\mrightarrow{} Point {}\mrightarrow{} Point|
(\mforall{}x:Point. \mforall{}f,h:Point. a f (a h x) \mequiv{} a (f h) x) \mwedge{} (\mforall{}x:Point. a 1 x \mequiv{} x)\}
Date html generated:
2017_10_02-PM-03_25_29
Last ObjectModification:
2017_07_03-PM-01_49_02
Theory : constructive!algebra
Home
Index