Nuprl Definition : contra-cc
CCC(T) == ∀R:ℕ ⟶ T ⟶ ℙ. ((∀g:ℕ ⟶ T. ∃n:ℕ. (R n (g n))) ⇒ (∃n:ℕ. ∀m:T. (R n m)))
Definitions occuring in Statement :
nat: ℕ,
prop: ℙ,
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,
all: ∀x:A. B[x],
nat: ℕ,
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
implies: P ⇒ Q,
prop: ℙ
FDL editor aliases :
contra-cc
Latex:
CCC(T) == \mforall{}R:\mBbbN{} {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}. ((\mforall{}g:\mBbbN{} {}\mrightarrow{} T. \mexists{}n:\mBbbN{}. (R n (g n))) {}\mRightarrow{} (\mexists{}n:\mBbbN{}. \mforall{}m:T. (R n m)))
Date html generated:
2019_06_20-PM-03_00_10
Last ObjectModification:
2019_06_12-PM-07_58_58
Theory : continuity
Home
Index