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