Nuprl Lemma : rat-cube-third-half

k:ℕ. ∀p:ℝ^k. ∀c:ℚCube(k).  (rat-cube-third(k;p;c)  (∀h:ℚCube(k). ((↑is-half-cube(k;h;c))  rat-cube-third(k;p;h))))


Proof




Definitions occuring in Statement :  rat-cube-third: rat-cube-third(k;p;c) real-vec: ^n nat: assert: b all: x:A. B[x] implies:  Q is-half-cube: is-half-cube(k;h;c) rational-cube: Cube(k)
Definitions unfolded in proof :  subtype_rel: A ⊆B rev_uimplies: rev_uimplies(P;Q) req_int_terms: t1 ≡ t2 rdiv: (x/y) ifthenelse: if then else fi  band: p ∧b q bfalse: ff nequal: a ≠ b ∈  int_nzero: -o sq_type: SQType(T) top: Top exists: x:A. B[x] satisfiable_int_formula: satisfiable_int_formula(fmla) decidable: Dec(P) not: ¬A false: False le: A ≤ B true: True less_than': less_than'(a;b) squash: T less_than: a < b rev_implies:  Q iff: ⇐⇒ Q or: P ∨ Q rneq: x ≠ y guard: {T} prop: nat: pi2: snd(t) pi1: fst(t) is-half-interval: is-half-interval(I;J) rat-interval-third: rat-interval-third(p;I) rational-interval: Interval real-vec: ^n rational-cube: Cube(k) in-rat-cube: in-rat-cube(k;p;c) uimplies: supposing a and: P ∧ Q uiff: uiff(P;Q) uall: [x:A]. B[x] member: t ∈ T rat-cube-third: rat-cube-third(k;p;c) implies:  Q all: x:A. B[x]
Lemmas referenced :  req_inversion true_wf real_wf rneq_wf squash_wf iff_weakening_equal subtype_rel_self qavg-same rleq_weakening rmul-rinv3 rdiv_functionality req_functionality rmul_preserves_req or_wf qle_wf real_term_value_minus_lemma int-rinv-cancel rat2real-qavg-2 real_term_value_const_lemma real_term_value_var_lemma real_term_value_add_lemma real_term_value_mul_lemma real_term_value_sub_lemma real_polynomial_null req-iff-rsub-is-0 rinv-mul-as-rdiv req_weakening rmul_functionality radd_functionality req_transitivity rleq_functionality assert_of_band assert_of_bor iff_weakening_uiff iff_transitivity rationals_wf equal_wf bfalse_wf assert-qeq btrue_wf band_wf eqtt_to_assert bool_subtype_base bool_wf bool_cases qeq_wf2 bor_wf assert_wf qle_antisymmetry itermMinus_wf rminus_wf radd-preserves-rleq nequal_wf int_formula_prop_wf int_term_value_mul_lemma int_term_value_constant_lemma int_formula_prop_eq_lemma istype-void int_formula_prop_not_lemma istype-int intformeq_wf intformnot_wf full-omega-unsat decidable__equal_int int_subtype_base subtype_base_sq itermConstant_wf itermVar_wf itermAdd_wf itermMultiply_wf itermSubtract_wf rinv_wf2 req_wf rmul_wf radd_wf rleq_wf istype-false rleq-int qavg_wf int-to-real_wf rless_wf rless-int rdiv_wf rmul_preserves_rleq2 rleq-rat2real rat2real_wf rleq_transitivity istype-nat real-vec_wf rational-cube_wf rat-cube-third_wf is-half-cube_wf istype-assert in-rat-cube_wf int_seg_wf assert-is-half-cube in-rat-half-cube
Rules used in proof :  universeEquality imageElimination applyLambdaEquality hyp_replacement int_eqEquality promote_hyp inlFormation_alt productEquality unionEquality sqequalBase dependent_set_memberEquality_alt voidElimination isect_memberEquality_alt lambdaEquality_alt dependent_pairFormation_alt approximateComputation unionElimination intEquality cumulativity instantiate productIsType unionIsType closedConclusion baseClosed imageMemberEquality independent_pairFormation inrFormation_alt because_Cache setElimination natural_numberEquality universeIsType equalitySymmetry equalityTransitivity equalityIstype sqequalRule rename inhabitedIsType applyEquality independent_isectElimination productElimination isectElimination hypothesis independent_functionElimination hypothesisEquality thin dependent_functionElimination extract_by_obid introduction cut sqequalHypSubstitution lambdaFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}p:\mBbbR{}\^{}k.  \mforall{}c:\mBbbQ{}Cube(k).
    (rat-cube-third(k;p;c)  {}\mRightarrow{}  (\mforall{}h:\mBbbQ{}Cube(k).  ((\muparrow{}is-half-cube(k;h;c))  {}\mRightarrow{}  rat-cube-third(k;p;h))))



Date html generated: 2019_11_04-PM-04_43_25
Last ObjectModification: 2019_11_04-PM-03_13_09

Theory : real!vectors


Home Index