Nuprl Definition : ident
(basic):: Ident(T;op;id) == ∀[x:T]. (((x op id) = x ∈ T) ∧ ((id op x) = x ∈ T))
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
infix_ap: x f y,
and: P ∧ Q,
equal: s = t ∈ T
Definitions occuring in definition :
uall: ∀[x:A]. B[x],
and: P ∧ Q,
equal: s = t ∈ T,
infix_ap: x f y
Latex:
(basic):: Ident(T;op;id) == \mforall{}[x:T]. (((x op id) = x) \mwedge{} ((id op x) = x))
Date html generated:
2016_05_15-PM-00_02_12
Last ObjectModification:
2015_09_23-AM-06_23_45
Theory : gen_algebra_1
Home
Index