Nuprl Lemma : unit-ball-approx-subtype

[k,n,m:ℕ].  unit-ball-approx(m;k) ⊆unit-ball-approx(n;k) supposing n ≤ m


Proof




Definitions occuring in Statement :  unit-ball-approx: unit-ball-approx(n;k) nat: uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] le: A ≤ B
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a subtype_rel: A ⊆B member: t ∈ T unit-ball-approx: unit-ball-approx(n;k) nat: and: P ∧ Q le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A implies:  Q cand: c∧ B so_lambda: λ2x.t[x] int_seg: {i..j-} so_apply: x[s] lelt: i ≤ j < k ge: i ≥  all: x:A. B[x] decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top prop: squash: T true: True guard: {T} iff: ⇐⇒ Q less_than: a < b uiff: uiff(P;Q)
Lemmas referenced :  subtype_rel_function int_seg_wf int_seg_subtype istype-false subtype_rel_self istype-le sum_wf unit-ball-approx_wf istype-nat sum_split nat_properties decidable__lt full-omega-unsat intformand_wf intformnot_wf intformless_wf itermVar_wf itermAdd_wf itermConstant_wf intformle_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_add_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf istype-less_than le_wf squash_wf true_wf iff_weakening_equal non_neg_sum subtract_wf decidable__le itermSubtract_wf int_term_value_subtract_lemma int_seg_properties square_non_neg add-member-int_seg2 add-is-int-iff itermMultiply_wf int_term_value_mul_lemma false_wf le_functionality add_functionality_wrt_le le_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaEquality_alt sqequalHypSubstitution setElimination thin rename cut dependent_set_memberEquality_alt hypothesisEquality applyEquality introduction extract_by_obid isectElimination natural_numberEquality hypothesis minusEquality addEquality because_Cache independent_isectElimination independent_pairFormation sqequalRule lambdaFormation_alt productElimination multiplyEquality inhabitedIsType equalityTransitivity equalitySymmetry universeIsType dependent_functionElimination unionElimination approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality isect_memberEquality_alt voidElimination productIsType imageElimination imageMemberEquality baseClosed instantiate universeEquality equalityIstype closedConclusion pointwiseFunctionality promote_hyp baseApply

Latex:
\mforall{}[k,n,m:\mBbbN{}].    unit-ball-approx(m;k)  \msubseteq{}r  unit-ball-approx(n;k)  supposing  n  \mleq{}  m



Date html generated: 2019_10_30-AM-11_28_08
Last ObjectModification: 2019_06_28-PM-01_56_09

Theory : real!vectors


Home Index