Nuprl Definition : eff-unique
eff-unique(A) == ∀g,h:ℕ ⟶ 𝔹. ∀n:ℕ. ((¬g n = h n) ⇒ (∃m:ℕ. (¬((A map(g;upto(m))) ∧ (A map(h;upto(m)))))))
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,
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,
bool: 𝔹,
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
Latex:
eff-unique(A) ==
\mforall{}g,h:\mBbbN{} {}\mrightarrow{} \mBbbB{}. \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_12_34
Last ObjectModification:
2015_09_22-PM-06_02_23
Theory : fan-theorem
Home
Index