:: by Agata Darmochwa{\l}

::

:: Received June 21, 1989

:: Copyright (c) 1990 Association of Mizar Users

begin

theorem :: TOPS_2:1

theorem :: TOPS_2:2

canceled;

theorem Th3: :: TOPS_2:3

for T being 1-sorted

for F being Subset-Family of T

for X being set st X c= F holds

X is Subset-Family of T

for F being Subset-Family of T

for X being set st X c= F holds

X is Subset-Family of T

proof end;

theorem :: TOPS_2:4

canceled;

theorem :: TOPS_2:5

proof end;

theorem :: TOPS_2:6

proof end;

theorem :: TOPS_2:7

canceled;

theorem :: TOPS_2:8

canceled;

theorem :: TOPS_2:9

canceled;

theorem :: TOPS_2:10

proof end;

theorem Th11: :: TOPS_2:11

proof end;

theorem Th12: :: TOPS_2:12

proof end;

Lm1: for T being 1-sorted

for F being Subset-Family of T st COMPLEMENT F is finite holds

F is finite

proof end;

theorem Th13: :: TOPS_2:13

for T being 1-sorted

for F being Subset-Family of T holds

( COMPLEMENT F is finite iff F is finite )

for F being Subset-Family of T holds

( COMPLEMENT F is finite iff F is finite )

proof end;

definition

let T be TopStruct ;

let F be Subset-Family of T;

attr F is open means :Def1: :: TOPS_2:def 1

for P being Subset of T st P in F holds

P is open ;

attr F is closed means :Def2: :: TOPS_2:def 2

for P being Subset of T st P in F holds

P is closed ;

end;
let F be Subset-Family of T;

attr F is open means :Def1: :: TOPS_2:def 1

for P being Subset of T st P in F holds

P is open ;

attr F is closed means :Def2: :: TOPS_2:def 2

for P being Subset of T st P in F holds

P is closed ;

:: deftheorem Def1 defines open TOPS_2:def 1 :

for T being TopStruct

for F being Subset-Family of T holds

( F is open iff for P being Subset of T st P in F holds

P is open );

:: deftheorem Def2 defines closed TOPS_2:def 2 :

for T being TopStruct

for F being Subset-Family of T holds

( F is closed iff for P being Subset of T st P in F holds

P is closed );

theorem :: TOPS_2:14

canceled;

theorem :: TOPS_2:15

canceled;

theorem Th16: :: TOPS_2:16

proof end;

theorem :: TOPS_2:17

proof end;

theorem :: TOPS_2:18

proof end;

theorem :: TOPS_2:19

proof end;

theorem :: TOPS_2:20

for T being TopStruct

for F, G being Subset-Family of T st F is open & G is open holds

F \/ G is open

for F, G being Subset-Family of T st F is open & G is open holds

F \/ G is open

proof end;

theorem :: TOPS_2:21

proof end;

theorem :: TOPS_2:22

proof end;

theorem :: TOPS_2:23

for T being TopStruct

for F, G being Subset-Family of T st F is closed & G is closed holds

F \/ G is closed

for F, G being Subset-Family of T st F is closed & G is closed holds

F \/ G is closed

proof end;

theorem :: TOPS_2:24

proof end;

theorem :: TOPS_2:25

proof end;

theorem Th26: :: TOPS_2:26

proof end;

theorem Th27: :: TOPS_2:27

for GX being TopSpace

for W being Subset-Family of GX st W is open & W is finite holds

meet W is open

for W being Subset-Family of GX st W is open & W is finite holds

meet W is open

proof end;

theorem :: TOPS_2:28

for GX being TopSpace

for W being Subset-Family of GX st W is closed & W is finite holds

union W is closed

for W being Subset-Family of GX st W is closed & W is finite holds

union W is closed

proof end;

theorem :: TOPS_2:29

proof end;

theorem :: TOPS_2:30

canceled;

theorem :: TOPS_2:31

for T being TopStruct

for A being SubSpace of T

for F being Subset-Family of A holds F is Subset-Family of T

for A being SubSpace of T

for F being Subset-Family of A holds F is Subset-Family of T

proof end;

theorem Th32: :: TOPS_2:32

for T being TopStruct

for A being SubSpace of T

for B being Subset of A holds

( B is open iff ex C being Subset of T st

( C is open & C /\ ([#] A) = B ) )

for A being SubSpace of T

for B being Subset of A holds

( B is open iff ex C being Subset of T st

( C is open & C /\ ([#] A) = B ) )

proof end;

theorem Th33: :: TOPS_2:33

for T being TopStruct

for Q being Subset of T

for A being SubSpace of T st Q is open holds

for P being Subset of A st P = Q holds

P is open

for Q being Subset of T

for A being SubSpace of T st Q is open holds

for P being Subset of A st P = Q holds

P is open

proof end;

theorem Th34: :: TOPS_2:34

for T being TopStruct

for Q being Subset of T

for A being SubSpace of T st Q is closed holds

for P being Subset of A st P = Q holds

P is closed

for Q being Subset of T

for A being SubSpace of T st Q is closed holds

for P being Subset of A st P = Q holds

P is closed

proof end;

theorem :: TOPS_2:35

for T being TopStruct

for F being Subset-Family of T

for A being SubSpace of T st F is open holds

for G being Subset-Family of A st G = F holds

G is open

for F being Subset-Family of T

for A being SubSpace of T st F is open holds

for G being Subset-Family of A st G = F holds

G is open

proof end;

theorem :: TOPS_2:36

for T being TopStruct

for F being Subset-Family of T

for A being SubSpace of T st F is closed holds

for G being Subset-Family of A st G = F holds

G is closed

for F being Subset-Family of T

for A being SubSpace of T st F is closed holds

for G being Subset-Family of A st G = F holds

G is closed

proof end;

theorem :: TOPS_2:37

canceled;

theorem Th38: :: TOPS_2:38

proof end;

definition

let T be TopStruct ;

let P be Subset of T;

let F be Subset-Family of T;

func F | P -> Subset-Family of (T | P) means :Def3: :: TOPS_2:def 3

for Q being Subset of (T | P) holds

( Q in it iff ex R being Subset of T st

( R in F & R /\ P = Q ) );

existence

ex b_{1} being Subset-Family of (T | P) st

for Q being Subset of (T | P) holds

( Q in b_{1} iff ex R being Subset of T st

( R in F & R /\ P = Q ) )

for b_{1}, b_{2} being Subset-Family of (T | P) st ( for Q being Subset of (T | P) holds

( Q in b_{1} iff ex R being Subset of T st

( R in F & R /\ P = Q ) ) ) & ( for Q being Subset of (T | P) holds

( Q in b_{2} iff ex R being Subset of T st

( R in F & R /\ P = Q ) ) ) holds

b_{1} = b_{2}

end;
let P be Subset of T;

let F be Subset-Family of T;

func F | P -> Subset-Family of (T | P) means :Def3: :: TOPS_2:def 3

for Q being Subset of (T | P) holds

( Q in it iff ex R being Subset of T st

( R in F & R /\ P = Q ) );

existence

ex b

for Q being Subset of (T | P) holds

( Q in b

( R in F & R /\ P = Q ) )

proof end;

uniqueness for b

( Q in b

( R in F & R /\ P = Q ) ) ) & ( for Q being Subset of (T | P) holds

( Q in b

( R in F & R /\ P = Q ) ) ) holds

b

proof end;

:: deftheorem Def3 defines | TOPS_2:def 3 :

for T being TopStruct

for P being Subset of T

for F being Subset-Family of T

for b

( b

( Q in b

( R in F & R /\ P = Q ) ) );

theorem :: TOPS_2:39

canceled;

theorem :: TOPS_2:40

for T being TopStruct

for M being Subset of T

for F, G being Subset-Family of T st F c= G holds

F | M c= G | M

for M being Subset of T

for F, G being Subset-Family of T st F c= G holds

F | M c= G | M

proof end;

theorem Th41: :: TOPS_2:41

for T being TopStruct

for Q, M being Subset of T

for F being Subset-Family of T st Q in F holds

Q /\ M in F | M

for Q, M being Subset of T

for F being Subset-Family of T st Q in F holds

Q /\ M in F | M

proof end;

theorem :: TOPS_2:42

for T being TopStruct

for Q, M being Subset of T

for F being Subset-Family of T st Q c= union F holds

Q /\ M c= union (F | M)

for Q, M being Subset of T

for F being Subset-Family of T st Q c= union F holds

Q /\ M c= union (F | M)

proof end;

theorem :: TOPS_2:43

for T being TopStruct

for M being Subset of T

for F being Subset-Family of T st M c= union F holds

M = union (F | M)

for M being Subset of T

for F being Subset-Family of T st M c= union F holds

M = union (F | M)

proof end;

theorem Th44: :: TOPS_2:44

for T being TopStruct

for M being Subset of T

for F being Subset-Family of T holds union (F | M) c= union F

for M being Subset of T

for F being Subset-Family of T holds union (F | M) c= union F

proof end;

theorem :: TOPS_2:45

for T being TopStruct

for M being Subset of T

for F being Subset-Family of T st M c= union (F | M) holds

M c= union F

for M being Subset of T

for F being Subset-Family of T st M c= union (F | M) holds

M c= union F

proof end;

theorem :: TOPS_2:46

for T being TopStruct

for M being Subset of T

for F being Subset-Family of T st F is finite holds

F | M is finite

for M being Subset of T

for F being Subset-Family of T st F is finite holds

F | M is finite

proof end;

theorem :: TOPS_2:47

for T being TopStruct

for M being Subset of T

for F being Subset-Family of T st F is open holds

F | M is open

for M being Subset of T

for F being Subset-Family of T st F is open holds

F | M is open

proof end;

theorem :: TOPS_2:48

for T being TopStruct

for M being Subset of T

for F being Subset-Family of T st F is closed holds

F | M is closed

for M being Subset of T

for F being Subset-Family of T st F is closed holds

F | M is closed

proof end;

theorem :: TOPS_2:49

for T being TopStruct

for A being SubSpace of T

for F being Subset-Family of A st F is open holds

ex G being Subset-Family of T st

( G is open & ( for AA being Subset of T st AA = [#] A holds

F = G | AA ) )

for A being SubSpace of T

for F being Subset-Family of A st F is open holds

ex G being Subset-Family of T st

( G is open & ( for AA being Subset of T st AA = [#] A holds

F = G | AA ) )

proof end;

theorem :: TOPS_2:50

for T being TopStruct

for P being Subset of T

for F being Subset-Family of T ex f being Function st

( dom f = F & rng f = F | P & ( for x being set st x in F holds

for Q being Subset of T st Q = x holds

f . x = Q /\ P ) )

for P being Subset of T

for F being Subset-Family of T ex f being Function st

( dom f = F & rng f = F | P & ( for x being set st x in F holds

for Q being Subset of T st Q = x holds

f . x = Q /\ P ) )

proof end;

theorem :: TOPS_2:51

canceled;

theorem Th52: :: TOPS_2:52

for X, Y being 1-sorted

for f being Function of X,Y st ( [#] Y = {} implies [#] X = {} ) holds

f " ([#] Y) = [#] X

for f being Function of X,Y st ( [#] Y = {} implies [#] X = {} ) holds

f " ([#] Y) = [#] X

proof end;

theorem :: TOPS_2:53

canceled;

theorem :: TOPS_2:54

for T being 1-sorted

for S being non empty 1-sorted

for f being Function of T,S

for H being Subset-Family of S holds (" f) .: H is Subset-Family of T

for S being non empty 1-sorted

for f being Function of T,S

for H being Subset-Family of S holds (" f) .: H is Subset-Family of T

proof end;

theorem Th55: :: TOPS_2:55

for X, Y being TopStruct

for f being Function of X,Y st ( [#] Y = {} implies [#] X = {} ) holds

( f is continuous iff for P being Subset of Y st P is open holds

f " P is open )

for f being Function of X,Y st ( [#] Y = {} implies [#] X = {} ) holds

( f is continuous iff for P being Subset of Y st P is open holds

f " P is open )

proof end;

theorem Th56: :: TOPS_2:56

for T, S being TopSpace

for f being Function of T,S holds

( f is continuous iff for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1) )

for f being Function of T,S holds

( f is continuous iff for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1) )

proof end;

theorem Th57: :: TOPS_2:57

for T being TopSpace

for S being non empty TopSpace

for f being Function of T,S holds

( f is continuous iff for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) )

for S being non empty TopSpace

for f being Function of T,S holds

( f is continuous iff for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) )

proof end;

theorem Th58: :: TOPS_2:58

for T, V being TopStruct

for S being non empty TopStruct

for f being Function of T,S

for g being Function of S,V st f is continuous & g is continuous holds

g * f is continuous

for S being non empty TopStruct

for f being Function of T,S

for g being Function of S,V st f is continuous & g is continuous holds

g * f is continuous

proof end;

theorem :: TOPS_2:59

for T being TopStruct

for S being non empty TopStruct

for f being Function of T,S

for H being Subset-Family of S st f is continuous & H is open holds

for F being Subset-Family of T st F = (" f) .: H holds

F is open

for S being non empty TopStruct

for f being Function of T,S

for H being Subset-Family of S st f is continuous & H is open holds

for F being Subset-Family of T st F = (" f) .: H holds

F is open

proof end;

theorem :: TOPS_2:60

for T, S being TopStruct

for f being Function of T,S

for H being Subset-Family of S st f is continuous & H is closed holds

for F being Subset-Family of T st F = (" f) .: H holds

F is closed

for f being Function of T,S

for H being Subset-Family of S st f is continuous & H is closed holds

for F being Subset-Family of T st F = (" f) .: H holds

F is closed

proof end;

definition

let S, T be set ;

let f be Function of S,T;

assume A1: ( rng f = T & f is one-to-one ) ;

func f /" -> Function of T,S equals :Def4: :: TOPS_2:def 4

f " ;

coherence

f " is Function of T,S by A1, FUNCT_2:31;

end;
let f be Function of S,T;

assume A1: ( rng f = T & f is one-to-one ) ;

func f /" -> Function of T,S equals :Def4: :: TOPS_2:def 4

f " ;

coherence

f " is Function of T,S by A1, FUNCT_2:31;

:: deftheorem Def4 defines /" TOPS_2:def 4 :

for S, T being set

for f being Function of S,T st rng f = T & f is one-to-one holds

f /" = f " ;

theorem :: TOPS_2:61

canceled;

theorem Th62: :: TOPS_2:62

for T being 1-sorted

for S being non empty 1-sorted

for f being Function of T,S st rng f = [#] S & f is one-to-one holds

( dom (f ") = [#] S & rng (f ") = [#] T )

for S being non empty 1-sorted

for f being Function of T,S st rng f = [#] S & f is one-to-one holds

( dom (f ") = [#] S & rng (f ") = [#] T )

proof end;

theorem Th63: :: TOPS_2:63

for T, S being 1-sorted

for f being Function of T,S st rng f = [#] S & f is one-to-one holds

f " is one-to-one

for f being Function of T,S st rng f = [#] S & f is one-to-one holds

f " is one-to-one

proof end;

theorem Th64: :: TOPS_2:64

for T being 1-sorted

for S being non empty 1-sorted

for f being Function of T,S st rng f = [#] S & f is one-to-one holds

(f ") " = f

for S being non empty 1-sorted

for f being Function of T,S st rng f = [#] S & f is one-to-one holds

(f ") " = f

proof end;

theorem :: TOPS_2:65

for T, S being 1-sorted

for f being Function of T,S st rng f = [#] S & f is one-to-one holds

( (f ") * f = id (dom f) & f * (f ") = id (rng f) )

for f being Function of T,S st rng f = [#] S & f is one-to-one holds

( (f ") * f = id (dom f) & f * (f ") = id (rng f) )

proof end;

theorem Th66: :: TOPS_2:66

for T being 1-sorted

for S, V being non empty 1-sorted

for f being Function of T,S

for g being Function of S,V st rng f = [#] S & f is one-to-one & dom g = [#] S & rng g = [#] V & g is one-to-one holds

(g * f) " = (f ") * (g ")

for S, V being non empty 1-sorted

for f being Function of T,S

for g being Function of S,V st rng f = [#] S & f is one-to-one & dom g = [#] S & rng g = [#] V & g is one-to-one holds

(g * f) " = (f ") * (g ")

proof end;

theorem Th67: :: TOPS_2:67

for T, S being 1-sorted

for f being Function of T,S

for P being Subset of T st rng f = [#] S & f is one-to-one holds

f .: P = (f ") " P

for f being Function of T,S

for P being Subset of T st rng f = [#] S & f is one-to-one holds

f .: P = (f ") " P

proof end;

theorem Th68: :: TOPS_2:68

for T, S being 1-sorted

for f being Function of T,S

for P1 being Subset of S st rng f = [#] S & f is one-to-one holds

f " P1 = (f ") .: P1

for f being Function of T,S

for P1 being Subset of S st rng f = [#] S & f is one-to-one holds

f " P1 = (f ") .: P1

proof end;

definition

let S, T be TopStruct ;

let f be Function of S,T;

attr f is being_homeomorphism means :Def5: :: TOPS_2:def 5

( dom f = [#] S & rng f = [#] T & f is one-to-one & f is continuous & f " is continuous );

end;
let f be Function of S,T;

attr f is being_homeomorphism means :Def5: :: TOPS_2:def 5

( dom f = [#] S & rng f = [#] T & f is one-to-one & f is continuous & f " is continuous );

:: deftheorem Def5 defines being_homeomorphism TOPS_2:def 5 :

for S, T being TopStruct

for f being Function of S,T holds

( f is being_homeomorphism iff ( dom f = [#] S & rng f = [#] T & f is one-to-one & f is continuous & f " is continuous ) );

theorem :: TOPS_2:69

canceled;

theorem :: TOPS_2:70

for T being TopStruct

for S being non empty TopStruct

for f being Function of T,S st f is being_homeomorphism holds

f " is being_homeomorphism

for S being non empty TopStruct

for f being Function of T,S st f is being_homeomorphism holds

f " is being_homeomorphism

proof end;

theorem :: TOPS_2:71

for T, S, V being non empty TopStruct

for f being Function of T,S

for g being Function of S,V st f is being_homeomorphism & g is being_homeomorphism holds

g * f is being_homeomorphism

for f being Function of T,S

for g being Function of S,V st f is being_homeomorphism & g is being_homeomorphism holds

g * f is being_homeomorphism

proof end;

theorem :: TOPS_2:72

for T being TopStruct

for S being non empty TopStruct

for f being Function of T,S holds

( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds

( P is closed iff f .: P is closed ) ) ) )

for S being non empty TopStruct

for f being Function of T,S holds

( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds

( P is closed iff f .: P is closed ) ) ) )

proof end;

theorem :: TOPS_2:73

for T being non empty TopSpace

for S being TopSpace

for f being Function of T,S holds

( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P1 being Subset of S holds f " (Cl P1) = Cl (f " P1) ) ) )

for S being TopSpace

for f being Function of T,S holds

( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P1 being Subset of S holds f " (Cl P1) = Cl (f " P1) ) ) )

proof end;

theorem :: TOPS_2:74

for T being TopSpace

for S being non empty TopSpace

for f being Function of T,S holds

( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ) ) )

for S being non empty TopSpace

for f being Function of T,S holds

( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ) ) )

proof end;

theorem Th75: :: TOPS_2:75

for X, Y being non empty TopSpace

for f being Function of X,Y

for A being Subset of X st f is continuous & A is connected holds

f .: A is connected

for f being Function of X,Y

for A being Subset of X st f is continuous & A is connected holds

f .: A is connected

proof end;

theorem :: TOPS_2:76

for S, T being non empty TopSpace

for f being Function of S,T

for A being Subset of T st f is being_homeomorphism & A is connected holds

f " A is connected

for f being Function of S,T

for A being Subset of T st f is being_homeomorphism & A is connected holds

f " A is connected

proof end;

begin

theorem :: TOPS_2:77

for GX being non empty TopSpace st ( for x, y being Point of GX ex GY being non empty TopSpace st

( GY is connected & ex f being Function of GY,GX st

( f is continuous & x in rng f & y in rng f ) ) ) holds

GX is connected

( GY is connected & ex f being Function of GY,GX st

( f is continuous & x in rng f & y in rng f ) ) ) holds

GX is connected

proof end;

theorem Th78: :: TOPS_2:78

proof end;

theorem :: TOPS_2:79

for X being TopStruct

for F being Subset-Family of X holds

( F is closed iff F c= COMPLEMENT the topology of X )

for F being Subset-Family of X holds

( F is closed iff F c= COMPLEMENT the topology of X )

proof end;

registration

let X be TopStruct ;

cluster the topology of X -> open ;

coherence

the topology of X is open by Th78;

cluster open Element of bool (bool the carrier of X);

existence

ex b_{1} being Subset-Family of X st b_{1} is open

end;
cluster the topology of X -> open ;

coherence

the topology of X is open by Th78;

cluster open Element of bool (bool the carrier of X);

existence

ex b

proof end;