Nuprl Lemma : closures-meet-sq'
∀[P,Q:ℝ ⟶ ℙ].
((∃a:{a:ℝ| P a} . (∃b:ℝ [((Q b) ∧ (a < b))]))
⇒ (∃c:{c:ℝ| (r0 ≤ c) ∧ (c < r1)}
∀a:{a:ℝ| P a} . ∀b:{b:ℝ| (Q b) ∧ (a < b)} .
∃a':{a':ℝ| P a'} . (∃b':{b':ℝ| (Q b') ∧ (a' < b')} [((a ≤ a') ∧ (b' ≤ b) ∧ ((b' - a') ≤ ((b - a) * c)))]))
⇒ (∃y:ℝ. (y ∈ closure(λz.(↓P z)) ∧ y ∈ closure(λz.(↓Q z)))))
Proof
Definitions occuring in Statement :
member-closure: y ∈ closure(A),
rleq: x ≤ y,
rless: x < y,
rsub: x - y,
rmul: a * b,
int-to-real: r(n),
real: ℝ,
uall: ∀[x:A]. B[x],
prop: ℙ,
all: ∀x:A. B[x],
sq_exists: ∃x:A [B[x]],
exists: ∃x:A. B[x],
squash: ↓T,
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
natural_number: $n
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
exists: ∃x:A. B[x],
sq_exists: ∃x:A [B[x]],
member: t ∈ T,
and: P ∧ Q,
prop: ℙ,
all: ∀x:A. B[x],
subtype_rel: A ⊆r B,
uimplies: b supposing a,
guard: {T},
cand: A c∧ B,
so_apply: x[s],
so_lambda: λ2x.t[x],
top: Top,
squash: ↓T,
sq_stable: SqStable(P),
pi2: snd(t),
pi1: fst(t),
false: False,
satisfiable_int_formula: satisfiable_int_formula(fmla),
not: ¬A,
or: P ∨ Q,
decidable: Dec(P),
ge: i ≥ j ,
nat: ℕ,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
assert: ↑b,
ifthenelse: if b then t else f fi ,
bnot: ¬bb,
sq_type: SQType(T),
bfalse: ff,
uiff: uiff(P;Q),
btrue: tt,
it: ⋅,
unit: Unit,
bool: 𝔹,
rleq: x ≤ y,
rnonneg: rnonneg(x),
le: A ≤ B,
rbetween: x≤y≤z,
less_than': less_than'(a;b),
rev_uimplies: rev_uimplies(P;Q),
req_int_terms: t1 ≡ t2,
rge: x ≥ y,
nat_plus: ℕ+,
rless: x < y,
nequal: a ≠ b ∈ T ,
real: ℝ,
rmul: a * b,
member-closure: y ∈ closure(A)
Latex:
\mforall{}[P,Q:\mBbbR{} {}\mrightarrow{} \mBbbP{}].
((\mexists{}a:\{a:\mBbbR{}| P a\} . (\mexists{}b:\mBbbR{} [((Q b) \mwedge{} (a < b))]))
{}\mRightarrow{} (\mexists{}c:\{c:\mBbbR{}| (r0 \mleq{} c) \mwedge{} (c < r1)\}
\mforall{}a:\{a:\mBbbR{}| P a\} . \mforall{}b:\{b:\mBbbR{}| (Q b) \mwedge{} (a < b)\} .
\mexists{}a':\{a':\mBbbR{}| P a'\} . (\mexists{}b':\{b':\mBbbR{}| (Q b') \mwedge{} (a' < b')\} [((a \mleq{} a') \mwedge{} (b' \mleq{} b) \mwedge{} ((b' - a') \mleq{} ((\000Cb - a) * c)))]))
{}\mRightarrow{} (\mexists{}y:\mBbbR{}. (y \mmember{} closure(\mlambda{}z.(\mdownarrow{}P z)) \mwedge{} y \mmember{} closure(\mlambda{}z.(\mdownarrow{}Q z)))))
Date html generated:
2020_05_20-AM-11_29_59
Last ObjectModification:
2020_01_06-PM-00_20_11
Theory : reals
Home
Index