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