Nuprl Definition : connected
Connected(X) ==
∀[A,B:X ⟶ ℙ].
((∀x:X. ∀y:{y:X| x = y} . (A[y] ⇒ A[x]))
⇒ (∀x:X. ∀y:{y:X| x = y} . (B[y] ⇒ B[x]))
⇒ (∃a:X. A[a])
⇒ (∃b:X. B[b])
⇒ (∀r:X. (A[r] ∨ B[r]))
⇒ (∃r:X. (A[r] ∧ B[r])))
Definitions occuring in Statement :
req: x = y,
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x]
Definitions occuring in definition :
uall: ∀[x:A]. B[x],
function: x:A ⟶ B[x],
prop: ℙ,
set: {x:A| B[x]} ,
req: x = y,
implies: P ⇒ Q,
all: ∀x:A. B[x],
or: P ∨ Q,
exists: ∃x:A. B[x],
and: P ∧ Q,
so_apply: x[s]
FDL editor aliases :
connected
Latex:
Connected(X) ==
\mforall{}[A,B:X {}\mrightarrow{} \mBbbP{}].
((\mforall{}x:X. \mforall{}y:\{y:X| x = y\} . (A[y] {}\mRightarrow{} A[x]))
{}\mRightarrow{} (\mforall{}x:X. \mforall{}y:\{y:X| x = y\} . (B[y] {}\mRightarrow{} B[x]))
{}\mRightarrow{} (\mexists{}a:X. A[a])
{}\mRightarrow{} (\mexists{}b:X. B[b])
{}\mRightarrow{} (\mforall{}r:X. (A[r] \mvee{} B[r]))
{}\mRightarrow{} (\mexists{}r:X. (A[r] \mwedge{} B[r])))
Date html generated:
2017_10_03-AM-10_11_07
Last ObjectModification:
2017_07_10-PM-01_12_47
Theory : reals
Home
Index