[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / math_92_Metric_Spaces
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Mon Dec 13 14:22:33 PST 2010

Contents


    Metric Spaces

    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. metric_space::=$ Metric_Space. M:=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,
      2. X::1..p->$ Metric_space,

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

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


      5. (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 [socket symbol] 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

    Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

    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 might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

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

    Notes on the Underlying Logic of MATHS

    The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

    For a more rigorous description of the standard notations see

  1. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

    Glossary

  2. above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
  3. given::reason="I've been told that...", used to describe a problem.
  4. given::variable="I'll be given a value or object like this...", used to describe a problem.
  5. goal::theorem="The result I'm trying to prove right now".
  6. goal::variable="The value or object I'm trying to find or construct".
  7. let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
  8. hyp::reason="I assumed this in my last Let/Case/Po/...".
  9. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  10. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  11. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.

End