Nuprl Lemma : ocgrp_subtype_abgrp
OGrp ⊆r AbGrp
Proof
Definitions occuring in Statement :
ocgrp: OGrp,
abgrp: AbGrp,
subtype_rel: A ⊆r B
Definitions unfolded in proof :
subtype_rel: A ⊆r B,
member: t ∈ T,
ocgrp: OGrp,
ocmon: OCMon,
abmonoid: AbMon,
abgrp: AbGrp,
grp: Group{i},
uall: ∀[x:A]. B[x],
mon: Mon,
prop: ℙ,
and: P ∧ Q,
so_lambda: λ2x y.t[x; y],
infix_ap: x f y,
so_apply: x[s1;s2],
all: ∀x:A. B[x],
or: P ∨ Q,
uimplies: b supposing a,
sq_type: SQType(T),
implies: P ⇒ Q,
guard: {T},
uiff: uiff(P;Q),
bfalse: ff,
band: p ∧b q,
ifthenelse: if b then t else f fi ,
so_lambda: λ2x.t[x],
so_apply: x[s],
sq_stable: SqStable(P),
squash: ↓T
Lemmas referenced :
subtype_rel_sets,
mon_wf,
comm_wf,
grp_car_wf,
grp_op_wf,
ulinorder_wf,
assert_wf,
grp_le_wf,
equal_wf,
bool_wf,
grp_eq_wf,
bool_cases,
subtype_base_sq,
bool_subtype_base,
eqtt_to_assert,
band_wf,
btrue_wf,
bfalse_wf,
cancel_wf,
monot_wf,
inverse_wf,
grp_id_wf,
grp_inv_wf,
sq_stable__comm,
ocgrp_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaEquality_alt,
cut,
hypothesisEquality,
applyEquality,
thin,
sqequalRule,
instantiate,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
setEquality,
hypothesis,
cumulativity,
setElimination,
rename,
because_Cache,
productEquality,
inhabitedIsType,
universeIsType,
functionEquality,
dependent_functionElimination,
unionElimination,
independent_isectElimination,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination,
productElimination,
isectEquality,
setIsType,
productIsType,
equalityIstype,
functionIsType,
isectIsType,
lambdaFormation_alt,
imageMemberEquality,
baseClosed,
imageElimination
Latex:
OGrp \msubseteq{}r AbGrp
Date html generated:
2020_05_19-PM-10_07_51
Last ObjectModification:
2020_01_08-PM-05_59_42
Theory : groups_1
Home
Index