Nuprl Lemma : quot_grp_car_wf
∀g:IGroup. ∀h:NormSubGrp{i}(g). (|g//h| ∈ Type)
Proof
Definitions occuring in Statement :
quot_grp_car: |g//h|,
norm_subgrp: NormSubGrp{i}(g),
igrp: IGroup,
all: ∀x:A. B[x],
member: t ∈ T,
universe: Type
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
norm_subgrp: NormSubGrp{i}(g),
quot_grp_car: |g//h|,
and: P ∧ Q,
uall: ∀[x:A]. B[x],
igrp: IGroup,
imon: IMonoid,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
uimplies: b supposing a,
implies: P ⇒ Q,
prop: ℙ,
guard: {T},
subgrp_p: s SubGrp of g
Lemmas referenced :
quotient_wf,
grp_car_wf,
eqv_mod_subset_wf,
eqv_mod_subset_is_eqv,
norm_subgrp_wf,
igrp_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalHypSubstitution,
setElimination,
thin,
rename,
productElimination,
lemma_by_obid,
isectElimination,
hypothesisEquality,
hypothesis,
sqequalRule,
lambdaEquality,
because_Cache,
independent_isectElimination,
dependent_functionElimination,
independent_functionElimination,
applyEquality
Latex:
\mforall{}g:IGroup. \mforall{}h:NormSubGrp\{i\}(g). (|g//h| \mmember{} Type)
Date html generated:
2016_05_15-PM-00_09_19
Last ObjectModification:
2015_12_26-PM-11_45_40
Theory : groups_1
Home
Index