Nuprl Lemma : abmonoid_properties

[g:AbMon]. Comm(|g|;*)


Proof




Definitions occuring in Statement :  abmonoid: AbMon grp_op: * grp_car: |g| comm: Comm(T;op) uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T abmonoid: AbMon mon: Mon sq_stable: SqStable(P) implies:  Q squash: T comm: Comm(T;op)
Lemmas referenced :  abmonoid_wf grp_op_wf grp_car_wf sq_stable__comm
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution setElimination thin rename lemma_by_obid isectElimination hypothesisEquality hypothesis independent_functionElimination sqequalRule imageMemberEquality baseClosed imageElimination isect_memberEquality axiomEquality

Latex:
\mforall{}[g:AbMon].  Comm(|g|;*)



Date html generated: 2016_05_15-PM-00_07_36
Last ObjectModification: 2016_01_15-PM-11_06_22

Theory : groups_1


Home Index