Nuprl Definition : prod-metric-space
prod-metric-space(k;X) == <i:ℕk ⟶ (fst((X i))), prod-metric(k;λi.(snd((X i))))>
Definitions occuring in Statement :
prod-metric: prod-metric(k;d),
int_seg: {i..j-},
pi1: fst(t),
pi2: snd(t),
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
pair: <a, b>,
natural_number: $n
Definitions occuring in definition :
pair: <a, b>,
function: x:A ⟶ B[x],
int_seg: {i..j-},
natural_number: $n,
pi1: fst(t),
prod-metric: prod-metric(k;d),
lambda: λx.A[x],
pi2: snd(t),
apply: f a
FDL editor aliases :
prod-metric-space
Latex:
prod-metric-space(k;X) == <i:\mBbbN{}k {}\mrightarrow{} (fst((X i))), prod-metric(k;\mlambda{}i.(snd((X i))))>
Date html generated:
2019_10_29-AM-11_11_16
Last ObjectModification:
2019_10_02-AM-09_51_53
Theory : reals
Home
Index