Nuprl Definition : member-closure
y ∈ closure(A) == ∃x:ℕ ⟶ ℝ. (lim n→∞.x[n] = y ∧ (∀n:ℕ. (A x[n])))
Definitions occuring in Statement :
converges-to: lim n→∞.x[n] = y,
real: ℝ,
nat: ℕ,
so_apply: x[s],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x]
Definitions occuring in definition :
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
real: ℝ,
and: P ∧ Q,
converges-to: lim n→∞.x[n] = y,
all: ∀x:A. B[x],
nat: ℕ,
apply: f a,
so_apply: x[s]
FDL editor aliases :
member-closure
member-closure
Latex:
y \mmember{} closure(A) == \mexists{}x:\mBbbN{} {}\mrightarrow{} \mBbbR{}. (lim n\mrightarrow{}\minfty{}.x[n] = y \mwedge{} (\mforall{}n:\mBbbN{}. (A x[n])))
Date html generated:
2016_05_18-AM-08_10_41
Last ObjectModification:
2015_09_23-AM-09_04_29
Theory : reals
Home
Index