Nuprl Definition : interval-vec
I^n ==  {v:ℝ^n| ∀i:ℕn. (v i ∈ I)} 
Definitions occuring in Statement : 
real-vec: ℝ^n
, 
i-member: r ∈ I
, 
int_seg: {i..j-}
, 
all: ∀x:A. B[x]
, 
set: {x:A| B[x]} 
, 
apply: f a
, 
natural_number: $n
Definitions occuring in definition : 
apply: f a
, 
i-member: r ∈ I
, 
natural_number: $n
, 
int_seg: {i..j-}
, 
all: ∀x:A. B[x]
, 
real-vec: ℝ^n
, 
set: {x:A| B[x]} 
FDL editor aliases : 
interval-vec
Latex:
I\^{}n  ==    \{v:\mBbbR{}\^{}n|  \mforall{}i:\mBbbN{}n.  (v  i  \mmember{}  I)\} 
Date html generated:
2018_07_29-AM-09_44_32
Last ObjectModification:
2018_07_02-AM-11_12_41
Theory : reals
Home
Index