Nuprl Lemma : abgrp_subtype_grp

AbGrp ⊆Group{i}


Proof




Definitions occuring in Statement :  abgrp: AbGrp grp: Group{i} subtype_rel: A ⊆B
Definitions unfolded in proof :  subtype_rel: A ⊆B member: t ∈ T abgrp: AbGrp
Lemmas referenced :  abgrp_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaEquality sqequalHypSubstitution setElimination thin rename hypothesisEquality cut lemma_by_obid hypothesis

Latex:
AbGrp  \msubseteq{}r  Group\{i\}



Date html generated: 2016_05_15-PM-00_09_33
Last ObjectModification: 2015_12_26-PM-11_45_21

Theory : groups_1


Home Index