Nuprl Definition : contra-dcc
dCCC(T) == ∀R:ℕ ⟶ T ⟶ 𝔹. ((∀g:ℕ ⟶ T. ∃n:ℕ. (↑(R n (g n)))) ⇒ (∃n:ℕ. ∀m:T. (↑(R n m))))
Definitions occuring in Statement :
nat: ℕ,
assert: ↑b,
bool: 𝔹,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x]
Definitions occuring in definition :
apply: f a,
assert: ↑b,
all: ∀x:A. B[x],
nat: ℕ,
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
implies: P ⇒ Q,
bool: 𝔹
FDL editor aliases :
contra-dcc
Latex:
dCCC(T) == \mforall{}R:\mBbbN{} {}\mrightarrow{} T {}\mrightarrow{} \mBbbB{}. ((\mforall{}g:\mBbbN{} {}\mrightarrow{} T. \mexists{}n:\mBbbN{}. (\muparrow{}(R n (g n)))) {}\mRightarrow{} (\mexists{}n:\mBbbN{}. \mforall{}m:T. (\muparrow{}(R n m))))
Date html generated:
2019_06_20-PM-03_00_15
Last ObjectModification:
2019_06_12-PM-08_01_17
Theory : continuity
Home
Index