1. Metric_Space::=
   Net{

   1. points::Sets,
   2. X::=points.

      Uses REAL_NUMBERS.

   3. METRIC::=
      Net{

      Uses REAL.
      1. S::Sets,
      2. d::S><S->[0..).
         
      3. |- (m1): for x:S, d(x,x)=0.
         
      4. |- (m2): for x,y:S, d(x,y)=d(y,x). (Thanks to PeterK for correcting the error that used to be above).
         
      5. |- (m3): for x,y,z:S, d(x,y)+d(y,z)<=d(x,z).

      6. non_Archimedian::@=( max(d(x,y),d(y,z))>=d(y,z) ).

      
      }=::METRIC.

      
      

   4. |- (metric): METRIC(S=>points).
   5. non_Archimedian::@=METRIC(S=>points, non_Archimedian).

   6. subspaces::={Metric_Space(X=>Y, d=>d') || for some Y:@X, d'=d o (Y><Y)}.

   7. BALL::=
      Net{

      
      
      1. |-METRIC,
      2. center::S,
      3. radius::Real & Positive & nonzero,
      4. closed::={x:S||d(x,center)<=radius},
      5. surface::={x:S||d(x,center)=radius},
      6. open::=close~surface

      
      }=::BALL.
   8. sphere::=BALL.surface.

   9. open::={A:@X || for all a:A, some ε, if ε>0 then for all x:X(if d(a,x)<ε then x in A}.

      
      

   10. (metric)|-topology.OPEN(Set=>X) and Hausdorff.

       Convergence in metric space

   11. CONVERGENCE::=
       Net{

       
       
       1. |-METRIC.
       2. a::Seq(S),
       3. c::S,
          
       4. |-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.

   12. lim::Seq(X)<>->X,
   13. convergent::=cor(lim),
       
   14. (lim, convergent)|-For all x:convergent, all ε:Real~Zero, abf n:Nat(d(x[n],lim(x))<ε.

       
       

   15. (above)|-For ε, /d(ε) in @(X,X).

       UNIFORM_SPACE(X, uniformities=>{/d(ε) || for some ε } ).

   16. Cauchy::@Seq(X)={x || for all ε, some N:Nat0, all m,n:Nat0, if m,n>=N then d(x[m],x[n])<=ε}.

       
       

   17. (above)|-convergent==>Cauchy.

   18. complete::@=( Cauchy = convergent).

   19. For s:Seq(X), subsequences(s)::={s o n || for some n:Seq(Nat)(<(n))}.

       
       

   20. (above)|-For s:Cauchy, s':subsequequences(s), if s in convergent then lim(s)=lim(s').

   21. contraction::@(X->X)={f || for some K:[0..1), all x,y:X(d(f(x),f(y))<K d(x,y)} }.

   22. d::(continuous)X->Real.

   23. D::@X><@X->@Real=[X,Y]{d(x,y)||x:X, y:Y},
   24. diameter::@X=[A](sup(D(A><A))),
   25. d::@X><@X=[A,B](inf(D(A><B)),
   26. d::X><@X=[a,B]d({a},B),
       
   27. (above)|-diameter o close=diameter
       
   28. (above)|-for all A,B, d(close(A),B)=d(A,B)
       
   29. (above)|-for A:@X~{}, x,y:X (|d(x,A)-d(y,A)|<=d(x,y))

       
       

   30. (above)|-for A:@X, x in close(A) iff for some s:Seq(A)(lim s =x).

       
       

   31. (above)|-for s:Seq(X), x:X, x in adherences(s) iff for some n:Seq(Nat)(<(n) and lim(s o n)=x).

       
       

   32. (above)|-compact iff for all s:Seq(X)( some adherences(s)).

       
       

   33. (above)|-for all A:@X, close(A) in compact iff for all s:Seq(A), some n:Seq(Nat)(<n and one lim(s o n)).

       
       

   34. (above)|-if complete, for Y:subspaces, Y is closed iff Y is complete.

       
       

   35. (above)|-if complete, for all F:Seq(closed~{}), if <==(F) and lim(diameter o F)=0 then |&F|=1.

       
       

   36. (above)|-if complete, for T:Sets, F:filter_bases(T), f:T->X, if for all ε:(0..), some B:F(diameter(B)<=ε) then one lim[x+>F]f(x).

       Baire's Theorem.

       
       
   37. (above)|- (Baire): if complete then for U:Seq(open & dense) then &U in dense.

   
   }=::MetricSpace.

   Examples

   
   
2. (above)|-For n:Nat, Metric_Space(X=>Real^n, d=>[x,y]sqrt(+[i]((x[i]-y[i])^2), |-complete ).
   
3. (above)|-Metric_Space(X=>@#X , d=>[A,B](if A=B then 0 else 2^-(min o len(A~B|B~A)), |- complete).
   
4. (above)|-For Y:$ Metric_Space, Metric_Space(X=>T->Y , d=>[f,g]max[t:T](d(f(t), g(t)) ).
5. M::=metric_space::=$ Metric_Space.
6. subspace::=[X,Y:M]X in subspaces(Y).

   Continuity

7. Continuity::=
   Net{

   X,Y::metric_space,
   1. f::X->Y,
   2. x::X.
      
   3. (above)|-f in continuous(x) iff for all s:convergent(X)( f(lim s)=lim(f o s) ).

   
   }=::Continuity.

8. For X,Y:M, uniformly_continuous::={f:X->Y || for all ε, some δ, for all x1,x2:X, if d(x1,x2)<=δ then d(f(x1),f(x2))<=ε).

   This means that there is an ε that does not vary with x1, x2. Normal continuity allows this.

   
   

9. (above)|-uniformally_continuous(X,Y)==>(Cont)X->Y.

   
   

10. (above)|-For X:compact&M, Y:M, f:(cont)X->Y (f in uc).

    
    

11. (above)|-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).

    
    

12. (above)|-For X:M, X in compact iff X in complete and for all ε, some C:finite & cover(C:@balls(r=>ε)).

    Products of Metric Spaces

13. ProductSpace::=
    Net{

    1. p::Nat, X::1..p->$ Metric_space,

    2. product_metric::=[x,y:X](max[i:1..p]d(x[i],y[i]))

    3. product_space::=$ MetricSpace(><X, d=>product_metric).

       
       

    4. (above)|-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.
14. NORM::=
    Net{

    1. X::metric_space & additive_group,
    2. For all x,y,z:X(d(x,y)=d(z+x,z+y)).

    3. norm::=d(x,0).
    4. abs::=norm.
       
    5. |-d(x,y)=abs(x-y).

    
    }=::NORM.

    Method of Successive Approximations

    Banach's Theorem.
    

15. (above)|-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)))

. . . . . . . . . ( end of section Metric Spaces) <<Contents | End>>

Uniform spaces

1. UNIFORM_SPACE::=
   Net{

   A generalization of metric spaces. Set:Sets, uniformity:@@(X,X),...

   [click here if you can fill this hole]

   
   }=::UNIFORM_SPACE.

. . . . . . . . . ( end of section Uniform Spaces) <<Contents | End>>

Glossary

1. abf::="all but a finite number of", an unusual but useful quantifier.

. . . . . . . . . ( end of section Glossary) <<Contents | End>>

Credits and Links

1. PeterK::= See 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.

. . . . . . . . . ( end of section Credits and Links) <<Contents | End>>

Notes on MATHS Notation

Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle = Net{radius:Positive Real, center:Point}.

For a complete listing of pages in this part of my site by topic see [ home.html ]

Notes on the Underlying Logic of MATHS

For a more rigorous description of the standard notations see