### Nuprl Lemma : map-is-permutation-on-list-of-all

`∀[T:Type]`
`  ∀f:T ⟶ T. (Bij(T;T;f) `` (∀as:T List. ((no_repeats(T;as) ∧ (∀t:T. (t ∈ as))) `` permutation(T;as;map(f;as)))))`

Proof

Definitions occuring in Statement :  permutation: `permutation(T;L1;L2)` no_repeats: `no_repeats(T;l)` l_member: `(x ∈ l)` map: `map(f;as)` list: `T List` biject: `Bij(A;B;f)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  guard: `{T}` so_apply: `x[s]` so_lambda: `λ2x.t[x]` rev_implies: `P `` Q` prop: `ℙ` iff: `P `⇐⇒` Q` member: `t ∈ T` and: `P ∧ Q` implies: `P `` Q` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` exists: `∃x:A. B[x]` surject: `Surj(A;B;f)` biject: `Bij(A;B;f)` top: `Top` false: `False` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` or: `P ∨ Q` decidable: `Dec(P)` ge: `i ≥ j ` uimplies: `b supposing a` nat: `ℕ` cand: `A c∧ B` l_member: `(x ∈ l)` true: `True` squash: `↓T` lelt: `i ≤ j < k` int_seg: `{i..j-}` subtype_rel: `A ⊆r B` inject: `Inj(A;B;f)`
Lemmas referenced :  biject_wf list_wf all_wf no_repeats_wf l_member_wf map_wf permutation-when-no_repeats int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf full-omega-unsat decidable__le nat_properties select_wf equal_wf length_wf less_than_wf map-length iff_weakening_equal true_wf squash_wf lelt_wf top_wf subtype_rel_list select-map set_wf subtype_rel_dep_function no_repeats_map
Rules used in proof :  universeEquality functionEquality lambdaEquality sqequalRule productEquality because_Cache independent_pairFormation independent_functionElimination hypothesis applyEquality functionExtensionality cumulativity dependent_functionElimination hypothesisEquality isectElimination extract_by_obid introduction cut thin productElimination sqequalHypSubstitution lambdaFormation isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution voidEquality voidElimination isect_memberEquality intEquality int_eqEquality approximateComputation unionElimination natural_numberEquality independent_isectElimination rename setElimination promote_hyp dependent_pairFormation baseClosed imageMemberEquality equalitySymmetry equalityTransitivity imageElimination dependent_set_memberEquality setEquality

Latex:
\mforall{}[T:Type]
\mforall{}f:T  {}\mrightarrow{}  T
(Bij(T;T;f)
{}\mRightarrow{}  (\mforall{}as:T  List.  ((no\_repeats(T;as)  \mwedge{}  (\mforall{}t:T.  (t  \mmember{}  as)))  {}\mRightarrow{}  permutation(T;as;map(f;as)))))

Date html generated: 2018_05_21-PM-00_44_09
Last ObjectModification: 2017_12_11-AM-10_52_34

Theory : list_1

Home Index