Nuprl Lemma : qadd_grp_wf2
<ℚ+> ∈ OGrp
Proof
Definitions occuring in Statement :
qadd_grp: <ℚ+>,
member: t ∈ T,
ocgrp: OGrp
Definitions unfolded in proof :
prop: ℙ,
mon: Mon,
abmonoid: AbMon,
ocmon: OCMon,
uall: ∀[x:A]. B[x],
ocgrp: OGrp,
member: t ∈ T,
so_apply: x[s],
so_lambda: λ2x.t[x],
bfalse: ff,
uimplies: b supposing a,
uiff: uiff(P;Q),
ifthenelse: if b then t else f fi ,
band: p ∧b q,
btrue: tt,
it: ⋅,
unit: Unit,
bool: 𝔹,
implies: P ⇒ Q,
all: ∀x:A. B[x],
infix_ap: x f y,
so_apply: x[s1;s2],
so_lambda: λ2x y.t[x; y],
and: P ∧ Q,
grp: Group{i},
abgrp: AbGrp,
subtype_rel: A ⊆r B,
monot: monot(T;x,y.R[x; y];f),
grp_op: *,
grp_eq: =b,
pi2: snd(t),
grp_le: ≤b,
pi1: fst(t),
grp_car: |g|,
qadd_grp: <ℚ+>,
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
connex: Connex(T;x,y.R[x; y]),
uanti_sym: UniformlyAntiSym(T;x,y.R[x; y]),
utrans: UniformlyTrans(T;x,y.E[x; y]),
urefl: UniformlyRefl(T;x,y.E[x; y]),
uorder: UniformOrder(T;x,y.R[x; y]),
ulinorder: UniformLinorder(T;x,y.R[x; y]),
or: P ∨ Q,
guard: {T},
true: True,
squash: ↓T,
false: False,
not: ¬A,
qsub: r - s,
bnot: ¬bb,
sq_type: SQType(T),
exists: ∃x:A. B[x],
rev_uimplies: rev_uimplies(P;Q),
assert: ↑b,
cancel: Cancel(T;S;op),
inverse: Inverse(T;op;id;inv),
grp_inv: ~,
grp_id: e,
cand: A c∧ B
Lemmas referenced :
grp_inv_wf,
grp_id_wf,
grp_op_wf,
grp_car_wf,
inverse_wf,
monot_wf,
uall_wf,
cancel_wf,
eqtt_to_assert,
grp_eq_wf,
equal_wf,
grp_le_wf,
bool_wf,
infix_ap_wf,
assert_wf,
ulinorder_wf,
set_wf,
comm_wf,
mon_wf,
subtype_rel_sets,
qadd_grp_wf,
rationals_wf,
qadd_wf,
q_le_wf,
assert_witness,
q_le-elim,
assert-qeq,
assert_of_bor,
iff_weakening_uiff,
iff_transitivity,
or_wf,
qeq_wf2,
int-subtype-rationals,
qmul_wf,
qpositive_wf,
bor_wf,
true_wf,
squash_wf,
qadd_positive,
iff_weakening_equal,
qadd_inv_assoc_q,
qadd_ac_1_q,
qadd_comm_q,
mon_assoc_q,
qinv_inv_q,
qinv_thru_op_q,
qminus_positive,
qsub_wf,
q_trichotomy,
qadd_ident,
band_wf,
iff_imp_equal_bool,
iff_wf,
assert_of_band,
assert-bnot,
bool_subtype_base,
subtype_base_sq,
bool_cases_sqequal,
eqff_to_assert,
btrue_wf,
bfalse_wf,
assert_functionality_wrt_uiff,
mon_ident_q,
qinverse_q,
subtype_rel_self,
istype-universe,
istype-assert,
qadd_minus,
qadd_com
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_functionElimination,
dependent_functionElimination,
equalitySymmetry,
equalityTransitivity,
independent_isectElimination,
productElimination,
equalityElimination,
unionElimination,
lambdaFormation,
functionEquality,
lambdaEquality,
sqequalRule,
productEquality,
cumulativity,
setEquality,
instantiate,
applyEquality,
isect_memberFormation,
independent_pairFormation,
addLevel,
orFunctionality,
axiomEquality,
isect_memberEquality,
natural_numberEquality,
minusEquality,
inrFormation,
inlFormation,
baseClosed,
imageMemberEquality,
imageElimination,
hyp_replacement,
universeEquality,
applyLambdaEquality,
voidElimination,
impliesFunctionality,
promote_hyp,
dependent_pairFormation,
inhabitedIsType,
universeIsType,
lambdaEquality_alt,
isectIsTypeImplies,
isect_memberEquality_alt,
equalityIstype,
isect_memberFormation_alt,
lambdaFormation_alt,
unionEquality,
unionIsType,
inlFormation_alt,
inrFormation_alt,
independent_pairEquality
Latex:
<\mBbbQ{}+> \mmember{} OGrp
Date html generated:
2020_05_20-AM-09_14_19
Last ObjectModification:
2020_01_25-AM-09_30_28
Theory : rationals
Home
Index