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

# 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. |-
2. center::S,
3. radius::Real & Positive & nonzero,
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. |-
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{
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),...

}=::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>>

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.