Nuprl Definition : interval-fun
interval-fun(I;J;x.f[x]) == (∀x:{x:ℝ| x ∈ I} . (f[x] ∈ J)) ∧ (∀x,y:{x:ℝ| x ∈ I} . f[x] = f[y] supposing x = y)
Definitions occuring in Statement :
i-member: r ∈ I,
req: x = y,
real: ℝ,
uimplies: b supposing a,
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]}
FDL editor aliases :
interval-fun
Latex:
interval-fun(I;J;x.f[x]) ==
(\mforall{}x:\{x:\mBbbR{}| x \mmember{} I\} . (f[x] \mmember{} J)) \mwedge{} (\mforall{}x,y:\{x:\mBbbR{}| x \mmember{} I\} . f[x] = f[y] supposing x = y)
Date html generated:
2020_05_20-PM-00_24_49
Last ObjectModification:
2019_12_05-PM-05_45_43
Theory : reals
Home
Index