Nuprl Definition : i-type
i-type(I) == n:ℕ+ × {r:ℝ| r ∈ i-approx(I;n)}
Definitions occuring in Statement :
i-approx: i-approx(I;n)
,
i-member: r ∈ I
,
real: ℝ
,
nat_plus: ℕ+
,
set: {x:A| B[x]}
,
product: x:A × B[x]
Definitions occuring in definition :
product: x:A × B[x]
,
nat_plus: ℕ+
,
set: {x:A| B[x]}
,
real: ℝ
,
i-member: r ∈ I
,
i-approx: i-approx(I;n)
FDL editor aliases :
i-type
i-type
Latex:
i-type(I) == n:\mBbbN{}\msupplus{} \mtimes{} \{r:\mBbbR{}| r \mmember{} i-approx(I;n)\}
Date html generated:
2016_05_18-AM-08_44_04
Last ObjectModification:
2015_09_23-AM-09_07_35
Theory : reals
Home
Index