### Nuprl Lemma : no_repeats_map_uiff

`∀[T:Type]. ∀[L:T List]. ∀[A:Type]. ∀[f:{x:T| (x ∈ L)}  ⟶ A].`
`  uiff(no_repeats(A;map(f;L));no_repeats(T;L)) supposing Inj({x:T| (x ∈ L)} ;A;f)`

Proof

Definitions occuring in Statement :  no_repeats: `no_repeats(T;l)` l_member: `(x ∈ l)` map: `map(f;as)` list: `T List` inject: `Inj(A;B;f)` uiff: `uiff(P;Q)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  mapl: `mapl(f;l)` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` uiff: `uiff(P;Q)` and: `P ∧ Q` implies: `P `` Q` prop: `ℙ` no_repeats: `no_repeats(T;l)` top: `Top` not: `¬A` false: `False` nat: `ℕ` ge: `i ≥ j ` all: `∀x:A. B[x]` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` subtype_rel: `A ⊆r B` int_seg: `{i..j-}` lelt: `i ≤ j < k` le: `A ≤ B` squash: `↓T`
Lemmas referenced :  no_repeats_witness no_repeats_wf mapl_wf l_member_wf no_repeats_map inject_wf list_wf length-map equal_wf select_wf nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf not_wf nat_wf less_than_wf length_wf subtype_rel_list top_wf lelt_wf list-subtype select-map
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut independent_pairFormation extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_functionElimination hypothesis cumulativity functionExtensionality applyEquality setEquality independent_isectElimination productElimination independent_pairEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry functionEquality universeEquality voidElimination voidEquality lambdaEquality dependent_functionElimination setElimination rename natural_numberEquality unionElimination dependent_pairFormation int_eqEquality intEquality computeAll dependent_set_memberEquality lambdaFormation applyLambdaEquality imageMemberEquality baseClosed imageElimination

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[A:Type].  \mforall{}[f:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  A].
uiff(no\_repeats(A;map(f;L));no\_repeats(T;L))  supposing  Inj(\{x:T|  (x  \mmember{}  L)\}  ;A;f)

Date html generated: 2017_04_17-AM-08_41_54
Last ObjectModification: 2017_02_27-PM-04_59_24

Theory : list_1

Home Index