Nuprl Lemma : mon_itop_perm_invar
∀g:IAbMonoid. ∀n:ℕ. ∀E:ℕn ⟶ |g|. ∀p:Sym(n). ((Π 0 ≤ j < n. E[p.f j]) = (Π 0 ≤ j < n. E[j]) ∈ |g|)
Proof
Definitions occuring in Statement :
sym_grp: Sym(n),
perm_f: p.f,
int_seg: {i..j-},
nat: ℕ,
so_apply: x[s],
all: ∀x:A. B[x],
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
equal: s = t ∈ T,
mon_itop: Π lb ≤ i < ub. E[i],
iabmonoid: IAbMonoid,
grp_car: |g|
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
nat: ℕ,
iabmonoid: IAbMonoid,
imon: IMonoid,
so_apply: x[s],
so_lambda: λ2x.t[x],
sym_grp: Sym(n),
perm: Perm(T),
implies: P ⇒ Q,
guard: {T},
id_perm: id_perm(),
mk_perm: mk_perm(f;b),
perm_f: p.f,
pi1: fst(t),
identity: Id,
comp_perm: comp_perm,
txpose_perm: txpose_perm,
compose: f o g
Lemmas referenced :
int_seg_wf,
grp_car_wf,
nat_wf,
iabmonoid_wf,
perm_induction_b,
equal_wf,
mon_itop_wf,
perm_f_wf,
perm_wf,
mon_itop_txpose_invar
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
functionIsType,
universeIsType,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
natural_numberEquality,
setElimination,
rename,
hypothesisEquality,
hypothesis,
sqequalRule,
dependent_functionElimination,
lambdaEquality_alt,
because_Cache,
applyEquality,
independent_functionElimination,
equalityIsType1,
equalityTransitivity
Latex:
\mforall{}g:IAbMonoid. \mforall{}n:\mBbbN{}. \mforall{}E:\mBbbN{}n {}\mrightarrow{} |g|. \mforall{}p:Sym(n). ((\mPi{} 0 \mleq{} j < n. E[p.f j]) = (\mPi{} 0 \mleq{} j < n. E[j]))
Date html generated:
2019_10_16-PM-01_02_10
Last ObjectModification:
2018_10_08-AM-11_50_40
Theory : list_2
Home
Index