Nuprl Definition : strictly-decreasing-on-interval
f[x] strictly-decreasing for x ∈ I ==  ∀x,y:{x:ℝ| x ∈ I} .  ((x < y) 
⇒ (f[y] < f[x]))
Definitions occuring in Statement : 
i-member: r ∈ I
, 
rless: x < y
, 
real: ℝ
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
set: {x:A| B[x]} 
Definitions occuring in definition : 
all: ∀x:A. B[x]
, 
set: {x:A| B[x]} 
, 
real: ℝ
, 
i-member: r ∈ I
, 
implies: P 
⇒ Q
, 
rless: x < y
FDL editor aliases : 
strictly-decreasing-on-interval
Latex:
f[x]  strictly-decreasing  for  x  \mmember{}  I  ==    \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  <  y)  {}\mRightarrow{}  (f[y]  <  f[x]))
Date html generated:
2016_05_18-AM-10_19_57
Last ObjectModification:
2015_09_23-AM-09_15_40
Theory : reals
Home
Index