Nuprl Lemma : avoid-real
∀a,b,x:ℝ. ((a < b) ⇒ (∃a',b':ℝ. ((a ≤ a') ∧ (b' ≤ b) ∧ (a' < b') ∧ ((x < a') ∨ (b' < x)))))
Proof
Definitions occuring in Statement :
rleq: x ≤ y,
rless: x < y,
real: ℝ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
cand: A c∧ B,
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x],
int_nzero: ℤ-o,
true: True,
nequal: a ≠ b ∈ T ,
not: ¬A,
uimplies: b supposing a,
sq_type: SQType(T),
guard: {T},
false: False,
rneq: x ≠ y,
or: P ∨ Q,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
less_than: a < b,
squash: ↓T,
less_than': less_than'(a;b),
exists: ∃x:A. B[x],
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
rless_wf,
real_wf,
int-rdiv_wf,
subtype_base_sq,
int_subtype_base,
equal-wf-base,
true_wf,
nequal_wf,
radd_wf,
int-rmul_wf,
rdiv_wf,
int-to-real_wf,
rless-int,
rmul_wf,
rmul_preserves_rless,
rless_functionality,
req_weakening,
int-rdiv-req,
rdiv_functionality,
radd_functionality,
int-rmul-req,
rmul_comm,
rmul-rdiv-cancel2,
radd-preserves-rless,
rminus_wf,
radd-zero-both,
rmul-one-both,
rmul-zero-both,
rmul_functionality,
req_transitivity,
radd-int,
rminus-as-rmul,
req_inversion,
rmul-distrib2,
radd-assoc,
radd-rminus-both,
radd-rminus-assoc,
radd-ac,
radd_comm,
rless-cases,
rleq_weakening_equal,
rless_transitivity2,
rleq_weakening_rless,
rleq_wf,
or_wf,
exists_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
independent_pairFormation,
hypothesis,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
dependent_set_memberEquality,
natural_numberEquality,
addLevel,
instantiate,
cumulativity,
intEquality,
independent_isectElimination,
dependent_functionElimination,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination,
voidElimination,
baseClosed,
because_Cache,
sqequalRule,
inrFormation,
productElimination,
imageMemberEquality,
minusEquality,
addEquality,
levelHypothesis,
unionElimination,
dependent_pairFormation,
productEquality,
lambdaEquality,
inlFormation
Latex:
\mforall{}a,b,x:\mBbbR{}. ((a < b) {}\mRightarrow{} (\mexists{}a',b':\mBbbR{}. ((a \mleq{} a') \mwedge{} (b' \mleq{} b) \mwedge{} (a' < b') \mwedge{} ((x < a') \mvee{} (b' < x)))))
Date html generated:
2016_10_26-AM-09_33_27
Last ObjectModification:
2016_08_13-AM-11_33_59
Theory : reals
Home
Index