Nuprl Lemma : mk-s-subgroup_wf
∀[sg:s-Group]. ∀[P:Point ⟶ ℙ]. mk-s-subgroup(sg;x.P[x]) ∈ s-Group supposing sg-subgroup(sg;x.P[x])
Proof
Definitions occuring in Statement :
mk-s-subgroup: mk-s-subgroup(sg;x.P[x]),
sg-subgroup: sg-subgroup(sg;x.P[x]),
s-group: s-Group,
ss-point: Point,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
member: t ∈ T,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
sg-inv: x^-1,
sg-op: (x y),
or: P ∨ Q,
guard: {T},
btrue: tt,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
record-select: r.x,
record+: record+,
s-group: s-Group,
cand: A c∧ B,
implies: P ⇒ Q,
all: ∀x:A. B[x],
subtype_rel: A ⊆r B,
prop: ℙ,
so_apply: x[s],
so_lambda: λ2x.t[x],
top: Top,
mk-s-subgroup: mk-s-subgroup(sg;x.P[x]),
and: P ∧ Q,
sg-subgroup: sg-subgroup(sg;x.P[x]),
uimplies: b supposing a,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
subtype_rel_dep_function,
or_wf,
ss-sep_wf,
subtype_rel_self,
ss-eq_wf,
all_wf,
sg-op-inv,
sg-op-id,
set_wf,
sg-assoc,
sg-op_wf,
sg-inv_wf,
sg-id_wf,
set-ss_wf,
set-ss-sep,
set-ss-eq,
s-group_wf,
s-group_subtype1,
ss-point_wf,
sg-subgroup_wf,
set-ss-point,
mk-s-group_wf
Rules used in proof :
independent_isectElimination,
tokenEquality,
dependentIntersectionEqElimination,
dependentIntersectionElimination,
productEquality,
independent_pairFormation,
lambdaFormation,
setEquality,
independent_functionElimination,
dependent_functionElimination,
rename,
setElimination,
dependent_set_memberEquality,
universeEquality,
cumulativity,
functionEquality,
functionExtensionality,
applyEquality,
lambdaEquality,
hypothesisEquality,
equalitySymmetry,
equalityTransitivity,
axiomEquality,
because_Cache,
hypothesis,
voidEquality,
voidElimination,
isect_memberEquality,
sqequalRule,
isectElimination,
extract_by_obid,
thin,
productElimination,
sqequalHypSubstitution,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[sg:s-Group]. \mforall{}[P:Point {}\mrightarrow{} \mBbbP{}]. mk-s-subgroup(sg;x.P[x]) \mmember{} s-Group supposing sg-subgroup(sg;x.P[x])
Date html generated:
2016_11_08-AM-09_12_36
Last ObjectModification:
2016_11_03-PM-00_23_44
Theory : inner!product!spaces
Home
Index