YELLOW_9: Bases and Refinements of Topologies

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

begin

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 trivial correct reflexive transitive antisymmetric with_suprema with_infima complete strict TopRelStr ;
existence

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 Function-like V27( the carrier of S) quasi_total infs-preserving Element of bool [: the carrier of S, the carrier of T:];
existence

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 Function-like V27( the carrier of S) quasi_total sups-preserving Element of bool [: the carrier of S, the carrier of T:];
existence

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 by RELAT_1:71;
A3: rng (id the carrier of S) = the carrier of S by RELAT_1:71;
func incl (S,R) -> Function of S,R equals :Def1: :: YELLOW_9:def 1
id the carrier of S;
coherence by A1, A2, A3, FUNCT_2:4;

end;

:: deftheorem Def1 defines incl YELLOW_9:def 1 :

registration

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

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 of R equals :: YELLOW_9:def 2
(incl ((subrelstr X),R)) * ((subrelstr X) +id);
coherence ;
func X opp+id -> non empty strict NetStr of R equals :: YELLOW_9:def 3
(incl ((subrelstr X),R)) * ((subrelstr X) opp+id);
coherence ;

end;

:: deftheorem defines +id YELLOW_9:def 2 :

:: deftheorem defines opp+id YELLOW_9:def 3 :

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 ;
cluster X opp+id -> non empty reflexive strict ;
coherence ;

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 ;
cluster X opp+id -> non empty transitive strict ;
coherence ;

end;

registration

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

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 ;

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

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 ;

end;

begin

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 non empty trivial 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 non empty trivial 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;

begin

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;

begin

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;

begin

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

proof end;

end;

:: deftheorem Def4 defines TopAugmentation YELLOW_9:def 4 :

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 TopAugmentation of R;
existence

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 TopAugmentation of R;
coherence

proof end;

end;

registration

let R be reflexive RelStr ;
cluster -> reflexive TopAugmentation of R;
coherence

proof end;

end;

registration

let R be transitive RelStr ;
cluster -> transitive TopAugmentation of R;
coherence

proof end;

end;

registration

let R be antisymmetric RelStr ;
cluster -> antisymmetric TopAugmentation of R;
coherence

proof end;

end;

registration

let R be non empty complete RelStr ;
cluster -> complete TopAugmentation of R;
coherence

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_by_directed_joins holds
C is inaccessible_by_directed_joins

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 V186() up-complete /\-complete strict Scott TopAugmentation of R;
existence

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 TopAugmentation of R;
coherence

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;

begin

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

proof end;

end;

:: deftheorem Def5 defines TopExtension YELLOW_9:def 5 :

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 TopExtension of T;
existence

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

proof end;

end;

:: deftheorem Def6 defines Refinement YELLOW_9:def 6 :

registration

let T1 be non empty TopStruct ;
let T2 be TopStruct ;
cluster -> non empty Refinement of T1,T2;
coherence

proof end;

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

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;