Nuprl Definition : VesleyAxiom
VesleyAxiom ==
∀P:ℝ ⟶ ℙ
(dense-in-interval((-∞, ∞);λx.(¬(P x)))
⇒ (∀x:ℝ. ∀y:{y:ℝ| x = y} . ((P y) ⇒ (P x)))
⇒ (∀Q:{x:ℝ| ¬(P x)} ⟶ 𝔹. ∃Q':ℝ ⟶ 𝔹. ∀x:{x:ℝ| ¬(P x)} . Q' x = Q x))
Definitions occuring in Statement :
dense-in-interval: dense-in-interval(I;X),
riiint: (-∞, ∞),
req: x = y,
real: ℝ,
bool: 𝔹,
prop: ℙ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
apply: f a,
bool: 𝔹,
equal: s = t ∈ T,
not: ¬A,
real: ℝ,
set: {x:A| B[x]} ,
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
req: x = y,
lambda: λx.A[x],
riiint: (-∞, ∞),
dense-in-interval: dense-in-interval(I;X),
prop: ℙ
FDL editor aliases :
VesleyAxiom
Latex:
VesleyAxiom ==
\mforall{}P:\mBbbR{} {}\mrightarrow{} \mBbbP{}
(dense-in-interval((-\minfty{}, \minfty{});\mlambda{}x.(\mneg{}(P x)))
{}\mRightarrow{} (\mforall{}x:\mBbbR{}. \mforall{}y:\{y:\mBbbR{}| x = y\} . ((P y) {}\mRightarrow{} (P x)))
{}\mRightarrow{} (\mforall{}Q:\{x:\mBbbR{}| \mneg{}(P x)\} {}\mrightarrow{} \mBbbB{}. \mexists{}Q':\mBbbR{} {}\mrightarrow{} \mBbbB{}. \mforall{}x:\{x:\mBbbR{}| \mneg{}(P x)\} . Q' x = Q x))
Date html generated:
2017_10_03-AM-10_15_01
Last ObjectModification:
2017_09_13-PM-03_54_27
Theory : reals
Home
Index