Nuprl Lemma : sublist_map

[A,B:Type].  ∀f:A ⟶ B. ∀as,bs:A List.  (as ⊆ bs  map(f;as) ⊆ map(f;bs))


Proof




Definitions occuring in Statement :  sublist: L1 ⊆ L2 map: map(f;as) list: List uall: [x:A]. B[x] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] implies:  Q sublist: L1 ⊆ L2 exists: x:A. B[x] member: t ∈ T and: P ∧ Q subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A prop: squash: T true: True guard: {T} iff: ⇐⇒ Q rev_implies:  Q decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top int_seg: {i..j-} lelt: i ≤ j < k cand: c∧ B less_than: a < b ge: i ≥  nat:
Lemmas referenced :  subtype_rel_dep_function int_seg_wf length_wf map_wf int_seg_subtype false_wf le_wf map_length_nat iff_weakening_equal decidable__le satisfiable-full-omega-tt intformnot_wf intformle_wf itermVar_wf int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_var_lemma int_formula_prop_wf int_seg_properties increasing_wf length_wf_nat all_wf equal_wf select_wf intformand_wf itermConstant_wf int_formula_prop_and_lemma int_term_value_constant_lemma decidable__lt intformless_wf int_formula_prop_less_lemma non_neg_length map_length lelt_wf nat_properties map-length intformeq_wf int_formula_prop_eq_lemma sublist_wf list_wf select-map subtype_rel_list top_wf squash_wf true_wf map_select length-map
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation sqequalHypSubstitution productElimination thin dependent_pairFormation cut hypothesisEquality applyEquality introduction extract_by_obid isectElimination natural_numberEquality cumulativity hypothesis sqequalRule lambdaEquality functionExtensionality independent_isectElimination because_Cache independent_pairFormation imageElimination imageMemberEquality baseClosed equalityTransitivity equalitySymmetry independent_functionElimination dependent_functionElimination unionElimination int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll setElimination rename productEquality dependent_set_memberEquality applyLambdaEquality functionEquality universeEquality

Latex:
\mforall{}[A,B:Type].    \mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}as,bs:A  List.    (as  \msubseteq{}  bs  {}\mRightarrow{}  map(f;as)  \msubseteq{}  map(f;bs))



Date html generated: 2017_04_14-AM-09_29_48
Last ObjectModification: 2017_02_27-PM-04_01_58

Theory : list_1


Home Index