:: 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{ F₁() -> non empty set , F₂() -> Subset of F₁(), F₃() -> Subset of F₁(), F₄( set ) -> Element of F₁() } :

F₂() = { F₄(a) where a is Element of F₁() : a in F₃() }

provided

A1: F₃() = { F₄(a) where a is Element of F₁() : a in F₂() } and
A2: for a being Element of F₁() holds F₄(F₄(a)) = a

proof end;

scheme :: YELLOW_9:sch 2
FraenkelComplement1{ F₁() -> non empty RelStr , F₂() -> Subset-Family of F₁(), F₃() -> set , F₄( set ) -> Subset of F₁() } :

COMPLEMENT F₂() = { (F₄(a) `) where a is Element of F₁() : a in F₃() }

provided

A1: F₂() = { F₄(a) where a is Element of F₁() : a in F₃() }

proof end;

scheme :: YELLOW_9:sch 3
FraenkelComplement2{ F₁() -> non empty RelStr , F₂() -> Subset-Family of F₁(), F₃() -> set , F₄( set ) -> Subset of F₁() } :

COMPLEMENT F₂() = { F₄(a) where a is Element of F₁() : a in F₃() }

provided

A1: F₂() = { (F₄(a) `) where a is Element of F₁() : a in F₃() }

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{ F₁() -> TopSpace, F₂( set ) -> set , F₃() -> Function, P₁[ set ] } :

F₃() " (union { F₂(x) where x is Subset of F₁() : P₁[x] } ) = union { (F₃() " F₂(y)) where y is Subset of F₁() : P₁[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 b₁ being TopLattice st
( b₁ is strict & b₁ is complete & b₁ 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 b₁ being Function of S,T st b₁ 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 b₁ being Function of S,T st b₁ 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 b₁ being TopRelStr st RelStr(# the carrier of b₁, the InternalRel of b₁ #) = 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 b₂ being TopRelStr holds
( b₂ is TopAugmentation of R iff RelStr(# the carrier of b₂, the InternalRel of b₂ #) = 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 b₁ being TopAugmentation of R st
( b₁ is correct & b₁ is discrete & b₁ 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 b₁ being TopAugmentation of R holds not b₁ is empty

proof end;

end;

registration

let R be reflexive RelStr ;

cluster -> reflexive for TopAugmentation of R;

coherence
for b₁ being TopAugmentation of R holds b₁ is reflexive

proof end;

end;

registration

let R be transitive RelStr ;

cluster -> transitive for TopAugmentation of R;

coherence
for b₁ being TopAugmentation of R holds b₁ is transitive

proof end;

end;

registration

let R be antisymmetric RelStr ;

cluster -> antisymmetric for TopAugmentation of R;

coherence
for b₁ being TopAugmentation of R holds b₁ is antisymmetric

proof end;

end;

registration

let R be non empty complete RelStr ;

cluster -> complete for TopAugmentation of R;

coherence
for b₁ being TopAugmentation of R holds b₁ 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 b₁ being TopAugmentation of R st
( b₁ is Scott & b₁ is strict & b₁ 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 b₁ being TopAugmentation of R st b₁ is Scott holds
b₁ 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 b₁ being TopSpace st
( the carrier of T = the carrier of b₁ & the topology of T c= the topology of b₁ )

proof end;

end;

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

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 b₁ being TopExtension of T st
( b₁ is strict & b₁ 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 b₁ being TopSpace st
( the carrier of b₁ = the carrier of T1 \/ the carrier of T2 & the topology of T1 \/ the topology of T2 is prebasis of b₁ )

proof end;

end;

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

registration

let T1 be non empty TopStruct ;
let T2 be TopStruct ;

cluster -> non empty for Refinement of T1,T2;

coherence
for b₁ being Refinement of T1,T2 holds not b₁ is empty

proof end;

cluster -> non empty for Refinement of T2,T1;

coherence
for b₁ being Refinement of T2,T1 holds not b₁ 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;