Nuprl Lemma : oal_grp_wf2
∀s:LOSet. ∀g:OGrp. (oal_grp(s;g) ∈ OGrp)
Proof
Definitions occuring in Statement :
oal_grp: oal_grp(s;g),
all: ∀x:A. B[x],
member: t ∈ T,
ocgrp: OGrp,
loset: LOSet
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
subtype_rel: A ⊆r B,
ocgrp: OGrp,
uall: ∀[x:A]. B[x],
ocmon: OCMon,
abmonoid: AbMon,
mon: Mon,
prop: ℙ,
squash: ↓T,
omon: OMon,
and: P ∧ Q,
grp: Group{i},
abgrp: AbGrp,
guard: {T},
uimplies: b supposing a,
cancel: Cancel(T;S;op),
dmon: DMon,
abdmonoid: AbDMon,
grp_leq: a ≤ b,
dset: DSet,
dset_of_mon: g↓set,
set_prod: s × t,
dset_list: s List,
set_car: |p|,
mk_dset: mk_dset(T, eq),
dset_set: dset_set,
oalist: oal(a;b),
implies: P ⇒ Q,
infix_ap: x f y,
pi2: snd(t),
grp_op: *,
pi1: fst(t),
grp_car: |g|,
oal_grp: oal_grp(s;g),
monot: monot(T;x,y.R[x; y];f),
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
so_apply: x[s],
so_lambda: λ2x.t[x],
bfalse: ff,
uiff: uiff(P;Q),
ifthenelse: if b then t else f fi ,
band: p ∧b q,
btrue: tt,
it: ⋅,
unit: Unit,
bool: 𝔹,
so_apply: x[s1;s2],
so_lambda: λ2x y.t[x; y]
Lemmas referenced :
ocgrp_wf,
loset_wf,
oal_grp_wf,
ocgrp_subtype_abdgrp,
abdgrp_subtype_abgrp,
oal_grp_wf1,
inverse_wf,
grp_car_wf,
grp_op_wf,
grp_id_wf,
grp_inv_wf,
infix_ap_wf,
equal_wf,
igrp_wf,
grp_wf,
abgrp_wf,
subtype_rel_transitivity,
abgrp_subtype_grp,
grp_subtype_igrp,
grp_op_cancel_l,
comm_wf,
dmon_wf,
abdmonoid_wf,
ocmon_wf,
ocgrp_subtype_ocmon,
ocmon_subtype_abdmonoid,
abdmonoid_dmon,
abmonoid_properties,
ocmon_properties,
ocgrp_properties,
omon_lt_mono_imp_leq_mono,
dset_wf,
oalist_wf,
set_car_wf,
grp_lt_wf,
oal_merge_wf2,
oal_lt_iff_grp_lt,
oal_merge_preserves_lt,
monot_wf,
uall_wf,
cancel_wf,
eqtt_to_assert,
grp_eq_wf,
grp_le_wf,
bool_wf,
assert_wf,
ulinorder_wf,
grp_properties,
abgrp_properties
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalHypSubstitution,
hypothesis,
introduction,
extract_by_obid,
dependent_functionElimination,
thin,
hypothesisEquality,
applyEquality,
sqequalRule,
dependent_set_memberEquality,
isectElimination,
setElimination,
rename,
because_Cache,
imageElimination,
baseClosed,
imageMemberEquality,
applyLambdaEquality,
equalitySymmetry,
equalityTransitivity,
independent_pairFormation,
axiomEquality,
isect_memberEquality,
lambdaEquality,
independent_isectElimination,
instantiate,
productElimination,
isect_memberFormation,
independent_functionElimination,
equalityElimination,
unionElimination,
functionEquality,
productEquality
Latex:
\mforall{}s:LOSet. \mforall{}g:OGrp. (oal\_grp(s;g) \mmember{} OGrp)
Date html generated:
2019_10_16-PM-01_08_49
Last ObjectModification:
2018_08_22-AM-11_53_49
Theory : polynom_2
Home
Index