.Open Metric Spaces Metric_Space::=Net{ points::Sets, X::=points. Uses REAL_NUMBERS. METRIC::=Net{ Uses REAL. S::Sets, d::S>[0..). |- (m1): for x:S, d(x,x)=0. |- (m2): for x,y:S, d(x,y)=d(y,x). (Thanks to $PeterK for correcting the error that used to be above). |- (m3): for x,y,z:S, d(x,y)+d(y,z)<=d(x,z). non_Archimedian::@=( max(d(x,y),d(y,z))>=d(y,z) ). }=::METRIC. |- (metric): METRIC(S=>points). non_Archimedian::@=$METRIC(S=>points, non_Archimedian). subspaces::={Metric_Space(X=>Y, d=>d') || for some Y:@X, d'=d o (Y>0 then for all x:X(if d(a,x)<\epsilon then x in A}. (metric)|- topology.OPEN(Set=>X) and Hausdorff. . Convergence in metric space CONVERGENCE::=Net{ |- $METRIC. a::Seq(S), c::S, |-For all r>0,$abf i(a[i] in BALL(center=>c, radius=>r).$open), For any radius, all but but a finite number of points in the sequence lie inside a ball of the radius about the center c. }=::CONVERGENCE. lim::Seq(X)<>->X, convergent::=cor(lim), (lim, convergent)|-For all x:convergent, all \epsilon:Real~Zero,$abf n:Nat(d(x[n],lim(x))<\epsilon. ()|-For \epsilon, /d(\epsilon) in @(X,X). UNIFORM_SPACE(X, uniformities=>{/d(\epsilon) || for some \epsilon } ). Cauchy::@Seq(X)={x || for all \epsilon, some N:Nat0, all m,n:Nat0, if m,n>=N then d(x[m],x[n])<=\epsilon}. ()|- convergent==>Cauchy. complete::@=( Cauchy = convergent). For s:Seq(X), subsequences(s) ::={s o n || for some n:Seq(Nat)(<(n))}. ()|- For s:Cauchy, s':subsequequences(s), if s in convergent then lim(s)=lim(s'). contraction::@(X->X)={f || for some K:[0..1), all x,y:X(d(f(x),f(y))Real. D::@X><@X->@Real=[X,Y]{d(x,y)||x:X, y:Y}, diameter::@X=[A](sup(D(A><@X=[A,B](inf(D(A><@X=[a,B]d({a},B), ()|- diameter o close=diameter ()|- for all A,B, d(close(A),B)=d(A,B) ()|- for A:@X~{}, x,y:X (|d(x,A)-d(y,A)|<=d(x,y)) ()|- for A:@X, x in close(A) iff for some s:Seq(A)(lim s =x). ()|- for s:Seq(X), x:X, x in adherences(s) iff for some n:Seq(Nat)(<(n) and lim(s o n)=x). ()|-compact iff for all s:Seq(X)( some adherences(s)). ()|- for all A:@X, close(A) in compact iff for all s:Seq(A), some n:Seq(Nat)(X, if for all \epsilon:(0..), some B:F(diameter(B)<=\epsilon) then one lim[x+>F]f(x). . Baire's Theorem. ()|-(Baire): if complete then for U:Seq(open & dense) then &U in dense. }=::MetricSpace. . Examples ()|- For n:Nat, Metric_Space(X=>Real^n, d=>[x,y]sqrt(+[i]((x[i]-y[i])^2), |-complete ). ()|- Metric_Space(X=>@#X , d=>[A,B](if A=B then 0 else 2^-(min o len(A~B|B~A)), |- complete). ()|- For Y:Metric_Space, Metric_Space(X=>T->Y , d=>[f,g]max[t:T](d(f(t), g(t)) ). metric_space::=Metric_Space. M:=metric_space. subspace::=[X,Y:M]X in subspaces(Y). . Continuity Continuity::=Net{ X,Y::metric_space, f::X->Y, x::X. ()|- f in continuous(x) iff for all s:convergent(X)( f(lim s)=lim(f o s) ). }=::Continuity. For X,Y:M, uniformly_continuous::={f:X->Y || for all \epsilon, some \delta, for all x1,x2:X, if d(x1,x2)<=\delta then d(f(x1),f(x2))<=\epsilon). This means that there is an \epsilon that does not vary with x1, x2. Normal continuity allows this. ()|- uniformally_continuous(X,Y)==>(Cont)X->Y. ()|- For X:compact&M, Y:M, f:(cont)X->Y (f in uc). ()|- For X:M, X':dense(X), Y:metric_space and {|-complete}, f':(uc)X'->Y (for one f:(cont)X->Y(f o X' =f') and the f:(cont)X->Y(f o X'=f') in uc). ()|- For X:M, X in compact iff X in complete and for all \epsilon, some C:finite & cover(C:@balls(r=>\epsilon)). . Products of Metric Spaces ProductSpace::=Net{ p::Nat, X::1..p->Metric_space, product_metric::=[x,y:X](max[i:1..p]d(x[i],y[i])) product_space::=MetricSpace(>product_metric). ()|- If for i:1..p (X[i].complete) then product.complete. }=::ProductSpace. . Normed Space Here the distance between points is depends only on the realtive positions of the points. More precisely the distance of points from a special origin defines a norm function that in in turn defines the distance between points. NORM::=Net{ X::metric_space & additive_group, For all x,y,z:X(d(x,y)=d(z+x,z+y)). norm::=d(x,0). abs::=norm. |- d(x,y)=abs(x-y). }=::NORM. . Method of Successive Approximations Banach's Theorem. ()|- For all X:M and Net{complete}, f:contraction (for one a:X(f(a)=a)and for all x:X (lim[n]f^n(x)=the a(a=f(a))) .Close Metric Spaces .Open Uniform spaces UNIFORM_SPACE::=Net{ A generalization of metric spaces. Set:Sets, uniformity:@@(X,X),... .Hole }=::UNIFORM_SPACE. .Close Uniform Spaces .Open Glossary abf::="all but a finite number of", an unusual but useful quantifier. .Close Glossary .Open Credits and Links PeterK::=http://www.itee.uq.edu.au/~kootsoop, Peter J. Kootsookos, who noted by EMail that $m2 of the definition of$METRIC was in error and corrected it October 4th 2002. .Close Credits and Links