:: Families of Subsets, Subspaces and Mappings in Topological Spaces
:: by Agata Darmochwa{\l}
::
:: Copyright (c) 1990-2018 Association of Mizar Users

::
:: A FAMILY OF SETS IN TOPOLOGICAL SPACES
::
theorem :: TOPS_2:1
for T being 1-sorted
for F being Subset-Family of T holds F c= bool ([#] T) ;

theorem Th2: :: TOPS_2:2
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
proof end;

theorem :: TOPS_2:3
for T being non empty 1-sorted
for F being Subset-Family of T st F is Cover of T holds
F <> {}
proof end;

theorem :: TOPS_2:4
for T being 1-sorted
for F, G being Subset-Family of T holds () \ () c= union (F \ G)
proof end;

theorem :: TOPS_2:5
for T being set
for F being Subset-Family of T holds
( F <> {} iff COMPLEMENT F <> {} )
proof end;

theorem Th6: :: TOPS_2:6
for T being set
for F being Subset-Family of T st F <> {} holds
meet () = () 
proof end;

theorem Th7: :: TOPS_2:7
for T being set
for F being Subset-Family of T st F <> {} holds
union () = (meet F)
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 Th8: :: TOPS_2:8
for T being 1-sorted
for F being Subset-Family of T holds
( COMPLEMENT F is finite iff F is finite )
proof end;

::
:: CLOSED AND OPEN FAMILIES
::
definition
let T be TopStruct ;
let F be Subset-Family of T;
attr F is open means :: TOPS_2:def 1
for P being Subset of T st P in F holds
P is open ;
attr F is closed means :: TOPS_2:def 2
for P being Subset of T st P in F holds
P is closed ;
end;

:: deftheorem 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 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 Th9: :: TOPS_2:9
for T being TopStruct
for F being Subset-Family of T holds
( F is closed iff COMPLEMENT F is open )
proof end;

theorem :: TOPS_2:10
for T being TopStruct
for F being Subset-Family of T holds
( F is open iff COMPLEMENT F is closed )
proof end;

theorem :: TOPS_2:11
for T being TopStruct
for F, G being Subset-Family of T st F c= G & G is open holds
F is open ;

theorem :: TOPS_2:12
for T being TopStruct
for F, G being Subset-Family of T st F c= G & G is closed holds
F is closed ;

theorem :: TOPS_2:13
for T being TopStruct
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:14
for T being TopStruct
for F, G being Subset-Family of T st F is open holds
F /\ G is open
proof end;

theorem :: TOPS_2:15
for T being TopStruct
for F, G being Subset-Family of T st F is open holds
F \ G is open
proof end;

theorem :: TOPS_2:16
for T being TopStruct
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:17
for T being TopStruct
for F, G being Subset-Family of T st F is closed holds
F /\ G is closed
proof end;

theorem :: TOPS_2:18
for T being TopStruct
for F, G being Subset-Family of T st F is closed holds
F \ G is closed
proof end;

theorem Th19: :: TOPS_2:19
for GX being TopSpace
for W being Subset-Family of GX st W is open holds
union W is open
proof end;

theorem Th20: :: TOPS_2:20
for GX being TopSpace
for W being Subset-Family of GX st W is open & W is finite holds
meet W is open
proof end;

theorem :: TOPS_2:21
for GX being TopSpace
for W being Subset-Family of GX st W is closed & W is finite holds
union W is closed
proof end;

theorem :: TOPS_2:22
for GX being TopSpace
for W being Subset-Family of GX st W is closed holds
meet W is closed
proof end;

::
:: SUBSPACES OF A TOPOLOGICAL SPACE
::
theorem :: TOPS_2:23
for T being TopStruct
for A being SubSpace of T
for F being Subset-Family of A holds F is Subset-Family of T
proof end;

theorem Th24: :: TOPS_2:24
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 ) )
proof end;

theorem Th25: :: TOPS_2:25
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
proof end;

theorem Th26: :: TOPS_2:26
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
proof end;

theorem :: TOPS_2:27
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 by Th25;

theorem :: TOPS_2:28
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 by Th26;

theorem Th29: :: TOPS_2:29
for T being TopStruct
for M, N being Subset of T holds M /\ N is Subset of (T | N)
proof end;

::
:: RESTRICTION OF A FAMILY
::
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 b1 being Subset-Family of (T | P) st
for Q being Subset of (T | P) holds
( Q in b1 iff ex R being Subset of T st
( R in F & R /\ P = Q ) )
proof end;
uniqueness
for b1, b2 being Subset-Family of (T | P) st ( for Q being Subset of (T | P) holds
( Q in b1 iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) ) & ( for Q being Subset of (T | P) holds
( Q in b2 iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) ) holds
b1 = b2
proof end;
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 b4 being Subset-Family of (T | P) holds
( b4 = F | P iff for Q being Subset of (T | P) holds
( Q in b4 iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) );

theorem :: TOPS_2:30
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
proof end;

theorem Th31: :: TOPS_2:31
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
proof end;

theorem :: TOPS_2:32
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)
proof end;

theorem :: TOPS_2:33
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)
proof end;

theorem Th34: :: TOPS_2:34
for T being TopStruct
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:35
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
proof end;

theorem :: TOPS_2:36
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
proof end;

theorem :: TOPS_2:37
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
proof end;

theorem :: TOPS_2:38
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
proof end;

theorem :: TOPS_2:39
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 ) )
proof end;

theorem :: TOPS_2:40
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 ) )
proof end;

theorem Th41: :: TOPS_2:41
for X, Y being 1-sorted
for f being Function of X,Y st ( [#] Y = {} implies [#] X = {} ) holds
f " ([#] Y) = [#] X
proof end;

theorem :: TOPS_2:42
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
proof end;

theorem Th43: :: TOPS_2:43
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 )
proof end;

theorem Th44: :: TOPS_2:44
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) )
proof end;

theorem Th45: :: TOPS_2:45
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) )
proof end;

theorem Th46: :: TOPS_2:46
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
proof end;

theorem :: TOPS_2:47
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
proof end;

theorem :: TOPS_2:48
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
proof end;

definition
let S, T be set ;
let f be Function of S,T;
assume A1: f is bijective ;
func f /" -> Function of T,S equals :Def4: :: TOPS_2:def 4
f " ;
coherence
f " is Function of T,S
proof end;
end;

:: deftheorem Def4 defines /" TOPS_2:def 4 :
for S, T being set
for f being Function of S,T st f is bijective holds
f /" = f " ;

notation
let S, T be set ;
let f be Function of S,T;
synonym f " for f /" ;
end;

theorem Th49: :: TOPS_2:49
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 )
proof end;

theorem Th50: :: TOPS_2:50
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
proof end;

theorem Th51: :: TOPS_2:51
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
proof end;

theorem :: TOPS_2:52
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) )
proof end;

theorem Th53: :: TOPS_2:53
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 ")
proof end;

theorem Th54: :: TOPS_2:54
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
proof end;

theorem Th55: :: TOPS_2:55
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
proof end;

::
:: HOMEOMORPHISM
::
definition
let S, T be TopStruct ;
let f be Function of S,T;
attr f is being_homeomorphism means :: TOPS_2:def 5
( dom f = [#] S & rng f = [#] T & f is one-to-one & f is continuous & f " is continuous );
end;

:: deftheorem 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:56
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 by ;

theorem :: TOPS_2:57
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
proof end;

theorem :: TOPS_2:58
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 ) ) ) )
proof end;

theorem :: TOPS_2:59
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) ) ) )
proof end;

theorem :: TOPS_2:60
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) ) ) )
proof end;

theorem Th61: :: TOPS_2:61
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
proof end;

theorem :: TOPS_2:62
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
proof end;

theorem :: TOPS_2:63
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
proof end;

theorem Th64: :: TOPS_2:64
for X being TopStruct
for F being Subset-Family of X holds
( F is open iff F c= the topology of X )
proof end;

theorem :: TOPS_2:65
for X being TopStruct
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 Th64;
cluster open for Subset-Family of X;
existence
ex b1 being Subset-Family of X st b1 is open
proof end;
end;