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