Nuprl Definition : eff-unique-path
eff-unique-path(T;A) ==
∀g,h:ℕ ⟶ T. ∀n:ℕ. ((¬((g n) = (h n) ∈ T)) ⇒ (∃m:ℕ. (¬((A map(g;upto(m))) ∧ (A map(h;upto(m)))))))
Definitions occuring in Statement :
upto: upto(n),
map: map(f;as),
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
function: x:A ⟶ B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
equal: s = t ∈ T,
exists: ∃x:A. B[x],
nat: ℕ,
not: ¬A,
and: P ∧ Q,
apply: f a,
map: map(f;as),
upto: upto(n)
FDL editor aliases :
eff-unique-path
Latex:
eff-unique-path(T;A) ==
\mforall{}g,h:\mBbbN{} {}\mrightarrow{} T. \mforall{}n:\mBbbN{}. ((\mneg{}((g n) = (h n))) {}\mRightarrow{} (\mexists{}m:\mBbbN{}. (\mneg{}((A map(g;upto(m))) \mwedge{} (A map(h;upto(m)))))))
Date html generated:
2016_05_14-PM-04_09_53
Last ObjectModification:
2015_09_22-PM-06_02_18
Theory : fan-theorem
Home
Index