Nuprl Definition : streamless
streamless(T) == ∀f:ℕ ⟶ T. ∃i,j:ℕ. ((¬(i = j ∈ ℕ)) ∧ ((f i) = (f j) ∈ T))
Definitions occuring in Statement :
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
not: ¬A,
nat: ℕ,
equal: s = t ∈ T,
apply: f a
FDL editor aliases :
streamless
Latex:
streamless(T) == \mforall{}f:\mBbbN{} {}\mrightarrow{} T. \mexists{}i,j:\mBbbN{}. ((\mneg{}(i = j)) \mwedge{} ((f i) = (f j)))
Date html generated:
2016_05_15-PM-07_39_14
Last ObjectModification:
2015_09_23-AM-08_17_55
Theory : general
Home
Index