Nuprl Lemma : permutation-of-permutations-list
∀n:ℕ. ∀f:{p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} ⟶ {p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} .
(Bij({p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} ;{p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} ;f)
⇒ permutation({p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} ;permutations-list(n);map(f;permutations-list(n))))
Proof
Definitions occuring in Statement :
permutations-list: permutations-list(n),
permutation: permutation(T;L1;L2),
map: map(f;as),
biject: Bij(A;B;f),
inject: Inj(A;B;f),
int_seg: {i..j-},
nat: ℕ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
uall: ∀[x:A]. B[x],
member: t ∈ T,
nat: ℕ,
prop: ℙ,
subtype_rel: A ⊆r B,
injection: A →⟶ B,
and: P ∧ Q,
so_lambda: λ2x.t[x],
so_apply: x[s],
cand: A c∧ B,
sq_stable: SqStable(P),
squash: ↓T
Lemmas referenced :
map-is-permutation-on-list-of-all,
int_seg_wf,
inject_wf,
permutations-list_wf,
list_wf,
injection_wf,
no_repeats_wf,
all_wf,
l_member_wf,
set_wf,
sq_stable__no_repeats,
equal_wf,
biject_wf,
nat_wf,
sq_stable__and,
sq_stable__all,
sq_stable__l_member,
decidable__equal_injection,
decidable__equal_int_seg
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
setEquality,
functionEquality,
natural_numberEquality,
setElimination,
rename,
because_Cache,
hypothesis,
hypothesisEquality,
dependent_functionElimination,
independent_functionElimination,
applyEquality,
lambdaEquality,
sqequalRule,
productEquality,
productElimination,
imageMemberEquality,
baseClosed,
imageElimination,
equalityTransitivity,
equalitySymmetry,
independent_pairFormation,
isect_memberEquality
Latex:
\mforall{}n:\mBbbN{}. \mforall{}f:\{p:\mBbbN{}n {}\mrightarrow{} \mBbbN{}n| Inj(\mBbbN{}n;\mBbbN{}n;p)\} {}\mrightarrow{} \{p:\mBbbN{}n {}\mrightarrow{} \mBbbN{}n| Inj(\mBbbN{}n;\mBbbN{}n;p)\} .
(Bij(\{p:\mBbbN{}n {}\mrightarrow{} \mBbbN{}n| Inj(\mBbbN{}n;\mBbbN{}n;p)\} ;\{p:\mBbbN{}n {}\mrightarrow{} \mBbbN{}n| Inj(\mBbbN{}n;\mBbbN{}n;p)\} ;f)
{}\mRightarrow{} permutation(\{p:\mBbbN{}n {}\mrightarrow{} \mBbbN{}n| Inj(\mBbbN{}n;\mBbbN{}n;p)\} ;permutations-list(n);map(f;permutations-list(n))))
Date html generated:
2018_05_21-PM-08_22_28
Last ObjectModification:
2018_05_19-PM-04_56_56
Theory : general
Home
Index