Nuprl Lemma : qadd_grp_wf
<ℚ+> ∈ AbGrp
Proof
Definitions occuring in Statement :
qadd_grp: <ℚ+>,
member: t ∈ T,
abgrp: AbGrp
Definitions unfolded in proof :
prop: ℙ,
mon: Mon,
grp: Group{i},
uall: ∀[x:A]. B[x],
abgrp: AbGrp,
member: t ∈ T,
qadd_grp: <ℚ+>,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
assoc: Assoc(T;op),
infix_ap: x f y,
ident: Ident(T;op;id),
and: P ∧ Q,
cand: A c∧ B,
squash: ↓T,
true: True,
guard: {T},
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
implies: P ⇒ Q,
inverse: Inverse(T;op;id;inv),
comm: Comm(T;op),
grp_car: |g|,
pi1: fst(t),
grp_op: *,
pi2: snd(t)
Lemmas referenced :
grp_op_wf,
grp_car_wf,
comm_wf,
qmul_wf,
int-subtype-rationals,
qadd_wf,
q_le_wf,
qeq_wf2,
rationals_wf,
mk_grp,
qadd_assoc,
equal_wf,
qadd_com,
iff_weakening_equal,
qadd_ident,
qadd_minus,
squash_wf,
true_wf,
istype-universe,
subtype_rel_self
Rules used in proof :
because_Cache,
hypothesis,
hypothesisEquality,
rename,
setElimination,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
dependent_set_memberEquality,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
independent_isectElimination,
minusEquality,
sqequalRule,
applyEquality,
natural_numberEquality,
lambdaEquality,
isect_memberFormation_alt,
equalitySymmetry,
inhabitedIsType,
isect_memberEquality_alt,
axiomEquality,
isectIsTypeImplies,
universeIsType,
lambdaEquality_alt,
imageElimination,
closedConclusion,
imageMemberEquality,
baseClosed,
equalityTransitivity,
productElimination,
independent_functionElimination,
independent_pairFormation,
independent_pairEquality,
instantiate,
universeEquality
Latex:
<\mBbbQ{}+> \mmember{} AbGrp
Date html generated:
2020_05_20-AM-09_13_39
Last ObjectModification:
2020_01_17-AM-11_08_27
Theory : rationals
Home
Index