Net{

There are many approaches to defining a topology of a space, differing only in their appeal to different people. This one starts with the 'closure' operation. Others follow.

To close a set is to add points to it - those points that we decide are infinitely close to or on the edge of the set. The result of 'close' is a 'closed' set.

Space::Sets -- the set of points in the space.
X::=Space, abbreviation.
0::@X={x:X||false} -a local abbreviation for the empty subset of the space.
CLOSURE::=
Net{
1. close::(monoid)(@X,|,0)->(@X,|,0),
2. (close)|-close(A|B) = close(A)|close(B).
3. (close)|-close(0) = 0.
4. |- (idempclose): close;close=close,
5. |- (closeadds): For all A:@X(A==>close(A)),
6. close::X->@X=close({(_)}), overloaded to handle points.
7. For x:X, Y:@X, x in close(Y)=x is close to or inside Y.
  A set is is dense if and only if closing it fills the space.
8. dense::={A:@X||close(A)=X},
  Closed sets arise from the closure operation:
9. closed::@@X,
10. |-closed={A:@X || close(X)=X },
11. (above)|-closed in closed_family(X),
12. |-close(A)=min{C:closed||A==>C}.
13. open::@@X. If we removes a closed set from a space then we remove its "edge" as well an leave behind a set that is said to be open.
14. |-open={A:@X|| X~A in closed},
15. (above)|-open in open_family(X).
  Two special topologies -- the discrete and indiscrete topologies:
16. discrete::@= (open=@X).
17. indiscrete::@= (open={0,X}).
  Note well: there are sets that are both open and closed, and there can be sets that are neither open or closed.
18. interior::@X->@X,
19. |-For all A:@X,
20. interior(A)=(|(open & @A)).
21. exterior::@X->@X,
22. exterior(A)=(interior(X~A)).
23. boundary::@X->@X,
24. boundary(A)=(X~interior(A)~exterior(A)).
25. (above)|-For all A:@X, X>=={interior(A), boundary(A), exterior(A)}.
26. (above)|-dense={A:@X||exterior(A)={}}.
27. |-For all A:@S, boundary(A)=boundary(S~A).
28. open_neighbourhoods::X->@@X.
29. |-For x:X,
30. open_neighbourhoods(x)={G:open||x in G},
31. neighbourhoods::X->@@X.
32. neighbourhoods(x)={N:@X||for some G:open( p in G ==> N)},
33. fundamental_neighbourhoods::X->@@X.
34. fundamental_neighbourhoods(x)={F:@@X ||for all V:open_neighbourhoods(x), some W:F (W==>V)}.
35. For A:@X, neighbourhoods(A)={N:@X||for some G:open(A==>G==>N)}.
36. separated::=Hausdorf, pronounced a litle like "housed off".
37. Hausdorff::@=Any two points can be separated.
38. |-Hausdorff iff for x,y:X, if x<>y then for some N1:n(x), N2:n(y) ( N1&N2 ).
39. |-if Hausdorff then for x:X, {x} in closed.
40. basis::@@X.
41. |-For all x:X ({V:basis||x in V}in fundamental_neighbourhoods(x)).
42. For p:X, W:@^S, for x:near[p](W(x)) ::=for some N:neighbourhoods(p), all x:N (W(x)).
43. inside::@(@X,@X)= (1st)==>interior((2nd)).
44. (above)|-if A inside B then some C:open(A==>C==>B).
45. (above)|-neighbourhoods=[x:X]{A:@X||{x}inside A}.
46. (above)|-open={A||A inside X}.
  
  Isolated points of a Space.
47. For A:@X, isolated(A)::={x:X||some N:neighbourhood(x)( A&N={x})}.
  
  Subspaces of X.
48. For Y:@Y, Y subspace X::= Y in subspaces.
49. subspaces::={Y:@X||Y.open={G&Y:@Y||G:X.open}.
50. (above)|-for Y:subspaces(Y.open in open_family(Y)).
51. compact::@.
52. compact::=Hausdorff and for all oc:open & covers(X), some foc:FiniteSubsets(oc)(foc in covers(X)),
53. (above)|-for all oc:open & covers(X), some foc:FiniteSubsets(oc)(foc in covers(X)) iff for all cc:closed & covers(X), some fcc:FiniteSubsets(fc)(fcc in covers(X)).
54. compact_sets::={A:@X||A subspace X and compact.A}.
  
  Limits in X.
55. For Y:Sets, β:filter_bases(Y), f:Y->X, f ->[β] l::=for all V:(X.neighbourhoods)(l), some b:β. (f(B)==>V), f ->[β] l::= f tends to l along β in space X. Cf. LIMITS later. connected:@. ?? connected::=no(open & covers(X)).?.
}=::CLOSURE.
Text Book Definitions.
There are other ways to define a topology. The text book starting point is from either a closed or an open family of subsets of the space S.
CLOSED::=
Net{
1. S::Sets,
2. closed::closed_family(S).
3. |-TOPOLOGY and Net{close:=[A]min{B:closed||A==>B} }.
}=::CLOSED.
OPEN::=
Net{
1. S::Sets,
2. open::open_family(S), Duality:|-CLOSED and Net{ closed:={S~G:@X||G in Open} }.
  Once you have got a set of points and the set of all open sets than you have determined the shape of the space. Knowing the closed sets determines the shape as well. As an example suppose that the whole space S>=={A,B} and both A,B in open, then clearly its possible for a sequence to be in A and for its limit to jump to B and vice versa - the space is not connected.
}=::OPEN.
INSIDE::=
Net{
1. X::Sets,
2. inside::@(@X,@X),
3. |-0 inside 0 and X inside X,
4. |-(==>;inside;==>) ==>inside,
5. |-inside ==> ( ==>),
6. |-For all A,B,C,D:@X(if A inside B and C inside D then A&C inside B&D),
7. |-For all A,B:array I of @X (if for all i:I(A(i) inside B(i)) then |A inside |B).
8. (above)|-CLOSED and Net{ closed:={B||(X~B) inside (X~B)} }.
}=::INSIDE.
INTERIOR::=
Net{
1. X::Sets,
2. interior::(monoid)(@X,&,0)->(@X,&,0).
3. |-interior;interior=interior.
4. |-For all A:@X(interior(A)==>A).
5. |-interior(X)=X.
6. (above)|-OPEN(open=>{G:@X||int(G)=G}).
}=::INTERIOR.
NEIGHBOURHOODS::=
Net{
1. X::Sets,
2. neighbourhoods::X->(@@X). n:=neighborhoods.
3. |-For all x:X( (n(x),&) in semigroup).
4. |-For all p:X, N:n(p)( p in N).
5. |-For all p,N, some G:n(p)&@N, all g:G(N in n(g)).
6. (above)|-OPEN(open=>{G:@S||for all x:G(G in n(x)}).
}=::NEIGHBOURHOODS.
FINENESS::=
Net{
1. |-X1 finer X2 iff for G:open.X1(G in open.X2) [click here if you can fill this hole]
  }.
LIMITS::=
Net{
1. |-{n..*||n:Nat} in filter_bases(Nat),
2. base for limits of sequences.
3. |-For X:Spaces, x:X, neighbourhoods(x) in filter_bases(X).
4. Used for limits of functions at a point.
5. |-For X:Space, Y:@X, x0:close(Y), {Y&V||V in neighbourhoods(x0)}in filters(Y).
6. For Y:Sets, β:filter_bases(Y), X:Spaces, f:Y->X, f ->[β,X] l::=for all V:(X.neighbourhoods)(l), some b:β.
7. (f(B)==>V), f ->[β,X] l ::= f tends to l along β in space X. Note. When there is no ambiguity the space (,X) is omitted).
8. For X:Spaces, a:Nat->X, lim[n->oo]a[n] ::= the [l](a->[{n..||n:Nat}]l),
9. l=lim[n->oo]a[n] iff for all V:neighbourhoods(l), abf n (a[n] in V). (note. 'oo' is an arbitrary symbol, not necesarily a value in Nat, and 'abf' is 'short for 'all but a finite number of'.).
10. For X,Y:Spaces, f:X->Y, lim[x->x0]f(x) ::= the [l](f->[X.neighbourhoods(x0)]l),
11. |-l=[x->x0]f(x) iff for all V:Y.neighbourhoods(l), some W:X.neighbouhoods(x0), (if x in W then f(x) in V).
  Similarly:
12. {[x0..x0+ε)||ε>0} is a filter_base for lim[x->x0,x>=0]f(x).
  Notice that {x0..x0+ε)||ε>=0} is not because [x0..x0) =0).
13. {[a..)||a:Real} is a filter_base for lim[x->oo]f(x).
14. For x0:close(Y), {Y&V||V in nieghbourhoods(x0)} is a base for lim[x->x0,x:Y].
15. For X,Y:Spaces, x0:X, y0:Y, f:X->Y,
16. W:X.fundamental_neighbourhoods(x0), V:Y.fundamental_neighbourhoods(y0),
17. y0=lim[x->x0]f(x) iff for all v:V, some w:W(f(w)==>V).
  Hausdorff spaces have unique limits (if any).
18. (above)|-For Y:Sets, β:filter_bases(Y), X:Spaces and Hausdorff, f:Y->X,
19. 0..1 l (f ->[β] l). The limit of a function does not depend on what it does initially (where the filter is widest) but what happens later (inside the narrower confines of the filter):
20. (above)|-For Y:Sets, β:filter_bases(Y), X:Spaces, f:Y->X, B:β,
21. γ={B&A||A in β},
22. f ->[β] l iff f ->[γ] l.
  
  Adherence/Accumulation points.
  Even though a function may not have a unique limit (at a point, as x->oo,...) it may still get close to one or more points while avoiding coming to a unique limit. For example fun[n]((-1)^n(1+1/n)) in Seq(Real) tends to accumulate at or adhere to both -1 and +1.
23. For X,Z:Spaces, f:X->Z, Y:@X, x0:close(Y), β={Y&V||V in neighbourhoods(x0)}, z0:Z, adherence_value[β](f):={z:Z ||for all V:neighbourhood(z), W:neighbourhoods(x0), (f(W&Y) & Y)},
24. |-For X:sets, Y:Spaces and Hausdorff, β:filter_bases(X), f:X->Y,
25. f ->[β] l iff l= the adherence_value[β](f).
26. |-For X:sets, Y:Spaces and Hausdorff, β:filter_bases(X), f:X->Y,
27. adherence_value[β](f)=&{close(f(B))||B in β}.
}=::LIMITS.
Continuity
CONTINUITY::=
Net{
1. arrow::{->,>->,...}, X,Y::Spaces,
2. p::X.
  (Cont)X arrow Y::={f:(X arrow Y || for all A:@X( f(close(A))==>close(f(A) )}, This is not the text book definition but is equivalent to it.
3. \swashC(X,Y)::=(Cont)(X->Y) - This notation is often used in text books.
  A easily understood definition of continuity at a point is that the limit of the function at that point is the value of the function at that point:
4. For all f:(Continuous(x0))X arrow Y iff f:X arrow Y and f ->[x0] f(x0).
  In the vernacular: If it looks like its going there, then it gets there.. (Continuous(p))::=Continuous at p, (C(p)) ::=(Continuous(p)),
  (Continuous(p))X arrow Y={f:X arrow Y||for all A:@X( if p in X.close(A) then f(p) in f(A))},
5. (above)|-for all p:X (Cont)==>(Cont(p)).
6. (above)|-for all f:X->Y, (f in Continuous iff for all A,B:@Y(if A inside B then /f(A) inside /f(B)).
7. (above)|-for f:X->Y, f in continuous iff for all x, some F:fundamental_neighbourhoods(f(x)), all V:F(/f(V)in open_neighbourhoods(x)).
8. (above)|-For f:(Cont)X->Y,
9. For all G:open(Y) (/f(G) in open(X))
10. and for all G:closed(Y) (/f(G) in closed(X))
11. and for all A:@X (f(close(A))==>close(f(A)))
12. and for all B:@Y (close(/f(B))==>/f(close(f(B)))
13. and for all B:@Y (/f(interior(B))==>interior(/f(B)))
14. and for all A,B:@Y (if A inside B then /f(A) inside /f(B))
15. and ? for all A:connected(Y) (f(A) is connected)
16. and for all A:compact(X) (f(A) in compact(Y) )
17. and for all x:X, N:neighbourhoods(f(x)) (/f(N) in neighbourhoods(x)).
18. (above)|-For f:>X->Y, g:Y->Z, if f,g in Cont then f;g in Cont.
19. (above)|-Id(X) is (Cont)X->X.
20. (above)|-CATEGORY(Spaces,Continuous).
21. |-For f:>X->Y, g:Y->Z, if f in Cont(x0), g in Cont(f(x0)) then f;g in Cont(x0).
}=::CONTINUITY.
Morphisms
TOPOLOGICAL_MORPHISMS::=
Net{
1. For X, Y::Spaces,
2. arrow::Arrows,
3. F::@@X|@@Y, (F is typically open, closed,...),
  (F)X arrow Y ::={f:X arrow Y|| for all A:@X(if A in F then f(A) in F)}.
  (topological) ::=(Closed)&(Continuous).
4. homeomorphisms(X,Y)::={f:(Cont)X---Y || /f in (Cont)Y---X}.
5. Hom(X,Y)::=homeomorphisms(X,Y).
6. (above)|-homeomorphism<>Continuous && (1)-(1).
7. (above)|-For F:X---Y, f in Hom(X,Y)
8. iff f,/f in Cont
9. iff (for all A:@X(X in open iff f(X) in open)
10. iff (for all A:@X(X in close iff f(X) in close).
11. (above)|-homeomorphisms(X,Y)=(topological)X---Y.
12. (above)|-if compact then homeomorphisms=continuous & (1)-(1).
  Example - stereographic projection of a sphere onto a plane.
13. ()|-for p:sphere[n], (topological) (sphere[n]~{p})---R^(n).
}=::TOPOLOGICAL_MORPHISMS.
Subspaces and relative topologies
SUBSPACE::=
Net{
1. |-TOPOLOGY(X),
2. Subset::@X.
3. Y:=Subset.
4. |-TOPOLOGY(Y,close=>[B:@Y](Y & X.close(B))
5. (above)|-Y.open={G&Y||G:X.open}.
}=::SUBSPACE.
For X:Space, subspaces(X)::=SUBSPACE.Subset.
|-for X:Spaces, Y:subspaces(X)(Y.open in open_family(Y) and Y ==> X).
For X,Y:Spaces, (topology)X==>Y::=X in subspaces(Y).
Many properties are propagated from space to subspace:
|-For X,Y, (topology)X==>Y,
X.closed={C&X||C:Y.closed},
X.neighbourhoods=[x]{N&X||N:Y.neighbourhoods(x)},
if Y.Hausdorff then then X.Hausdorff,
For I:Sets, β:fbase(I), f:I->X, l:X(f ->[β,X]l iff f->[β,Y]l).
For T:Spaces, f:T->X(f in Continous(X) iff continuous(Y),
Id(X) in (continuous.Y)X->Y.
|-For X:Spaces, Y:@X, Y.discrete iff for all y:Y(y in isolated.Y).
|-subspace in Transitive(Spaces).

Embedding.
??|-(topology)X-->Y iff for some Z((topology)X---Z and Z subspace Y).

Quotient Topology.
QUOTIENT_TOPOLOGY::=
Net{
1. |-TOPOLOGY(X).
2. R::equivalence_relations(X). Glueing things together
3. φ::=[x]x/R. quotient_topology is the finest topology with φ in (continous)X>==X/R.
4. |-TOPOLOGY(X=>X/R,open=>{A||A./φ in open(X)},...).
}=::QUOTIENT_TOPOLOGY.
Basies.
TOPOLOGICAL_BASIS::=
Net{
1. S::Sets,
2. basis::covers(S), 0 in basis.
3. For all A:finite(basis)(&A in basis).
4. generate_open::=[B:@@S]{|(A) || A:@B}.
5. |-OPEN and Net{open=generate_open(basis)}.
}=::TOPOLOGICAL_BASIS.
.
ORDERED_TOPOLOGY::=
Net{
1. |-Toset(X,<=).
2. |-TOPOLOGICAL_BASIS,
3. |-basis={u..v ~{u,v}||u,v:S}.
4. (above)|-for all u,v(u..v=close(u..v not {u,v})).
}=::ORDERED_TOPOLOGY.
ADIC::=
Net{
1. p::Integer,
2. S::=Integer,
3. |-neighbourhoods=[n]{n+s*p^r||r:Nat0, s:Integer
  [click here if you can fill this hole]
}=::ADIC.
INITIAL::=
Net{
1. I::Sets,
2. Y::I->TOPOLOGY,
3. X::Set,
4. Z::TOPOLOGY.
5. For i:I, f[i]::X->Y(i), α:coarsest topology on X such that for all i(f[i] in continuous).
6. |-for all g:(continuous???).
  [click here if you can fill this hole]
}=::INITIAL.
FINAL::=
Net{
1. I::Sets,
2. Y::I->TOPOLOGY,
3. X::Set,
4. Z::TOPOLOGY.
5. For i:I, f[i]::Y(i)->X, β:finest topology on X such that for all i(f[i] in continuous).
6. |-β={U||for all i (/(f[i])in open)}.
}=::FINAL.
Product of Spaces
1. PRODUCT_2_SPACES::=
  Net{
  1. |-TOPOLOGY(X).
  2. |-TOPOLOGY(Y).
  3. (above)|-TOPOLOGY(X><Y, open=>{U:@(X><Y)||some eo:elementary(open)(U= |(eo))}).
  }=::PRODUCT_SPACE.
  In general when we need a topological space that is the product of a number (including infinitely many) spaces then we use the INITIAL topology that makes all the projection functions continuous. The Initial topology is also known as the Tychonoff Product Topology.
. . . . . . . . . ( end of section Product of Spaces) <<Contents | End>>

Sums of Spaces
SUM_2_SPACES::=
Net{
1. |-TOPOLOGY(X).
2. |-TOPOLOGY(Y).
3. |-{X,Y} in open & partitions(X|Y).
}=::SUM_SPACE.

. . . . . . . . . ( end of section Topology) <<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

Contents

Topology

History

Uses Families of Sets

Spaces

Definition of a Topology

Isolated points of a Space.

Subspaces of X.

Limits in X.

Text Book Definitions.

Adherence/Accumulation points.

Continuity

Morphisms

Subspaces and relative topologies

Embedding.

Quotient Topology.

Basies.

Product of Spaces

Sums of Spaces

Notes on MATHS Notation

Notes on the Underlying Logic of MATHS

Glossary

End