Nuprl Definition : has-no-path
has-no-path(A) == ∀f:ℕ ⟶ 𝔹. ∃n:ℕ. (¬(A map(f;upto(n))))
Definitions occuring in Statement :
upto: upto(n),
map: map(f;as),
nat: ℕ,
bool: 𝔹,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
apply: f a,
function: x:A ⟶ B[x]
Definitions occuring in definition :
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
bool: 𝔹,
exists: ∃x:A. B[x],
nat: ℕ,
not: ¬A,
apply: f a,
map: map(f;as),
upto: upto(n)
FDL editor aliases :
has-no-path
Latex:
has-no-path(A) == \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbB{}. \mexists{}n:\mBbbN{}. (\mneg{}(A map(f;upto(n))))
Date html generated:
2016_05_14-PM-04_12_29
Last ObjectModification:
2015_09_22-PM-06_02_22
Theory : fan-theorem
Home
Index