Nuprl Lemma : remove-singularity-max-seq_wf

[X:Type]. ∀[k:ℕ]. ∀[p:ℝ^k]. ∀[f:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)}  ⟶ X]. ∀[z:X].
  (remove-singularity-max-seq(k;p;f;z) ∈ ℕ ⟶ X)


Proof




Definitions occuring in Statement :  remove-singularity-max-seq: remove-singularity-max-seq(k;p;f;z) max-metric: max-metric(n) real-vec: ^n mdist: mdist(d;x;y) rless: x < y int-to-real: r(n) nat: uall: [x:A]. B[x] member: t ∈ T set: {x:A| B[x]}  lambda: λx.A[x] function: x:A ⟶ B[x] natural_number: $n universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] real-vec: ^n member: t ∈ T int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q le: A ≤ B nat: remove-singularity-max-seq: remove-singularity-max-seq(k;p;f;z) subtype_rel: A ⊆B all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  uiff: uiff(P;Q) uimplies: supposing a iff: ⇐⇒ Q rev_implies:  Q exists: x:A. B[x] so_lambda: λ2x.t[x] so_apply: x[s] prop: bfalse: ff
Lemmas referenced :  int-to-real_wf int_seg_wf realvec-max-ibs_wf eq_int_wf eqtt_to_assert assert_of_eq_int realvec-max-ibs-property set_subtype_base lelt_wf int_subtype_base rless_wf mdist_wf real-vec_wf max-metric_wf istype-nat istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut sqequalRule lambdaEquality_alt introduction extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename productElimination hypothesis universeIsType natural_numberEquality hypothesisEquality applyEquality because_Cache closedConclusion inhabitedIsType lambdaFormation_alt unionElimination equalityElimination independent_isectElimination dependent_functionElimination independent_functionElimination dependent_pairFormation_alt equalityIstype equalityTransitivity equalitySymmetry intEquality baseClosed sqequalBase dependent_set_memberEquality_alt axiomEquality isect_memberEquality_alt isectIsTypeImplies functionIsType setIsType instantiate universeEquality

Latex:
\mforall{}[X:Type].  \mforall{}[k:\mBbbN{}].  \mforall{}[p:\mBbbR{}\^{}k].  \mforall{}[f:\{p:\mBbbR{}\^{}k|  r0  <  mdist(max-metric(k);p;\mlambda{}i.r0)\}    {}\mrightarrow{}  X].  \mforall{}[z:X].
    (remove-singularity-max-seq(k;p;f;z)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  X)



Date html generated: 2019_10_30-AM-10_16_28
Last ObjectModification: 2019_07_03-PM-04_27_14

Theory : real!vectors


Home Index