Nuprl Definition : fan
Fan ==
∀A:(𝔹 List) ⟶ ℙ
((∀as:𝔹 List. Dec(A as)) ⇒ (∀f:ℕ ⟶ 𝔹. ∃n:ℕ. (A map(f;upto(n)))) ⇒ (∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. (A map(f;upto(n)))))
Definitions occuring in Statement :
upto: upto(n),
map: map(f;as),
list: T List,
int_seg: {i..j-},
nat: ℕ,
bool: 𝔹,
decidable: Dec(P),
prop: ℙ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n
Definitions occuring in definition :
prop: ℙ,
list: T List,
decidable: Dec(P),
implies: P ⇒ Q,
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
nat: ℕ,
bool: 𝔹,
exists: ∃x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
apply: f a,
map: map(f;as),
upto: upto(n)
FDL editor aliases :
fan
Latex:
Fan ==
\mforall{}A:(\mBbbB{} List) {}\mrightarrow{} \mBbbP{}
((\mforall{}as:\mBbbB{} List. Dec(A as))
{}\mRightarrow{} (\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbB{}. \mexists{}n:\mBbbN{}. (A map(f;upto(n))))
{}\mRightarrow{} (\mexists{}k:\mBbbN{}. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbB{}. \mexists{}n:\mBbbN{}k. (A map(f;upto(n)))))
Date html generated:
2016_05_14-PM-04_12_26
Last ObjectModification:
2015_09_22-PM-06_02_22
Theory : fan-theorem
Home
Index