Nuprl Lemma : permutation-mapfilter
∀[A:Type]
∀L1,L2:A List.
(permutation(A;L1;L2)
⇒ (∀p:A ⟶ 𝔹. ∀[B:Type]. ∀f:{a:A| ↑(p a)} ⟶ B. permutation(B;mapfilter(f;p;L1);mapfilter(f;p;L2))))
Proof
Definitions occuring in Statement :
permutation: permutation(T;L1;L2),
mapfilter: mapfilter(f;P;L),
list: T List,
assert: ↑b,
bool: 𝔹,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
mapfilter: mapfilter(f;P;L),
member: t ∈ T,
prop: ℙ
Lemmas referenced :
permutation-map,
assert_wf,
filter_type,
permutation-filter,
bool_wf,
permutation_wf,
list_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
setEquality,
hypothesisEquality,
applyEquality,
hypothesis,
dependent_functionElimination,
cumulativity,
because_Cache,
independent_functionElimination,
functionEquality,
universeEquality
Latex:
\mforall{}[A:Type]
\mforall{}L1,L2:A List.
(permutation(A;L1;L2)
{}\mRightarrow{} (\mforall{}p:A {}\mrightarrow{} \mBbbB{}
\mforall{}[B:Type]. \mforall{}f:\{a:A| \muparrow{}(p a)\} {}\mrightarrow{} B. permutation(B;mapfilter(f;p;L1);mapfilter(f;p;L2))))
Date html generated:
2016_05_14-PM-02_34_05
Last ObjectModification:
2015_12_26-PM-04_20_28
Theory : list_1
Home
Index