### Nuprl Lemma : map_functionality_wrt_sq

`∀[T:Type]. ∀[f,g:Base]. ∀[L:T List].  map(f;L) ~ map(g;L) supposing ∀x:T. ((x ∈ L) `` (f x ~ g x)) supposing T ⊆r Base`

Proof

Definitions occuring in Statement :  l_member: `(x ∈ l)` map: `map(f;as)` list: `T List` uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a` base: `Base` universe: `Type` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` prop: `ℙ` so_lambda: `λ2x.t[x]` implies: `P `` Q` subtype_rel: `A ⊆r B` so_apply: `x[s]` all: `∀x:A. B[x]` nat: `ℕ` false: `False` ge: `i ≥ j ` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` and: `P ∧ Q` or: `P ∨ Q` cons: `[a / b]` colength: `colength(L)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` guard: `{T}` decidable: `Dec(P)` nil: `[]` it: `⋅` sq_type: `SQType(T)` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` rev_implies: `P `` Q` iff: `P `⇐⇒` Q`
Lemmas referenced :  list_wf base_wf subtype_rel_wf all_wf l_member_wf sqequal-wf-base nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf less_than_wf equal-wf-T-base nat_wf colength_wf_list int_subtype_base list-cases map_nil_lemma product_subtype_list spread_cons_lemma intformeq_wf itermAdd_wf int_formula_prop_eq_lemma int_term_value_add_lemma decidable__le intformnot_wf int_formula_prop_not_lemma le_wf equal_wf subtract_wf itermSubtract_wf int_term_value_subtract_lemma subtype_base_sq set_subtype_base decidable__equal_int map_cons_lemma nil_wf cons_wf cons_member
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule sqequalHypSubstitution isect_memberEquality isectElimination thin hypothesisEquality axiomSqEquality hypothesis because_Cache equalityTransitivity equalitySymmetry Error :universeIsType,  extract_by_obid Error :inhabitedIsType,  lambdaEquality functionEquality baseApply closedConclusion baseClosed applyEquality universeEquality lambdaFormation setElimination rename intWeakElimination natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation int_eqEquality intEquality dependent_functionElimination voidElimination voidEquality independent_pairFormation unionElimination promote_hyp hypothesis_subsumption productElimination applyLambdaEquality dependent_set_memberEquality addEquality instantiate cumulativity imageElimination isect_memberFormation Error :functionIsType,  sqequalIntensionalEquality inrFormation inlFormation

Latex:
\mforall{}[T:Type]
\mforall{}[f,g:Base].  \mforall{}[L:T  List].    map(f;L)  \msim{}  map(g;L)  supposing  \mforall{}x:T.  ((x  \mmember{}  L)  {}\mRightarrow{}  (f  x  \msim{}  g  x))
supposing  T  \msubseteq{}r  Base

Date html generated: 2019_06_20-PM-01_33_19
Last ObjectModification: 2018_09_26-PM-06_00_39

Theory : list_1

Home Index