Nuprl Lemma : const-sphere-map_wf

[n:ℕ]. ∀[p:S(n)].  (const-sphere-map(p) ∈ sphere-map(n))


Proof




Definitions occuring in Statement :  const-sphere-map: const-sphere-map(p) sphere-map: sphere-map(n) real-unit-sphere: S(n) nat: uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T sphere-map: sphere-map(n) const-sphere-map: const-sphere-map(p) all: x:A. B[x] exists: x:A. B[x] nat_plus: + nat: ge: i ≥  decidable: Dec(P) or: P ∨ Q uimplies: supposing a not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top prop: false: False and: P ∧ Q real-unit-sphere: S(n) subtype_rel: A ⊆B rneq: x ≠ y guard: {T} iff: ⇐⇒ Q rev_implies:  Q less_than: a < b squash: T less_than': less_than'(a;b) true: True uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  nat_plus_properties nat_properties decidable__lt full-omega-unsat intformnot_wf intformless_wf itermConstant_wf istype-int int_formula_prop_not_lemma istype-void int_formula_prop_less_lemma int_term_value_constant_lemma int_formula_prop_wf istype-less_than real-vec-dist-same-zero decidable__le intformand_wf intformle_wf itermAdd_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_add_lemma int_term_value_var_lemma istype-le rleq_wf real-vec-dist_wf rdiv_wf int-to-real_wf rless-int rless_wf nat_plus_wf real-unit-sphere_wf istype-nat rleq-int-fractions2 itermMultiply_wf int_term_value_mul_lemma rleq_functionality req_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut dependent_set_memberEquality_alt lambdaEquality_alt hypothesisEquality inhabitedIsType sqequalRule lambdaFormation_alt dependent_pairFormation_alt natural_numberEquality extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis setElimination rename dependent_functionElimination unionElimination independent_isectElimination approximateComputation independent_functionElimination isect_memberEquality_alt voidElimination universeIsType addEquality because_Cache int_eqEquality independent_pairFormation applyEquality closedConclusion inrFormation_alt productElimination imageMemberEquality baseClosed functionIsType productIsType axiomEquality equalityTransitivity equalitySymmetry isectIsTypeImplies multiplyEquality

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[p:S(n)].    (const-sphere-map(p)  \mmember{}  sphere-map(n))



Date html generated: 2019_10_30-AM-10_15_31
Last ObjectModification: 2019_07_30-PM-02_25_26

Theory : real!vectors


Home Index