Nuprl Definition : ocmon
OCMon ==
{g:AbMon|
(UniformLinorder(|g|;x,y.↑(x ≤b y)) ∧ (=b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|g| ⟶ |g| ⟶ 𝔹)))
∧ Cancel(|g|;|g|;*)
∧ (∀[z:|g|]. monot(|g|;x,y.↑(x ≤b y);λw.(z * w)))}
Definitions occuring in Statement :
abmonoid: AbMon
,
grp_op: *
,
grp_le: ≤b
,
grp_eq: =b
,
grp_car: |g|
,
monot: monot(T;x,y.R[x; y];f)
,
cancel: Cancel(T;S;op)
,
ulinorder: UniformLinorder(T;x,y.R[x; y])
,
band: p ∧b q
,
assert: ↑b
,
bool: 𝔹
,
uall: ∀[x:A]. B[x]
,
infix_ap: x f y
,
and: P ∧ Q
,
set: {x:A| B[x]}
,
lambda: λx.A[x]
,
function: x:A ⟶ B[x]
,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]}
,
abmonoid: AbMon
,
ulinorder: UniformLinorder(T;x,y.R[x; y])
,
equal: s = t ∈ T
,
function: x:A ⟶ B[x]
,
bool: 𝔹
,
grp_eq: =b
,
band: p ∧b q
,
and: P ∧ Q
,
cancel: Cancel(T;S;op)
,
uall: ∀[x:A]. B[x]
,
monot: monot(T;x,y.R[x; y];f)
,
grp_car: |g|
,
assert: ↑b
,
grp_le: ≤b
,
lambda: λx.A[x]
,
infix_ap: x f y
,
grp_op: *
Latex:
OCMon ==
\{g:AbMon|
(UniformLinorder(|g|;x,y.\muparrow{}(x \mleq{}\msubb{} y)) \mwedge{} (=\msubb{} = (\mlambda{}x,y. ((x \mleq{}\msubb{} y) \mwedge{}\msubb{} (y \mleq{}\msubb{} x)))))
\mwedge{} Cancel(|g|;|g|;*)
\mwedge{} (\mforall{}[z:|g|]. monot(|g|;x,y.\muparrow{}(x \mleq{}\msubb{} y);\mlambda{}w.(z * w)))\}
Date html generated:
2016_05_15-PM-00_11_03
Last ObjectModification:
2015_09_23-AM-06_24_40
Theory : groups_1
Home
Index