Nuprl Lemma : mon_for_functionality_wrt_permr
∀g:IAbMonoid. ∀A:Type. ∀as,as':A List. ∀f,f':A ⟶ |g|.
((as ≡(A) as')
⇒ (∀x:A. (mem_f(A;x;as) ⇒ (f[x] = f'[x] ∈ |g|)))
⇒ ((For{g} x ∈ as. f[x]) = (For{g} x ∈ as'. f'[x]) ∈ |g|))
Proof
Definitions occuring in Statement :
mon_for: For{g} x ∈ as. f[x],
mem_f: mem_f(T;a;bs),
permr: as ≡(T) bs,
list: T List,
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T,
iabmonoid: IAbMonoid,
grp_car: |g|
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
mon_for: For{g} x ∈ as. f[x],
for: For{T,op,id} x ∈ as. f[x],
mon_reduce: mon_reduce,
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x],
iabmonoid: IAbMonoid,
imon: IMonoid,
so_apply: x[s],
tlambda: λx:T. b[x],
true: True,
squash: ↓T,
subtype_rel: A ⊆r B,
uimplies: b supposing a,
guard: {T},
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q
Lemmas referenced :
mem_f_wf,
grp_car_wf,
permr_wf,
list_wf,
istype-universe,
iabmonoid_wf,
mon_reduce_wf,
map_wf,
equal_wf,
squash_wf,
true_wf,
mon_reduce_functionality_wrt_permr,
map_functionality,
permr_inversion,
subtype_rel_self,
iff_weakening_equal,
imon_wf,
map_functionality_2
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
hypothesis,
sqequalRule,
functionIsType,
universeIsType,
hypothesisEquality,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
equalityIstype,
isectElimination,
setElimination,
rename,
applyEquality,
inhabitedIsType,
instantiate,
universeEquality,
because_Cache,
lambdaEquality_alt,
natural_numberEquality,
imageElimination,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination,
imageMemberEquality,
baseClosed,
independent_isectElimination,
productElimination,
setIsType
Latex:
\mforall{}g:IAbMonoid. \mforall{}A:Type. \mforall{}as,as':A List. \mforall{}f,f':A {}\mrightarrow{} |g|.
((as \mequiv{}(A) as')
{}\mRightarrow{} (\mforall{}x:A. (mem\_f(A;x;as) {}\mRightarrow{} (f[x] = f'[x])))
{}\mRightarrow{} ((For\{g\} x \mmember{} as. f[x]) = (For\{g\} x \mmember{} as'. f'[x])))
Date html generated:
2020_05_20-AM-09_35_34
Last ObjectModification:
2020_01_08-PM-06_00_19
Theory : list_2
Home
Index