- Metric_Space::=
Net{
- points::Sets,
- X::=points.
Uses REAL_NUMBERS.
- METRIC::=
Net{
Uses REAL.
- S::Sets,
- d::S><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><Y)}.
- BALL::=
- sphere::=BALL.surface.
- open::={A:@X || for all a:A, some ε, if ε>0 then for all x:X(if d(a,x)<ε then x in A}.
- (metric)|-topology.OPEN(Set=>X) and Hausdorff.
- 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 ε:Real~Zero, abf n:Nat(d(x[n],lim(x))<ε.
- (above)|-For ε, /d(ε) in @(X,X).
UNIFORM_SPACE(X, uniformities=>{/d(ε) || for some ε } ).
- Cauchy::@Seq(X)={x || for all ε, some N:Nat0, all m,n:Nat0, if m,n>=N then d(x[m],x[n])<=ε}.
- (above)|-convergent==>Cauchy.
- complete::@=( Cauchy = convergent).
- For s:Seq(X), subsequences(s)::={s o n || for some n:Seq(Nat)(<(n))}.
- (above)|-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))<K d(x,y)} }.
- d::(continuous)X->Real.
- D::@X><@X->@Real=[X,Y]{d(x,y)||x:X, y:Y},
- diameter::@X=[A](sup(D(A><A))),
- d::@X><@X=[A,B](inf(D(A><B)),
- d::X><@X=[a,B]d({a},B),
- (above)|-diameter o close=diameter
- (above)|-for all A,B, d(close(A),B)=d(A,B)
- (above)|-for A:@X~{}, x,y:X (|d(x,A)-d(y,A)|<=d(x,y))
- (above)|-for A:@X, x in close(A) iff for some s:Seq(A)(lim s =x).
- (above)|-for s:Seq(X), x:X, x in adherences(s) iff for some n:Seq(Nat)(<(n) and lim(s o n)=x).
- (above)|-compact iff for all s:Seq(X)( some adherences(s)).
- (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)).
- (above)|-if complete, for Y:subspaces, Y is closed iff Y is complete.
- (above)|-if complete, for all F:Seq(closed~{}), if <==(F) and lim(diameter o F)=0 then |&F|=1.
- (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).
- (above)|- (Baire): if complete then for U:Seq(open & dense) then &U in dense.
}=::
MetricSpace.
- (above)|-For n:Nat, Metric_Space(X=>Real^n, d=>[x,y]sqrt(+[i]((x[i]-y[i])^2), |-complete ).
- (above)|-Metric_Space(X=>@#X , d=>[A,B](if A=B then 0 else 2^-(min o len(A~B|B~A)), |- complete).
- (above)|-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::=
Net{
X,Y::metric_space,
- f::X->Y,
- x::X.
- (above)|-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 ε, 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.
- (above)|-uniformally_continuous(X,Y)==>(Cont)X->Y.
- (above)|-For X:compact&M, Y:M, f:(cont)X->Y (f in uc).
- (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).
- (above)|-For X:M, X in compact iff X in complete and for all ε, some C:finite & cover(C:@balls(r=>ε)).
- ProductSpace::=
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.
Banach's Theorem.
- (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_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>>
- abf::="all but a finite number of", an unusual but useful quantifier.
. . . . . . . . . ( end of section Glossary) <<Contents | End>>
- 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>>
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 ]
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
- STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html
- 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).
- given::reason="I've been told that...", used to describe a problem.
- given::variable="I'll be given a value or object like this...", used to describe a problem.
- goal::theorem="The result I'm trying to prove right now".
- goal::variable="The value or object I'm trying to find or construct".
- 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.
- hyp::reason="I assumed this in my last Let/Case/Po/...".
- QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
- QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
- RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last
assumption (let) that you introduced.