Nuprl Definition : uniform-continuity-pi2
ucB(T;F;n) == ∀s:ℕn ⟶ 𝔹. ((F ext2Cantor(n;s;tt)) = (F ext2Cantor(n;s;ff)) ∈ T)
Definitions occuring in Statement :
ext2Cantor: ext2Cantor(n;f;d),
int_seg: {i..j-},
bfalse: ff,
btrue: tt,
bool: 𝔹,
all: ∀x:A. B[x],
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
int_seg: {i..j-},
natural_number: $n,
bool: 𝔹,
equal: s = t ∈ T,
btrue: tt,
apply: f a,
ext2Cantor: ext2Cantor(n;f;d),
bfalse: ff
FDL editor aliases :
uniform-continuity-pi2
Latex:
ucB(T;F;n) == \mforall{}s:\mBbbN{}n {}\mrightarrow{} \mBbbB{}. ((F ext2Cantor(n;s;tt)) = (F ext2Cantor(n;s;ff)))
Date html generated:
2016_05_14-PM-09_38_26
Last ObjectModification:
2015_09_22-PM-06_03_34
Theory : continuity
Home
Index