Nuprl Lemma : grp_car_subtype
|(<ℤ+>↓hgrp)| ⊆r ℕ
Proof
Definitions occuring in Statement :
int_add_grp: <ℤ+>,
hgrp_of_ocgrp: g↓hgrp,
grp_car: |g|,
nat: ℕ,
subtype_rel: A ⊆r B
Definitions unfolded in proof :
subtype_rel: A ⊆r B,
member: t ∈ T,
nat: ℕ,
hgrp_of_ocgrp: g↓hgrp,
grp_car: |g|,
pi1: fst(t),
hgrp_car: |g|+,
int_add_grp: <ℤ+>,
uall: ∀[x:A]. B[x],
prop: ℙ
Lemmas referenced :
grp_car_wf,
hgrp_of_ocgrp_wf,
int_add_grp_wf2,
zero-le-nat,
grp_car_inc,
le_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaEquality,
dependent_set_memberEquality,
cut,
hypothesisEquality,
applyEquality,
thin,
sqequalHypSubstitution,
sqequalRule,
setElimination,
rename,
introduction,
extract_by_obid,
isectElimination,
hypothesis,
natural_numberEquality
Latex:
|(<\mBbbZ{}+>\mdownarrow{}hgrp)| \msubseteq{}r \mBbbN{}
Date html generated:
2019_10_15-AM-10_33_18
Last ObjectModification:
2018_09_18-PM-00_38_49
Theory : groups_1
Home
Index