Nuprl Definition : inverse
(basic):: Inverse(T;op;id;inv) == ∀[x:T]. (((x op (inv x)) = id ∈ T) ∧ (((inv x) op x) = id ∈ T))
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
infix_ap: x f y,
and: P ∧ Q,
apply: f a,
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,
apply: f a
Latex:
(basic):: Inverse(T;op;id;inv) == \mforall{}[x:T]. (((x op (inv x)) = id) \mwedge{} (((inv x) op x) = id))
Date html generated:
2016_05_13-PM-04_08_56
Last ObjectModification:
2015_09_22-PM-05_45_54
Theory : fun_1
Home
Index