Nuprl Lemma : abmonoid_inc

AbMon ⊆AbMon{[i j]}


Proof




Definitions occuring in Statement :  abmonoid: AbMon subtype_rel: A ⊆B
Definitions unfolded in proof :  subtype_rel: A ⊆B member: t ∈ T abmonoid: AbMon mon: Mon uall: [x:A]. B[x] prop:
Lemmas referenced :  subtype_rel_grp monoid_p_wf grp_car_wf grp_op_wf grp_id_wf mon_wf comm_wf abmonoid_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaEquality sqequalHypSubstitution setElimination thin rename dependent_set_memberEquality cut hypothesisEquality applyEquality introduction extract_by_obid hypothesis sqequalRule instantiate isectElimination because_Cache

Latex:
AbMon  \msubseteq{}r  AbMon\{[i  |  j]\}



Date html generated: 2019_10_15-AM-10_32_36
Last ObjectModification: 2018_09_17-PM-06_25_24

Theory : groups_1


Home Index