### Nuprl Lemma : pairwise-map

`∀[T,T2:Type].`
`  ∀L:T List. ∀[P:T2 ⟶ T2 ⟶ ℙ']. ∀[f:{x:T| (x ∈ L)}  ⟶ T2].  ((∀x,y∈map(f;L).  P[x;y]) `⇐⇒` (∀x,y∈L.  P[f x;f y]))`

Proof

Definitions occuring in Statement :  pairwise: `(∀x,y∈L.  P[x; y])` l_member: `(x ∈ l)` map: `map(f;as)` list: `T List` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` prop: `ℙ` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` pairwise: `(∀x,y∈L.  P[x; y])` top: `Top` int_seg: `{i..j-}` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` rev_implies: `P `` Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` lelt: `i ≤ j < k` guard: `{T}` decidable: `Dec(P)` or: `P ∨ Q` less_than: `a < b` squash: `↓T` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` le: `A ≤ B`
Lemmas referenced :  list-subtype list_wf l_member_wf length-map int_seg_wf length_wf pairwise_wf2 map_wf equal_wf set_wf subtype_rel_list top_wf int_seg_properties decidable__lt satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_formula_prop_wf lelt_wf select-map
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality equalityTransitivity hypothesis equalitySymmetry setEquality independent_pairFormation sqequalRule isect_memberEquality voidElimination voidEquality dependent_functionElimination because_Cache setElimination rename natural_numberEquality instantiate functionExtensionality applyEquality lambdaEquality dependent_set_memberEquality independent_functionElimination functionEquality universeEquality independent_isectElimination productElimination unionElimination imageElimination dependent_pairFormation int_eqEquality intEquality computeAll

Latex:
\mforall{}[T,T2:Type].
\mforall{}L:T  List
\mforall{}[P:T2  {}\mrightarrow{}  T2  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}[f:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  T2].
((\mforall{}x,y\mmember{}map(f;L).    P[x;y])  \mLeftarrow{}{}\mRightarrow{}  (\mforall{}x,y\mmember{}L.    P[f  x;f  y]))

Date html generated: 2017_04_17-AM-07_44_23
Last ObjectModification: 2017_02_27-PM-04_16_07

Theory : list_1

Home Index