Nuprl Lemma : rat-cube-third-not-in-face

[k:ℕ]. ∀[p:ℝ^k]. ∀[c:ℚCube(k)].
  ∀f:ℚCube(k). in-rat-cube(k;p;f)) supposing ((¬(f c ∈ ℚCube(k))) and f ≤ c) supposing rat-cube-third(k;p;c) ∧ (↑Inh\000Cabited(c))


Proof




Definitions occuring in Statement :  rat-cube-third: rat-cube-third(k;p;c) in-rat-cube: in-rat-cube(k;p;c) real-vec: ^n nat: assert: b uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] not: ¬A and: P ∧ Q equal: t ∈ T inhabited-rat-cube: Inhabited(c) rat-cube-face: c ≤ d rational-cube: Cube(k)
Definitions unfolded in proof :  req_int_terms: t1 ≡ t2 rdiv: (x/y) rev_uimplies: rev_uimplies(P;Q) nequal: a ≠ b ∈  int_nzero: -o sq_type: SQType(T) exists: x:A. B[x] satisfiable_int_formula: satisfiable_int_formula(fmla) decidable: Dec(P) uiff: uiff(P;Q) less_than': less_than'(a;b) less_than: a < b rneq: x ≠ y rat-interval-third: rat-interval-third(p;I) rev_implies:  Q iff: ⇐⇒ Q guard: {T} squash: T true: True subtype_rel: A ⊆B nat: prop: pi1: fst(t) pi2: snd(t) top: Top so_apply: x[s] so_lambda: λ2x.t[x] or: P ∨ Q rat-point-interval: [a] rat-interval-face: I ≤ J rational-interval: Interval real-vec: ^n rat-cube-face: c ≤ d in-rat-cube: in-rat-cube(k;p;c) rational-cube: Cube(k) rat-cube-third: rat-cube-third(k;p;c) and: P ∧ Q false: False implies:  Q not: ¬A all: x:A. B[x] uimplies: supposing a member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  real_term_value_add_lemma real_term_value_const_lemma real_term_value_var_lemma real_term_value_mul_lemma real_term_value_sub_lemma real_polynomial_null int-rinv-cancel rmul-rinv3 radd_functionality req_transitivity req_weakening req_functionality req-iff-rsub-is-0 rsub_wf req-implies-req req-rat2real nequal_wf int_formula_prop_wf int_term_value_mul_lemma int_term_value_constant_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma istype-int intformeq_wf intformnot_wf full-omega-unsat decidable__equal_int int_subtype_base subtype_base_sq itermAdd_wf rinv_wf2 itermConstant_wf itermVar_wf itermMultiply_wf itermSubtract_wf rmul_preserves_req rless_wf rless-int int-to-real_wf rmul_wf radd_wf rdiv_wf req_fake_le_antisymmetry istype-universe equal_wf iff_weakening_equal subtype_rel_self real_wf true_wf squash_wf rational-interval_wf rat2real_wf rleq_wf rat-interval-third_wf istype-nat real-vec_wf rational-cube_wf inhabited-rat-cube_wf istype-assert rat-cube-third_wf rat-cube-face_wf in-rat-cube_wf int_seg_wf rat-interval-face_wf istype-void pi1_wf_top rationals_wf pi2_wf in-rat-cube-face
Rules used in proof :  int_eqEquality sqequalBase dependent_set_memberEquality_alt dependent_pairFormation_alt approximateComputation intEquality cumulativity inrFormation_alt closedConclusion promote_hyp independent_pairFormation universeEquality instantiate baseClosed imageMemberEquality imageElimination productIsType isectIsTypeImplies functionIsType functionIsTypeImplies because_Cache rename setElimination natural_numberEquality equalitySymmetry equalityTransitivity equalityIstype universeIsType voidElimination isect_memberEquality_alt independent_pairEquality lambdaEquality_alt sqequalRule applyLambdaEquality unionElimination inhabitedIsType applyEquality dependent_functionElimination functionExtensionality hypothesis independent_isectElimination hypothesisEquality isectElimination extract_by_obid independent_functionElimination productElimination sqequalHypSubstitution thin lambdaFormation_alt cut introduction isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[p:\mBbbR{}\^{}k].  \mforall{}[c:\mBbbQ{}Cube(k)].
    \mforall{}f:\mBbbQ{}Cube(k).  (\mneg{}in-rat-cube(k;p;f))  supposing  ((\mneg{}(f  =  c))  and  f  \mleq{}  c) 
    supposing  rat-cube-third(k;p;c)  \mwedge{}  (\muparrow{}Inhabited(c))



Date html generated: 2019_11_04-PM-04_43_32
Last ObjectModification: 2019_11_04-PM-03_32_34

Theory : real!vectors


Home Index