### Nuprl Lemma : tuple-equiv-is-equiv

`∀L:(X:Type × (X ⟶ X ⟶ ℙ)) List`
`  ((∀i:ℕ||L||. let X,E = L[i] in EquivRel(X;x,y.E x y))`
`  `` EquivRel(tuple-type(map(λp.(fst(p));L));t,t'.tuple-equiv(L) t t'))`

Proof

Definitions occuring in Statement :  tuple-equiv: `tuple-equiv(L)` tuple-type: `tuple-type(L)` select: `L[n]` length: `||as||` map: `map(f;as)` list: `T List` equiv_rel: `EquivRel(T;x,y.E[x; y])` int_seg: `{i..j-}` prop: `ℙ` pi1: `fst(t)` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` spread: spread def product: `x:A × B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` equiv_rel: `EquivRel(T;x,y.E[x; y])` and: `P ∧ Q` refl: `Refl(T;x,y.E[x; y])` tuple-equiv: `tuple-equiv(L)` let: let member: `t ∈ T` uall: `∀[x:A]. B[x]` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` cand: `A c∧ B` sym: `Sym(T;x,y.E[x; y])` subtype_rel: `A ⊆r B` trans: `Trans(T;x,y.E[x; y])` int_seg: `{i..j-}` uimplies: `b supposing a` lelt: `i ≤ j < k` le: `A ≤ B` less_than: `a < b` squash: `↓T` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` pi2: `snd(t)` pi1: `fst(t)` less_than': `less_than'(a;b)` label: `...\$L... t` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  tuple-type_wf map_wf pi1_wf istype-universe tuple-equiv_wf subtype_rel_self int_seg_wf length_wf select_wf int_seg_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt intformless_wf int_formula_prop_less_lemma equiv_rel_wf list_wf select-tuple_wf int_seg_subtype_nat istype-false map-length equal_wf squash_wf true_wf length-map-sq subtype_rel_list top_wf iff_weakening_equal select-map subtype_rel_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  independent_pairFormation sqequalRule Error :universeIsType,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin instantiate productEquality universeEquality functionEquality cumulativity hypothesisEquality Error :lambdaEquality_alt,  hypothesis Error :productIsType,  Error :functionIsType,  Error :inhabitedIsType,  applyEquality because_Cache natural_numberEquality closedConclusion setElimination rename independent_isectElimination productElimination imageElimination dependent_functionElimination unionElimination approximateComputation independent_functionElimination Error :dependent_pairFormation_alt,  int_eqEquality Error :isect_memberEquality_alt,  voidElimination Error :equalityIstype,  equalityTransitivity equalitySymmetry intEquality imageMemberEquality baseClosed

Latex:
\mforall{}L:(X:Type  \mtimes{}  (X  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}))  List
((\mforall{}i:\mBbbN{}||L||.  let  X,E  =  L[i]  in  EquivRel(X;x,y.E  x  y))
{}\mRightarrow{}  EquivRel(tuple-type(map(\mlambda{}p.(fst(p));L));t,t'.tuple-equiv(L)  t  t'))

Date html generated: 2019_06_20-PM-02_16_41
Last ObjectModification: 2019_03_18-PM-04_19_42

Theory : tuples

Home Index