Nuprl Definition : alt-one-path
AtMostOnePath(A) == ∀g,h:ℕ ⟶ T. ∀n:ℕ. ((¬((g n) = (h n) ∈ T)) ⇒ (∃m:ℕ. (¬((↑(A m g)) ∧ (↑(A m h))))))
Definitions occuring in Statement :
nat: ℕ,
assert: ↑b,
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 :
apply: f a,
assert: ↑b,
and: P ∧ Q,
not: ¬A,
nat: ℕ,
exists: ∃x:A. B[x],
equal: s = t ∈ T,
implies: P ⇒ Q,
all: ∀x:A. B[x],
function: x:A ⟶ B[x]
FDL editor aliases :
alt-one-path
Latex:
AtMostOnePath(A) ==
\mforall{}g,h:\mBbbN{} {}\mrightarrow{} T. \mforall{}n:\mBbbN{}. ((\mneg{}((g n) = (h n))) {}\mRightarrow{} (\mexists{}m:\mBbbN{}. (\mneg{}((\muparrow{}(A m g)) \mwedge{} (\muparrow{}(A m h))))))
Date html generated:
2019_06_20-PM-02_46_25
Last ObjectModification:
2019_06_06-PM-01_49_07
Theory : fan-theorem
Home
Index