:: by Agata Darmochwa{\l} and Yatsuka Nakamura

::

:: Received November 21, 1991

:: Copyright (c) 1991-2012 Association of Mizar Users

begin

:: Topological spaces

theorem :: TOPMETR:1

for T being TopStruct

for F being Subset-Family of T holds

( F is Cover of T iff the carrier of T c= union F ) by SETFAM_1:def 11;

for F being Subset-Family of T holds

( F is Cover of T iff the carrier of T c= union F ) by SETFAM_1:def 11;

theorem Th3: :: TOPMETR:3

for T being TopSpace

for A, B being SubSpace of T st the carrier of A c= the carrier of B holds

A is SubSpace of B

for A, B being SubSpace of T st the carrier of A c= the carrier of B holds

A is SubSpace of B

proof end;

theorem Th4: :: TOPMETR:4

for T being non empty TopSpace

for P, Q being Subset of T holds

( T | P is SubSpace of T | (P \/ Q) & T | Q is SubSpace of T | (P \/ Q) )

for P, Q being Subset of T holds

( T | P is SubSpace of T | (P \/ Q) & T | Q is SubSpace of T | (P \/ Q) )

proof end;

theorem :: TOPMETR:5

for T being non empty TopSpace

for p being Point of T

for P being non empty Subset of T st p in P holds

for Q being a_neighborhood of p

for p9 being Point of (T | P)

for Q9 being Subset of (T | P) st Q9 = Q /\ P & p9 = p holds

Q9 is a_neighborhood of p9

for p being Point of T

for P being non empty Subset of T st p in P holds

for Q being a_neighborhood of p

for p9 being Point of (T | P)

for Q9 being Subset of (T | P) st Q9 = Q /\ P & p9 = p holds

Q9 is a_neighborhood of p9

proof end;

theorem :: TOPMETR:6

for A, B being TopSpace

for f being Function of A,B

for C being Subset of B st f is continuous holds

for h being Function of A,(B | C) st h = f holds

h is continuous

for f being Function of A,B

for C being Subset of B st f is continuous holds

for h being Function of A,(B | C) st h = f holds

h is continuous

proof end;

theorem :: TOPMETR:7

for X being TopStruct

for Y being non empty TopStruct

for K0 being Subset of X

for f being Function of X,Y

for g being Function of (X | K0),Y st f is continuous & g = f | K0 holds

g is continuous

for Y being non empty TopStruct

for K0 being Subset of X

for f being Function of X,Y

for g being Function of (X | K0),Y st f is continuous & g = f | K0 holds

g is continuous

proof end;

Lm1: for M being MetrSpace holds MetrStruct(# the carrier of M, the distance of M #) is MetrSpace

proof end;

definition

let M be MetrSpace;

ex b_{1} being MetrSpace st

( the carrier of b_{1} c= the carrier of M & ( for x, y being Point of b_{1} holds the distance of b_{1} . (x,y) = the distance of M . (x,y) ) )

end;
mode SubSpace of M -> MetrSpace means :Def1: :: TOPMETR:def 1

( the carrier of it c= the carrier of M & ( for x, y being Point of it holds the distance of it . (x,y) = the distance of M . (x,y) ) );

existence ( the carrier of it c= the carrier of M & ( for x, y being Point of it holds the distance of it . (x,y) = the distance of M . (x,y) ) );

ex b

( the carrier of b

proof end;

:: deftheorem Def1 defines SubSpace TOPMETR:def 1 :

for M, b_{2} being MetrSpace holds

( b_{2} is SubSpace of M iff ( the carrier of b_{2} c= the carrier of M & ( for x, y being Point of b_{2} holds the distance of b_{2} . (x,y) = the distance of M . (x,y) ) ) );

for M, b

( b

registration
end;

registration

let M be non empty MetrSpace;

existence

ex b_{1} being SubSpace of M st

( b_{1} is strict & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

theorem Th8: :: TOPMETR:8

for M being non empty MetrSpace

for A being non empty SubSpace of M

for p being Point of A holds p is Point of M

for A being non empty SubSpace of M

for p being Point of A holds p is Point of M

proof end;

theorem Th9: :: TOPMETR:9

for r being real number

for M being MetrSpace

for A being SubSpace of M

for x being Point of M

for x9 being Point of A st x = x9 holds

Ball (x9,r) = (Ball (x,r)) /\ the carrier of A

for M being MetrSpace

for A being SubSpace of M

for x being Point of M

for x9 being Point of A st x = x9 holds

Ball (x9,r) = (Ball (x,r)) /\ the carrier of A

proof end;

definition

let M be non empty MetrSpace;

let A be non empty Subset of M;

existence

ex b_{1} being strict SubSpace of M st the carrier of b_{1} = A

for b_{1}, b_{2} being strict SubSpace of M st the carrier of b_{1} = A & the carrier of b_{2} = A holds

b_{1} = b_{2}

end;
let A be non empty Subset of M;

existence

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines | TOPMETR:def 2 :

for M being non empty MetrSpace

for A being non empty Subset of M

for b_{3} being strict SubSpace of M holds

( b_{3} = M | A iff the carrier of b_{3} = A );

for M being non empty MetrSpace

for A being non empty Subset of M

for b

( b

registration
end;

definition

let a, b be real number ;

assume A1: a <= b ;

ex b_{1} being non empty strict SubSpace of RealSpace st

for P being non empty Subset of RealSpace st P = [.a,b.] holds

b_{1} = RealSpace | P

for b_{1}, b_{2} being non empty strict SubSpace of RealSpace st ( for P being non empty Subset of RealSpace st P = [.a,b.] holds

b_{1} = RealSpace | P ) & ( for P being non empty Subset of RealSpace st P = [.a,b.] holds

b_{2} = RealSpace | P ) holds

b_{1} = b_{2}

end;
assume A1: a <= b ;

func Closed-Interval-MSpace (a,b) -> non empty strict SubSpace of RealSpace means :Def3: :: TOPMETR:def 3

for P being non empty Subset of RealSpace st P = [.a,b.] holds

it = RealSpace | P;

existence for P being non empty Subset of RealSpace st P = [.a,b.] holds

it = RealSpace | P;

ex b

for P being non empty Subset of RealSpace st P = [.a,b.] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines Closed-Interval-MSpace TOPMETR:def 3 :

for a, b being real number st a <= b holds

for b_{3} being non empty strict SubSpace of RealSpace holds

( b_{3} = Closed-Interval-MSpace (a,b) iff for P being non empty Subset of RealSpace st P = [.a,b.] holds

b_{3} = RealSpace | P );

for a, b being real number st a <= b holds

for b

( b

b

definition

let M be MetrStruct ;

let F be Subset-Family of M;

end;
let F be Subset-Family of M;

attr F is being_ball-family means :Def4: :: TOPMETR:def 4

for P being set st P in F holds

ex p being Point of M ex r being Real st P = Ball (p,r);

for P being set st P in F holds

ex p being Point of M ex r being Real st P = Ball (p,r);

:: deftheorem Def4 defines being_ball-family TOPMETR:def 4 :

for M being MetrStruct

for F being Subset-Family of M holds

( F is being_ball-family iff for P being set st P in F holds

ex p being Point of M ex r being Real st P = Ball (p,r) );

for M being MetrStruct

for F being Subset-Family of M holds

( F is being_ball-family iff for P being set st P in F holds

ex p being Point of M ex r being Real st P = Ball (p,r) );

:: Metric spaces and topology

theorem :: TOPMETR:12

for M being MetrStruct holds

( the carrier of M = the carrier of (TopSpaceMetr M) & the topology of (TopSpaceMetr M) = Family_open_set M ) ;

( the carrier of M = the carrier of (TopSpaceMetr M) & the topology of (TopSpaceMetr M) = Family_open_set M ) ;

theorem Th13: :: TOPMETR:13

for M being non empty MetrSpace

for A being non empty SubSpace of M holds TopSpaceMetr A is SubSpace of TopSpaceMetr M

for A being non empty SubSpace of M holds TopSpaceMetr A is SubSpace of TopSpaceMetr M

proof end;

theorem Th14: :: TOPMETR:14

for r being real number

for M being triangle MetrStruct

for p being Point of M

for P being Subset of (TopSpaceMetr M) st P = Ball (p,r) holds

P is open

for M being triangle MetrStruct

for p being Point of M

for P being Subset of (TopSpaceMetr M) st P = Ball (p,r) holds

P is open

proof end;

theorem Th15: :: TOPMETR:15

for M being non empty MetrSpace

for P being Subset of (TopSpaceMetr M) holds

( P is open iff for p being Point of M st p in P holds

ex r being real number st

( r > 0 & Ball (p,r) c= P ) )

for P being Subset of (TopSpaceMetr M) holds

( P is open iff for p being Point of M st p in P holds

ex r being real number st

( r > 0 & Ball (p,r) c= P ) )

proof end;

definition
end;

:: deftheorem Def5 defines compact TOPMETR:def 5 :

for M being MetrStruct holds

( M is compact iff TopSpaceMetr M is compact );

for M being MetrStruct holds

( M is compact iff TopSpaceMetr M is compact );

theorem :: TOPMETR:16

for M being non empty MetrSpace holds

( M is compact iff for F being Subset-Family of M st F is being_ball-family & F is Cover of M holds

ex G being Subset-Family of M st

( G c= F & G is Cover of M & G is finite ) )

( M is compact iff for F being Subset-Family of M st F is being_ball-family & F is Cover of M holds

ex G being Subset-Family of M st

( G c= F & G is Cover of M & G is finite ) )

proof end;

:: REAL as topological space

registration
end;

definition

let a, b be real number ;

TopSpaceMetr (Closed-Interval-MSpace (a,b)) is non empty strict SubSpace of R^1 by Th13;

end;
func Closed-Interval-TSpace (a,b) -> non empty strict SubSpace of R^1 equals :: TOPMETR:def 7

TopSpaceMetr (Closed-Interval-MSpace (a,b));

coherence TopSpaceMetr (Closed-Interval-MSpace (a,b));

TopSpaceMetr (Closed-Interval-MSpace (a,b)) is non empty strict SubSpace of R^1 by Th13;

:: deftheorem defines Closed-Interval-TSpace TOPMETR:def 7 :

for a, b being real number holds Closed-Interval-TSpace (a,b) = TopSpaceMetr (Closed-Interval-MSpace (a,b));

for a, b being real number holds Closed-Interval-TSpace (a,b) = TopSpaceMetr (Closed-Interval-MSpace (a,b));

theorem Th19: :: TOPMETR:19

for a, b being real number st a <= b holds

for P being Subset of R^1 st P = [.a,b.] holds

Closed-Interval-TSpace (a,b) = R^1 | P

for P being Subset of R^1 st P = [.a,b.] holds

Closed-Interval-TSpace (a,b) = R^1 | P

proof end;

definition

:: original: I[01]

redefine func I[01] -> SubSpace of R^1 ;

coherence

I[01] is SubSpace of R^1 by Th20;

end;
redefine func I[01] -> SubSpace of R^1 ;

coherence

I[01] is SubSpace of R^1 by Th20;

Lm2: for a, b, r being real number st r >= 0 & a + r <= b holds

a <= b

proof end;

theorem :: TOPMETR:21

for f being Function of R^1,R^1 st ex a, b being Real st

for x being Real holds f . x = (a * x) + b holds

f is continuous

for x being Real holds f . x = (a * x) + b holds

f is continuous

proof end;

::Moved from JORDAN16:6, AK 20.02.2006

theorem :: TOPMETR:22

for T being non empty TopSpace

for A, B being Subset of T st A c= B holds

T | A is SubSpace of T | B

for A, B being Subset of T st A c= B holds

T | A is SubSpace of T | B

proof end;

::Moved from JGRAPH_5:6,7, AK 20.02.2006

theorem Th23: :: TOPMETR:23

for a, b, d, e being real number

for B being Subset of (Closed-Interval-TSpace (d,e)) st d <= a & a <= b & b <= e & B = [.a,b.] holds

Closed-Interval-TSpace (a,b) = (Closed-Interval-TSpace (d,e)) | B

for B being Subset of (Closed-Interval-TSpace (d,e)) st d <= a & a <= b & b <= e & B = [.a,b.] holds

Closed-Interval-TSpace (a,b) = (Closed-Interval-TSpace (d,e)) | B

proof end;

theorem :: TOPMETR:24

:: from BORSUK_6, 2007.04.08, A,T.

:: deftheorem Def8 defines real-membered TOPMETR:def 8 :

for T being 1-sorted holds

( T is real-membered iff the carrier of T is real-membered );

for T being 1-sorted holds

( T is real-membered iff the carrier of T is real-membered );

:: from RCOMP_3, 2007.04.08, A,T.

registration
end;

registration
end;

:: from BORSUK_6, 2010.03.07, A.T.

:: from BORSUK_6, 2010.05.31, A.K.

registration

existence

ex b_{1} being TopSpace st

( b_{1} is strict & not b_{1} is empty & b_{1} is real-membered )

end;
ex b

( b

proof end;

registration

let T be real-membered TopStruct ;

coherence

for b_{1} being SubSpace of T holds b_{1} is real-membered

end;
coherence

for b

proof end;

:: from EUCLID_9, 2010.10.05, A.K.

registration
end;