Nuprl Definition : omon
OMon == {g:AbMon| UniformLinorder(|g|;x,y.↑(x ≤b y)) ∧ (=b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|g| ⟶ |g| ⟶ 𝔹))}
Definitions occuring in Statement :
abmonoid: AbMon,
grp_le: ≤b,
grp_eq: =b,
grp_car: |g|,
ulinorder: UniformLinorder(T;x,y.R[x; y]),
band: p ∧b q,
assert: ↑b,
bool: 𝔹,
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,
and: P ∧ Q,
ulinorder: UniformLinorder(T;x,y.R[x; y]),
assert: ↑b,
equal: s = t ∈ T,
function: x:A ⟶ B[x],
grp_car: |g|,
bool: 𝔹,
grp_eq: =b,
lambda: λx.A[x],
band: p ∧b q,
infix_ap: x f y,
grp_le: ≤b
Latex:
OMon == \{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))))\}
Date html generated:
2016_05_15-PM-00_10_46
Last ObjectModification:
2015_09_23-AM-06_24_39
Theory : groups_1
Home
Index