:: Bases and Refinements of Topologies
:: by Grzegorz Bancerek
::
:: Received March 9, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users


scheme :: YELLOW_9:sch 1
FraenkelInvolution{ F1() -> non empty set , F2() -> Subset of F1(), F3() -> Subset of F1(), F4( set ) -> Element of F1() } :
F2() = { F4(a) where a is Element of F1() : a in F3() }
provided
A1: F3() = { F4(a) where a is Element of F1() : a in F2() } and
A2: for a being Element of F1() holds F4(F4(a)) = a
proof end;

scheme :: YELLOW_9:sch 2
FraenkelComplement1{ F1() -> non empty RelStr , F2() -> Subset-Family of F1(), F3() -> set , F4( set ) -> Subset of F1() } :
COMPLEMENT F2() = { (F4(a) `) where a is Element of F1() : a in F3() }
provided
A1: F2() = { F4(a) where a is Element of F1() : a in F3() }
proof end;

scheme :: YELLOW_9:sch 3
FraenkelComplement2{ F1() -> non empty RelStr , F2() -> Subset-Family of F1(), F3() -> set , F4( set ) -> Subset of F1() } :
COMPLEMENT F2() = { F4(a) where a is Element of F1() : a in F3() }
provided
A1: F2() = { (F4(a) `) where a is Element of F1() : a in F3() }
proof end;

theorem :: YELLOW_9:1
for R being non empty RelStr
for x, y being Element of R holds
( y in (uparrow x) ` iff not x <= y )
proof end;

scheme :: YELLOW_9:sch 4
ABC{ F1() -> TopSpace, F2( set ) -> set , F3() -> Function, P1[ set ] } :
F3() " (union { F2(x) where x is Subset of F1() : P1[x] } ) = union { (F3() " F2(y)) where y is Subset of F1() : P1[y] }
proof end;

theorem Th2: :: YELLOW_9:2
for S being 1-sorted
for T being non empty 1-sorted
for f being Function of S,T
for X being Subset of T holds (f " X) ` = f " (X `)
proof end;

theorem Th3: :: YELLOW_9:3
for T being 1-sorted
for F being Subset-Family of T holds COMPLEMENT F = { (a `) where a is Subset of T : a in F }
proof end;

theorem Th4: :: YELLOW_9:4
for R being non empty RelStr
for F being Subset of R holds
( uparrow F = union { (uparrow x) where x is Element of R : x in F } & downarrow F = union { (downarrow x) where x is Element of R : x in F } )
proof end;

theorem :: YELLOW_9:5
for R being non empty RelStr
for A being Subset-Family of R
for F being Subset of R st A = { ((uparrow x) `) where x is Element of R : x in F } holds
Intersect A = (uparrow F) `
proof end;

registration
cluster non empty 1 -element correct reflexive transitive antisymmetric with_suprema with_infima complete strict for TopRelStr ;
existence
ex b1 being TopLattice st
( b1 is strict & b1 is complete & b1 is 1 -element )
proof end;
end;

registration
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric upper-bounded RelStr ;
cluster non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V27( the carrier of S) quasi_total infs-preserving for Element of bool [: the carrier of S, the carrier of T:];
existence
ex b1 being Function of S,T st b1 is infs-preserving
proof end;
end;

registration
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric lower-bounded RelStr ;
cluster non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V27( the carrier of S) quasi_total sups-preserving for Element of bool [: the carrier of S, the carrier of T:];
existence
ex b1 being Function of S,T st b1 is sups-preserving
proof end;
end;

definition
let R, S be 1-sorted ;
assume A1: the carrier of S c= the carrier of R ;
A2: dom (id the carrier of S) = the carrier of S ;
A3: rng (id the carrier of S) = the carrier of S ;
func incl (S,R) -> Function of S,R equals :Def1: :: YELLOW_9:def 1
 id the carrier of S;
coherence
id the carrier of S is Function of S,R by A1, A2, A3, FUNCT_2:2;
end;

:: deftheorem Def1 defines incl YELLOW_9:def 1 :
for R, S being 1-sorted st the carrier of S c= the carrier of R holds
incl (S,R) = id the carrier of S;

registration
let R be non empty RelStr ;
let S be non empty SubRelStr of R;
cluster incl (S,R) -> monotone ;
coherence
incl (S,R) is monotone
proof end;
end;

definition
let R be non empty RelStr ;
let X be non empty Subset of R;
func X +id -> non empty strict NetStr over R equals :: YELLOW_9:def 2
(incl ((subrelstr X),R)) * ((subrelstr X) +id);
coherence
(incl ((subrelstr X),R)) * ((subrelstr X) +id) is non empty strict NetStr over R ;
func X opp+id -> non empty strict NetStr over R equals :: YELLOW_9:def 3
(incl ((subrelstr X),R)) * ((subrelstr X) opp+id);
coherence
(incl ((subrelstr X),R)) * ((subrelstr X) opp+id) is non empty strict NetStr over R ;
end;

:: deftheorem defines +id YELLOW_9:def 2 :
for R being non empty RelStr
for X being non empty Subset of R holds X +id = (incl ((subrelstr X),R)) * ((subrelstr X) +id);

:: deftheorem defines opp+id YELLOW_9:def 3 :
for R being non empty RelStr
for X being non empty Subset of R holds X opp+id = (incl ((subrelstr X),R)) * ((subrelstr X) opp+id);

theorem :: YELLOW_9:6
for R being non empty RelStr
for X being non empty Subset of R holds
( the carrier of (X +id) = X & X +id is full SubRelStr of R & ( for x being Element of (X +id) holds (X +id) . x = x ) )
proof end;

theorem :: YELLOW_9:7
for R being non empty RelStr
for X being non empty Subset of R holds
( the carrier of (X opp+id) = X & X opp+id is full SubRelStr of R opp & ( for x being Element of (X opp+id) holds (X opp+id) . x = x ) )
proof end;

registration
let R be non empty reflexive RelStr ;
let X be non empty Subset of R;
cluster X +id -> non empty reflexive strict ;
coherence
X +id is reflexive ;
cluster X opp+id -> non empty reflexive strict ;
coherence
X opp+id is reflexive ;
end;

registration
let R be non empty transitive RelStr ;
let X be non empty Subset of R;
cluster X +id -> non empty transitive strict ;
coherence
X +id is transitive ;
cluster X opp+id -> non empty transitive strict ;
coherence
X opp+id is transitive ;
end;

registration
let R be non empty reflexive RelStr ;
let I be directed Subset of R;
cluster subrelstr I -> directed ;
coherence
subrelstr I is directed
proof end;
end;

registration
let R be non empty reflexive RelStr ;
let I be non empty directed Subset of R;
cluster I +id -> non empty strict directed ;
coherence
I +id is directed ;
end;

registration
let R be non empty reflexive RelStr ;
let F be non empty filtered Subset of R;
cluster (subrelstr F) opp+id -> directed ;
coherence
(subrelstr F) opp+id is directed
proof end;
end;

registration
let R be non empty reflexive RelStr ;
let F be non empty filtered Subset of R;
cluster F opp+id -> non empty strict directed ;
coherence
F opp+id is directed ;
end;

theorem Th8: :: YELLOW_9:8
for T being TopSpace st T is empty holds
the topology of T = {{}}
proof end;

theorem Th9: :: YELLOW_9:9
for T being 1 -element TopSpace holds
( the topology of T = bool the carrier of T & ( for x being Point of T holds
( the carrier of T = {x} & the topology of T = {{},{x}} ) ) )
proof end;

theorem :: YELLOW_9:10
for T being 1 -element TopSpace holds
( { the carrier of T} is Basis of T & {} is prebasis of T & {{}} is prebasis of T )
proof end;

theorem Th11: :: YELLOW_9:11
for X, Y being set
for A being Subset-Family of X st A = {Y} holds
( FinMeetCl A = {Y,X} & UniCl A = {Y,{}} )
proof end;

theorem :: YELLOW_9:12
for X being set
for A, B being Subset-Family of X st ( A = B \/ {X} or B = A \ {X} ) holds
Intersect A = Intersect B
proof end;

theorem :: YELLOW_9:13
for X being set
for A, B being Subset-Family of X st ( A = B \/ {X} or B = A \ {X} ) holds
FinMeetCl A = FinMeetCl B
proof end;

theorem Th14: :: YELLOW_9:14
for X being set
for A being Subset-Family of X st X in A holds
for x being set holds
( x in FinMeetCl A iff ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y ) )
proof end;

theorem Th15: :: YELLOW_9:15
for X being set
for A being Subset-Family of X holds UniCl (UniCl A) = UniCl A
proof end;

theorem Th16: :: YELLOW_9:16
for X being set
for A being empty Subset-Family of X holds UniCl A = {{}}
proof end;

theorem Th17: :: YELLOW_9:17
for X being set
for A being empty Subset-Family of X holds FinMeetCl A = {X}
proof end;

theorem Th18: :: YELLOW_9:18
for X being set
for A being Subset-Family of X st A = {{},X} holds
( UniCl A = A & FinMeetCl A = A )
proof end;

theorem Th19: :: YELLOW_9:19
for X, Y being set
for A being Subset-Family of X
for B being Subset-Family of Y holds
( ( A c= B implies UniCl A c= UniCl B ) & ( A = B implies UniCl A = UniCl B ) )
proof end;

theorem Th20: :: YELLOW_9:20
for X, Y being set
for A being Subset-Family of X
for B being Subset-Family of Y st A = B & X in A holds
FinMeetCl B = {Y} \/ (FinMeetCl A)
proof end;

theorem Th21: :: YELLOW_9:21
for X being set
for A being Subset-Family of X holds UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A)
proof end;

theorem Th22: :: YELLOW_9:22
for T being TopSpace
for K being Subset-Family of T holds
( the topology of T = UniCl K iff K is Basis of T )
proof end;

theorem Th23: :: YELLOW_9:23
for T being TopSpace
for K being Subset-Family of T holds
( K is prebasis of T iff FinMeetCl K is Basis of T )
proof end;

theorem Th24: :: YELLOW_9:24
for T being non empty TopSpace
for B being Subset-Family of T st UniCl B is prebasis of T holds
B is prebasis of T
proof end;

theorem Th25: :: YELLOW_9:25
for T1, T2 being TopSpace
for B being Basis of T1 st the carrier of T1 = the carrier of T2 & B is Basis of T2 holds
the topology of T1 = the topology of T2
proof end;

theorem Th26: :: YELLOW_9:26
for T1, T2 being TopSpace
for P being prebasis of T1 st the carrier of T1 = the carrier of T2 & P is prebasis of T2 holds
the topology of T1 = the topology of T2
proof end;

theorem :: YELLOW_9:27
for T being TopSpace
for K being Basis of T holds
( K is open & K is prebasis of T ) ;

theorem :: YELLOW_9:28
for T being TopSpace
for K being prebasis of T holds K is open ;

theorem Th29: :: YELLOW_9:29
for T being non empty TopSpace
for B being prebasis of T holds B \/ { the carrier of T} is prebasis of T
proof end;

theorem :: YELLOW_9:30
for T being TopSpace
for B being Basis of T holds B \/ { the carrier of T} is Basis of T
proof end;

theorem Th31: :: YELLOW_9:31
for T being TopSpace
for B being Basis of T
for A being Subset of T holds
( A is open iff for p being Point of T st p in A holds
ex a being Subset of T st
( a in B & p in a & a c= A ) )
proof end;

theorem Th32: :: YELLOW_9:32
for T being TopSpace
for B being Subset-Family of T st B c= the topology of T & ( for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in B & p in a & a c= A ) ) holds
B is Basis of T
proof end;

theorem Th33: :: YELLOW_9:33
for S being TopSpace
for T being non empty TopSpace
for K being Basis of T
for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " (A `) is closed )
proof end;

theorem :: YELLOW_9:34
for S being TopSpace
for T being non empty TopSpace
for K being Basis of T
for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " A is open )
proof end;

theorem Th35: :: YELLOW_9:35
for S being TopSpace
for T being non empty TopSpace
for K being prebasis of T
for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " (A `) is closed )
proof end;

theorem :: YELLOW_9:36
for S being TopSpace
for T being non empty TopSpace
for K being prebasis of T
for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " A is open )
proof end;

theorem Th37: :: YELLOW_9:37
for T being non empty TopSpace
for x being Point of T
for X being Subset of T
for K being Basis of T st ( for A being Subset of T st A in K & x in A holds
A meets X ) holds
x in Cl X
proof end;

theorem Th38: :: YELLOW_9:38
for T being non empty TopSpace
for x being Point of T
for X being Subset of T
for K being prebasis of T st ( for Z being finite Subset-Family of T st Z c= K & x in Intersect Z holds
Intersect Z meets X ) holds
x in Cl X
proof end;

theorem :: YELLOW_9:39
for T being non empty TopSpace
for K being prebasis of T
for x being Point of T
for N being net of T st ( for A being Subset of T st A in K & x in A holds
N is_eventually_in A ) holds
for S being Subset of T st rng (netmap (N,T)) c= S holds
x in Cl S
proof end;

theorem Th40: :: YELLOW_9:40
for T1, T2 being non empty TopSpace
for B1 being Basis of T1
for B2 being Basis of T2 holds { [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } is Basis of [:T1,T2:]
proof end;

theorem Th41: :: YELLOW_9:41
for T1, T2 being non empty TopSpace
for B1 being prebasis of T1
for B2 being prebasis of T2 holds { [: the carrier of T1,b:] where b is Subset of T2 : b in B2 } \/ { [:a, the carrier of T2:] where a is Subset of T1 : a in B1 } is prebasis of [:T1,T2:]
proof end;

theorem :: YELLOW_9:42
for X1, X2 being set
for A being Subset-Family of [:X1,X2:]
for A1 being non empty Subset-Family of X1
for A2 being non empty Subset-Family of X2 st A = { [:a,b:] where a is Subset of X1, b is Subset of X2 : ( a in A1 & b in A2 ) } holds
Intersect A = [:(Intersect A1),(Intersect A2):]
proof end;

theorem :: YELLOW_9:43
for T1, T2 being non empty TopSpace
for B1 being prebasis of T1
for B2 being prebasis of T2 st union B1 = the carrier of T1 & union B2 = the carrier of T2 holds
{ [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } is prebasis of [:T1,T2:]
proof end;

definition
let R be RelStr ;
mode TopAugmentation of R -> TopRelStr means :Def4: :: YELLOW_9:def 4
 RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of R, the InternalRel of R #);
existence
ex b1 being TopRelStr st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of R, the InternalRel of R #)
proof end;
end;

:: deftheorem Def4 defines TopAugmentation YELLOW_9:def 4 :
for R being RelStr
for b2 being TopRelStr holds
( b2 is TopAugmentation of R iff RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of R, the InternalRel of R #) );

notation
let R be RelStr ;
let T be TopAugmentation of R;
synonym correct T for TopSpace-like ;
end;

registration
let R be RelStr ;
cluster correct discrete strict for TopAugmentation of R;
existence
ex b1 being TopAugmentation of R st
( b1 is correct & b1 is discrete & b1 is strict )
proof end;
end;

theorem :: YELLOW_9:44
for T being TopRelStr holds T is TopAugmentation of T
proof end;

theorem :: YELLOW_9:45
for S being TopRelStr
for T being TopAugmentation of S holds S is TopAugmentation of T
proof end;

theorem :: YELLOW_9:46
for R being RelStr
for T1 being TopAugmentation of R
for T2 being TopAugmentation of T1 holds T2 is TopAugmentation of R
proof end;

registration
let R be non empty RelStr ;
cluster -> non empty for TopAugmentation of R;
coherence
for b1 being TopAugmentation of R holds not b1 is empty
proof end;
end;

registration
let R be reflexive RelStr ;
cluster -> reflexive for TopAugmentation of R;
coherence
for b1 being TopAugmentation of R holds b1 is reflexive
proof end;
end;

registration
let R be transitive RelStr ;
cluster -> transitive for TopAugmentation of R;
coherence
for b1 being TopAugmentation of R holds b1 is transitive
proof end;
end;

registration
let R be antisymmetric RelStr ;
cluster -> antisymmetric for TopAugmentation of R;
coherence
for b1 being TopAugmentation of R holds b1 is antisymmetric
proof end;
end;

registration
let R be non empty complete RelStr ;
cluster -> complete for TopAugmentation of R;
coherence
for b1 being TopAugmentation of R holds b1 is complete
proof end;
end;

theorem Th47: :: YELLOW_9:47
for S being non empty reflexive antisymmetric up-complete RelStr
for T being non empty reflexive RelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds
for A being Subset of S
for C being Subset of T st A = C & A is inaccessible holds
C is inaccessible
proof end;

theorem Th48: :: YELLOW_9:48
for S being non empty reflexive RelStr
for T being TopAugmentation of S st the topology of T = sigma S holds
T is correct
proof end;

theorem Th49: :: YELLOW_9:49
for S being complete LATTICE
for T being TopAugmentation of S st the topology of T = sigma S holds
T is Scott
proof end;

registration
let R be complete LATTICE;
cluster non empty correct reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V197() up-complete /\-complete strict Scott for TopAugmentation of R;
existence
ex b1 being TopAugmentation of R st
( b1 is Scott & b1 is strict & b1 is correct )
proof end;
end;

theorem Th50: :: YELLOW_9:50
for S, T being non empty reflexive transitive antisymmetric complete Scott TopRelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds
for F being Subset of S
for G being Subset of T st F = G & F is open holds
G is open
proof end;

theorem Th51: :: YELLOW_9:51
for S being complete LATTICE
for T being Scott TopAugmentation of S holds the topology of T = sigma S
proof end;

theorem :: YELLOW_9:52
for S, T being complete LATTICE st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds
sigma S = sigma T
proof end;

registration
let R be complete LATTICE;
cluster Scott -> correct for TopAugmentation of R;
coherence
for b1 being TopAugmentation of R st b1 is Scott holds
b1 is correct
proof end;
end;

Lm1: for S being TopStruct ex T being strict TopSpace st
( the carrier of T = the carrier of S & the topology of S is prebasis of T )
proof end;

definition
let T be TopStruct ;
mode TopExtension of T -> TopSpace means :Def5: :: YELLOW_9:def 5
( the carrier of T = the carrier of it & the topology of T c= the topology of it );
existence
ex b1 being TopSpace st
( the carrier of T = the carrier of b1 & the topology of T c= the topology of b1 )
proof end;
end;

:: deftheorem Def5 defines TopExtension YELLOW_9:def 5 :
for T being TopStruct
for b2 being TopSpace holds
( b2 is TopExtension of T iff ( the carrier of T = the carrier of b2 & the topology of T c= the topology of b2 ) );

theorem Th53: :: YELLOW_9:53
for S being TopStruct ex T being TopExtension of S st
( T is strict & the topology of S is prebasis of T )
proof end;

registration
let T be TopStruct ;
cluster strict correct discrete for TopExtension of T;
existence
ex b1 being TopExtension of T st
( b1 is strict & b1 is discrete )
proof end;
end;

definition
let T1, T2 be TopStruct ;
mode Refinement of T1,T2 -> TopSpace means :Def6: :: YELLOW_9:def 6
( the carrier of it = the carrier of T1 \/ the carrier of T2 & the topology of T1 \/ the topology of T2 is prebasis of it );
existence
ex b1 being TopSpace st
( the carrier of b1 = the carrier of T1 \/ the carrier of T2 & the topology of T1 \/ the topology of T2 is prebasis of b1 )
proof end;
end;

:: deftheorem Def6 defines Refinement YELLOW_9:def 6 :
for T1, T2 being TopStruct
for b3 being TopSpace holds
( b3 is Refinement of T1,T2 iff ( the carrier of b3 = the carrier of T1 \/ the carrier of T2 & the topology of T1 \/ the topology of T2 is prebasis of b3 ) );

registration
let T1 be non empty TopStruct ;
let T2 be TopStruct ;
cluster -> non empty for Refinement of T1,T2;
coherence
for b1 being Refinement of T1,T2 holds not b1 is empty
proof end;
cluster -> non empty for Refinement of T2,T1;
coherence
for b1 being Refinement of T2,T1 holds not b1 is empty
proof end;
end;

theorem :: YELLOW_9:54
for T1, T2 being TopStruct
for T, T9 being Refinement of T1,T2 holds TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of T9, the topology of T9 #)
proof end;

theorem :: YELLOW_9:55
for T1, T2 being TopStruct
for T being Refinement of T1,T2 holds T is Refinement of T2,T1
proof end;

theorem :: YELLOW_9:56
for T1, T2 being TopStruct
for T being Refinement of T1,T2
for X being Subset-Family of T st X = the topology of T1 \/ the topology of T2 holds
the topology of T = UniCl (FinMeetCl X)
proof end;

theorem :: YELLOW_9:57
for T1, T2 being TopStruct st the carrier of T1 = the carrier of T2 holds
for T being Refinement of T1,T2 holds
( T is TopExtension of T1 & T is TopExtension of T2 )
proof end;

theorem :: YELLOW_9:58
for T1, T2 being non empty TopSpace
for T being Refinement of T1,T2
for B1 being prebasis of T1
for B2 being prebasis of T2 holds (B1 \/ B2) \/ { the carrier of T1, the carrier of T2} is prebasis of T
proof end;

theorem Th59: :: YELLOW_9:59
for T1, T2 being non empty TopSpace
for B1 being Basis of T1
for B2 being Basis of T2
for T being Refinement of T1,T2 holds (B1 \/ B2) \/ (INTERSECTION (B1,B2)) is Basis of T
proof end;

theorem Th60: :: YELLOW_9:60
for T1, T2 being non empty TopSpace st the carrier of T1 = the carrier of T2 holds
for T being Refinement of T1,T2 holds INTERSECTION ( the topology of T1, the topology of T2) is Basis of T
proof end;

theorem :: YELLOW_9:61
for L being non empty RelStr
for T1, T2 being correct TopAugmentation of L
for T being Refinement of T1,T2 holds INTERSECTION ( the topology of T1, the topology of T2) is Basis of T
proof end;