FINTOPO7: Topology from Neighbourhoods

:: Topology from Neighbourhoods
:: by Roland Coghetto
::
:: Received August 14, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users

theorem :: FINTOPO7:1

for X being non empty set
for B, Y being Subset-Family of X st Y c= UniCl B holds
union Y in UniCl B

proof end;

theorem Th1: :: FINTOPO7:2

for X being non empty set
for B being empty Subset-Family of X st ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & X = union B holds
FinMeetCl B c= UniCl B

proof end;

theorem Th2: :: FINTOPO7:3

for X being non empty set
for B being non empty Subset-Family of X st ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & X = union B holds
FinMeetCl B c= UniCl B

proof end;

theorem Th3: :: FINTOPO7:4

for X being non empty set
for B being Subset-Family of X st ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & X = union B holds
( UniCl B = UniCl (FinMeetCl B) & TopStruct(# X,(UniCl B) #) is TopSpace-like )

proof end;

theorem :: FINTOPO7:5

for FMT being non empty FMT_Space_Str ex S being RelStr st
for x being Element of FMT holds U_FMT x is Subset of S

proof end;

registration

let T be non empty TopSpace;

cluster NeighSp T -> Fo_filled ;

proof end;

end;

definition

let ET be non empty strict FMT_Space_Str ;
let O be Subset of ET;

attr O is open means :Def1: :: FINTOPO7:def 1
for x being Element of ET st x in O holds
O in U_FMT x;

end;

:: deftheorem Def1 defines open FINTOPO7:def 1 :

definition

let ET be non empty strict FMT_Space_Str ;

attr ET is U_FMT_filter means :Def2: :: FINTOPO7:def 2
for x being Element of ET holds U_FMT x is Filter of the carrier of ET;

attr ET is U_FMT_with_point means :Def3: :: FINTOPO7:def 3
for x being Element of ET
for V being Element of U_FMT x holds x in V;

attr ET is U_FMT_local means :Def4: :: FINTOPO7:def 4
for x being Element of ET
for V being Element of U_FMT x ex W being Element of U_FMT x st
for y being Element of ET st y is Element of W holds
V is Element of U_FMT y;

end;

:: deftheorem Def2 defines U_FMT_filter FINTOPO7:def 2 :

:: deftheorem Def3 defines U_FMT_with_point FINTOPO7:def 3 :

:: deftheorem Def4 defines U_FMT_local FINTOPO7:def 4 :

theorem Th4: :: FINTOPO7:6

for ET being non empty strict FMT_Space_Str st ET is U_FMT_filter holds
for x being Element of ET holds not U_FMT x is empty ;

theorem :: FINTOPO7:7

for ET being non empty strict FMT_Space_Str st ET is U_FMT_with_point holds
ET is Fo_filled ;

theorem Th5: :: FINTOPO7:8

for ET being non empty strict FMT_Space_Str st ET is Fo_filled & ( for x being Element of ET holds not U_FMT x is empty ) holds
ET is U_FMT_with_point

proof end;

theorem :: FINTOPO7:9

for ET being non empty strict FMT_Space_Str st ET is Fo_filled & ET is U_FMT_filter holds
ET is U_FMT_with_point

proof end;

registration

cluster non empty strict U_FMT_filter U_FMT_with_point U_FMT_local for FMT_Space_Str ;

proof end;

end;

theorem Th6: :: FINTOPO7:10

for ET being non empty strict U_FMT_filter FMT_Space_Str
for x being Element of ET holds the carrier of ET in U_FMT x

proof end;

definition

let ET be non empty strict U_FMT_filter FMT_Space_Str ;
let x be Element of ET;

mode a_neighborhood of x -> Subset of ET means :Def5: :: FINTOPO7:def 5
it in U_FMT x;

proof end;

end;

:: deftheorem Def5 defines a_neighborhood FINTOPO7:def 5 :

registration

let ET be non empty strict U_FMT_filter FMT_Space_Str ;
let x be Element of ET;

cluster open for a_neighborhood of x;

proof end;

end;

definition

let ET be non empty strict U_FMT_filter FMT_Space_Str ;
let A be Subset of ET;

mode a_neighborhood of A -> Subset of ET means :Def6: :: FINTOPO7:def 6
for x being Element of ET st x in A holds
it in U_FMT x;

proof end;

end;

:: deftheorem Def6 defines a_neighborhood FINTOPO7:def 6 :

registration

let ET be non empty strict U_FMT_filter FMT_Space_Str ;
let A be Subset of ET;

cluster open for a_neighborhood of A;

proof end;

end;

theorem Th7: :: FINTOPO7:11

for ET being non empty strict U_FMT_filter FMT_Space_Str
for A being Subset of ET
for NA being a_neighborhood of A
for B being Subset of ET st NA c= B holds
B is a_neighborhood of A

proof end;

definition

let ET be non empty strict U_FMT_filter FMT_Space_Str ;
let A be Subset of ET;

func Neighborhood A -> Subset-Family of ET equals :: FINTOPO7:def 7
{ N where N is a_neighborhood of A : verum } ;

proof end;

end;

:: deftheorem defines Neighborhood FINTOPO7:def 7 :

theorem Th7bis: :: FINTOPO7:12

for ET being non empty strict U_FMT_filter FMT_Space_Str
for A being non empty Subset of ET holds Neighborhood A is Filter of the carrier of ET

proof end;

definition

let ET be non empty strict FMT_Space_Str ;

attr ET is U_FMT_filter_base means :: FINTOPO7:def 8
for x being Element of the carrier of ET holds U_FMT x is filter_base of the carrier of ET;

end;

:: deftheorem defines U_FMT_filter_base FINTOPO7:def 8 :

definition

let ET be non empty FMT_Space_Str ;

func <.ET.] -> Function of the carrier of ET,(bool (bool the carrier of ET)) means :Def7: :: FINTOPO7:def 9
for x being Element of the carrier of ET holds it . x = <.(U_FMT x).];

proof end;

proof end;

end;

:: deftheorem Def7 defines <. FINTOPO7:def 9 :

definition

let ET be non empty strict FMT_Space_Str ;

func gen_filter ET -> non empty strict FMT_Space_Str equals :: FINTOPO7:def 10
FMT_Space_Str(# the carrier of ET,<.ET.] #);

end;

:: deftheorem defines gen_filter FINTOPO7:def 10 :

theorem Th8: :: FINTOPO7:13

for ET being non empty strict FMT_Space_Str st ET is U_FMT_filter_base holds
gen_filter ET is U_FMT_filter

proof end;

definition

mode FMT_TopSpace is non empty strict U_FMT_filter U_FMT_with_point U_FMT_local FMT_Space_Str ;

end;

notation

let ET be FMT_TopSpace;
let x be Element of ET;
synonym NeighborhoodSystem x for U_FMT x;

end;

registration

let ET be FMT_TopSpace;

cluster open for Element of K24( the carrier of ET);

proof end;

end;

definition

let ET be FMT_TopSpace;

func Family_open_set ET -> non empty Subset-Family of the carrier of ET equals :: FINTOPO7:def 11
{ O where O is open Subset of ET : verum } ;

proof end;

end;

:: deftheorem defines Family_open_set FINTOPO7:def 11 :

theorem Th9: :: FINTOPO7:14

for ET being FMT_TopSpace holds
( {} in Family_open_set ET & the carrier of ET in Family_open_set ET & ( for a being Subset-Family of ET st a c= Family_open_set ET holds
union a in Family_open_set ET ) & ( for a, b being Subset of ET st a in Family_open_set ET & b in Family_open_set ET holds
a /\ b in Family_open_set ET ) )

proof end;

theorem Th10: :: FINTOPO7:15

for ET being FMT_TopSpace
for a being Element of ET
for V being a_neighborhood of a ex O being open Subset of ET st
( a in O & O c= V )

proof end;

theorem Th11: :: FINTOPO7:16

for ET being FMT_TopSpace
for A being non empty Subset of ET
for V being Subset of ET holds
( V is a_neighborhood of A iff ex O being open Subset of ET st
( A c= O & O c= V ) )

proof end;

theorem :: FINTOPO7:17

for ET being FMT_TopSpace
for A being non empty Subset of ET holds Neighborhood A is Filter of the carrier of ET by Th7bis;

definition

let ET be FMT_TopSpace;
let A be non empty Subset of ET;

func OpenNeighborhoods A -> Subset-Family of the carrier of ET equals :: FINTOPO7:def 12
{ N where N is open a_neighborhood of A : verum } ;

proof end;

end;

:: deftheorem defines OpenNeighborhoods FINTOPO7:def 12 :

theorem :: FINTOPO7:18

for ET being FMT_TopSpace
for cF being Filter of the carrier of ET
for cS being non empty Subset of cF
for A being non empty Subset of ET st cF = Neighborhood A & cS = OpenNeighborhoods A holds
cS is filter_basis

proof end;

theorem Th12: :: FINTOPO7:19

for T being non empty TopSpace ex ET being FMT_TopSpace st
( the carrier of T = the carrier of ET & Family_open_set ET = the topology of T )

proof end;

theorem Th13: :: FINTOPO7:20

for T being non empty TopSpace
for ET being FMT_TopSpace st the carrier of T = the carrier of ET & Family_open_set ET = the topology of T holds
for x being Element of ET holds U_FMT x = { V where V is Subset of ET : ex O being Subset of T st
( O in the topology of T & x in O & O c= V ) }

proof end;

definition

let ET be FMT_TopSpace;
let F be Subset-Family of ET;

attr F is quasi_basis means :Def8: :: FINTOPO7:def 13
Family_open_set ET c= UniCl F;

end;

:: deftheorem Def8 defines quasi_basis FINTOPO7:def 13 :

registration

let ET be FMT_TopSpace;

cluster Family_open_set ET -> non empty quasi_basis ;

proof end;

end;

registration

let ET be FMT_TopSpace;

cluster quasi_basis for Element of K24(K24( the carrier of ET));

proof end;

end;

definition

let ET be FMT_TopSpace;
let S be Subset-Family of ET;

attr S is open means :: FINTOPO7:def 14
S c= Family_open_set ET;

end;

:: deftheorem defines open FINTOPO7:def 14 :

registration

let ET be FMT_TopSpace;

cluster open for Element of K24(K24( the carrier of ET));

proof end;

end;

registration

let ET be FMT_TopSpace;

cluster quasi_basis open for Element of K24(K24( the carrier of ET));

proof end;

end;

definition

let ET be FMT_TopSpace;
mode Basis of ET is quasi_basis open Subset-Family of ET;

end;

theorem :: FINTOPO7:21

for ET being FMT_TopSpace
for B being Basis of ET holds Family_open_set ET = UniCl B

proof end;

theorem :: FINTOPO7:22

for X being non empty set
for B being non empty Subset-Family of X st ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & X = union B holds
ex ET being FMT_TopSpace st
( the carrier of ET = X & B is Basis of ET )

proof end;

theorem :: FINTOPO7:23

for ET being FMT_TopSpace
for B being Basis of ET holds
( ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & the carrier of ET = union B )

proof end;

definition

let T be non empty TopSpace;

func TopSpace2FMT T -> FMT_TopSpace means :Def9: :: FINTOPO7:def 15
( the carrier of it = the carrier of T & Family_open_set it = the topology of T );

existence by Th12;
uniqueness

proof end;

end;

:: deftheorem Def9 defines TopSpace2FMT FINTOPO7:def 15 :

definition

let ET be FMT_TopSpace;

func FMT2TopSpace ET -> strict TopSpace means :Def10: :: FINTOPO7:def 16
( the carrier of it = the carrier of ET & Family_open_set ET = the topology of it );

proof end;

end;

:: deftheorem Def10 defines FMT2TopSpace FINTOPO7:def 16 :

registration

let ET be FMT_TopSpace;

cluster FMT2TopSpace ET -> non empty strict ;

coherence by Def10;

end;

theorem :: FINTOPO7:24

for T being non empty strict TopSpace holds T = FMT2TopSpace (TopSpace2FMT T)

proof end;

theorem :: FINTOPO7:25

for ET being FMT_TopSpace holds ET = TopSpace2FMT (FMT2TopSpace ET)

proof end;