### Nuprl Lemma : prod-metric-meq

`∀[k:ℕ]. ∀[X:ℕk ⟶ Type]. ∀[d:i:ℕk ⟶ metric(X[i])]. ∀[p,q:i:ℕk ⟶ X[i]].  uiff(p ≡ q;∀i:ℕk. p i ≡ q i)`

Proof

Definitions occuring in Statement :  prod-metric: `prod-metric(k;d)` meq: `x ≡ y` metric: `metric(X)` int_seg: `{i..j-}` nat: `ℕ` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` nat: `ℕ` so_apply: `x[s]` so_lambda: `λ2x.t[x]` prop: `ℙ` all: `∀x:A. B[x]` implies: `P `` Q` sq_stable: `SqStable(P)` meq: `x ≡ y` subtype_rel: `A ⊆r B` metric: `metric(X)` int_seg: `{i..j-}` lelt: `i ≤ j < k` and: `P ∧ Q` le: `A ≤ B` prod-metric: `prod-metric(k;d)` mdist: `mdist(d;x;y)` squash: `↓T` uimplies: `b supposing a` uiff: `uiff(P;Q)`
Lemmas referenced :  sq_stable__uiff meq_wf int_seg_wf prod-metric_wf sq_stable__meq sq_stable__all req_witness int-to-real_wf metric_wf istype-universe istype-nat rsum-of-nonneg-zero-iff subtract_wf subtract-add-cancel mdist_wf mdist-nonneg
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin functionEquality natural_numberEquality setElimination rename because_Cache hypothesis applyEquality hypothesisEquality sqequalRule lambdaEquality_alt universeIsType independent_functionElimination lambdaFormation_alt dependent_functionElimination inhabitedIsType equalityTransitivity equalitySymmetry productElimination functionIsTypeImplies imageMemberEquality baseClosed imageElimination functionIsType instantiate universeEquality independent_isectElimination

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[X:\mBbbN{}k  {}\mrightarrow{}  Type].  \mforall{}[d:i:\mBbbN{}k  {}\mrightarrow{}  metric(X[i])].  \mforall{}[p,q:i:\mBbbN{}k  {}\mrightarrow{}  X[i]].
uiff(p  \mequiv{}  q;\mforall{}i:\mBbbN{}k.  p  i  \mequiv{}  q  i)

Date html generated: 2019_10_29-AM-11_09_54
Last ObjectModification: 2019_10_10-PM-10_07_38

Theory : reals

Home Index