Nuprl Lemma : real-unit-ball-0

B(0) ≡ Top


Proof




Definitions occuring in Statement :  real-unit-ball: B(n) ext-eq: A ≡ B top: Top natural_number: $n
Definitions unfolded in proof :  ext-eq: A ≡ B and: P ∧ Q subtype_rel: A ⊆B member: t ∈ T top: Top uall: [x:A]. B[x] nat: le: A ≤ B less_than': less_than'(a;b) not: ¬A implies:  Q false: False real-unit-ball: B(n) real-vec: ^n int_seg: {i..j-} lelt: i ≤ j < k uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] all: x:A. B[x] prop: real-vec-norm: ||x|| dot-product: x⋅y subtract: m so_lambda: λ2x.t[x] so_apply: x[s] less_than: a < b squash: T true: True iff: ⇐⇒ Q rev_implies:  Q uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  istype-void real-unit-ball_wf istype-le int_seg_properties full-omega-unsat intformand_wf intformless_wf itermVar_wf itermConstant_wf intformle_wf istype-int int_formula_prop_and_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf int_seg_wf rleq_wf real-vec-norm_wf int-to-real_wf istype-top rsum-empty rsqrt_wf rleq_weakening_equal rleq-int istype-false rleq_functionality rsqrt0 req_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation lambdaEquality_alt isect_memberEquality_alt voidElimination cut introduction extract_by_obid hypothesis universeIsType sqequalHypSubstitution isectElimination thin dependent_set_memberEquality_alt natural_numberEquality sqequalRule lambdaFormation_alt hypothesisEquality functionExtensionality setElimination rename productElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality dependent_functionElimination minusEquality imageMemberEquality baseClosed because_Cache applyEquality

Latex:
B(0)  \mequiv{}  Top



Date html generated: 2019_10_30-AM-10_15_12
Last ObjectModification: 2019_06_28-PM-01_52_18

Theory : real!vectors


Home Index