Nuprl Lemma : map_functionality_2
∀A,B:Type. ∀as:A List. ∀f,f':A ⟶ B. ∀as:A List.
((f = f' ∈ ({x:A| mem_f(A;x;as)} ⟶ B)) ⇒ (map(f;as) = map(f';as) ∈ (B List)))
Proof
Definitions occuring in Statement :
mem_f: mem_f(T;a;bs),
map: map(f;as),
list: T List,
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
so_apply: x[s],
uimplies: b supposing a,
mem_f: mem_f(T;a;bs),
ycomb: Y,
so_lambda: so_lambda(x,y,z.t[x; y; z]),
top: Top,
so_apply: x[s1;s2;s3],
or: P ∨ Q,
squash: ↓T,
true: True,
guard: {T}
Lemmas referenced :
equal_wf,
mem_f_wf,
subtype_rel_dep_function,
set_wf,
list_wf,
list_induction,
map_wf,
list_ind_nil_lemma,
map_nil_lemma,
nil_wf,
false_wf,
list_ind_cons_lemma,
map_cons_lemma,
or_wf,
cons_wf,
squash_wf,
true_wf,
subtype_rel_sets,
equal_functionality_wrt_subtype_rel2
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
hypothesis,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
functionEquality,
setEquality,
hypothesisEquality,
dependent_functionElimination,
applyEquality,
sqequalRule,
lambdaEquality,
independent_isectElimination,
setElimination,
rename,
because_Cache,
independent_functionElimination,
isect_memberEquality,
voidElimination,
voidEquality,
imageElimination,
equalityTransitivity,
equalitySymmetry,
universeEquality,
natural_numberEquality,
imageMemberEquality,
baseClosed,
hyp_replacement,
applyLambdaEquality,
cumulativity,
functionExtensionality,
inlFormation,
dependent_set_memberEquality,
inrFormation
Latex:
\mforall{}A,B:Type. \mforall{}as:A List. \mforall{}f,f':A {}\mrightarrow{} B. \mforall{}as:A List. ((f = f') {}\mRightarrow{} (map(f;as) = map(f';as)))
Date html generated:
2019_10_16-PM-01_02_34
Last ObjectModification:
2018_09_17-PM-06_17_46
Theory : list_2
Home
Index