:: 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

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

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

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 )

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

for x being Element of FMT holds U_FMT x is Subset of S

proof end;

:: deftheorem Def1 defines open FINTOPO7:def 1 :

for ET being non empty strict FMT_Space_Str

for O being Subset of ET holds

( O is open iff for x being Element of ET st x in O holds

O in U_FMT x );

for ET being non empty strict FMT_Space_Str

for O being Subset of ET holds

( O is open iff for x being Element of ET st x in O holds

O in U_FMT x );

definition

let ET be non empty strict FMT_Space_Str ;

end;
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;

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;

for x being Element of ET

for V being Element of U_FMT x holds x in V;

:: deftheorem Def2 defines U_FMT_filter FINTOPO7:def 2 :

for ET being non empty strict FMT_Space_Str holds

( ET is U_FMT_filter iff for x being Element of ET holds U_FMT x is Filter of the carrier of ET );

for ET being non empty strict FMT_Space_Str holds

( ET is U_FMT_filter iff for x being Element of ET holds U_FMT x is Filter of the carrier of ET );

:: deftheorem Def3 defines U_FMT_with_point FINTOPO7:def 3 :

for ET being non empty strict FMT_Space_Str holds

( ET is U_FMT_with_point iff for x being Element of ET

for V being Element of U_FMT x holds x in V );

for ET being non empty strict FMT_Space_Str holds

( ET is U_FMT_with_point iff for x being Element of ET

for V being Element of U_FMT x holds x in V );

:: deftheorem Def4 defines U_FMT_local FINTOPO7:def 4 :

for ET being non empty strict FMT_Space_Str holds

( ET is U_FMT_local iff 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 );

for ET being non empty strict FMT_Space_Str holds

( ET is U_FMT_local iff 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 );

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 ;

for x being Element of ET holds not U_FMT x is empty ;

theorem :: FINTOPO7:7

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

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

ET is U_FMT_with_point

proof end;

registration

existence

ex b_{1} being non empty strict FMT_Space_Str st

( b_{1} is U_FMT_local & b_{1} is U_FMT_with_point & b_{1} is U_FMT_filter )

end;
ex b

( b

proof 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

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;

existence

ex b_{1} being Subset of ET st b_{1} in U_FMT x

end;
let x be Element of ET;

existence

ex b

proof end;

:: deftheorem Def5 defines a_neighborhood FINTOPO7:def 5 :

for ET being non empty strict U_FMT_filter FMT_Space_Str

for x being Element of ET

for b_{3} being Subset of ET holds

( b_{3} is a_neighborhood of x iff b_{3} in U_FMT x );

for ET being non empty strict U_FMT_filter FMT_Space_Str

for x being Element of ET

for b

( b

registration

let ET be non empty strict U_FMT_filter FMT_Space_Str ;

let x be Element of ET;

existence

ex b_{1} being a_neighborhood of x st b_{1} is open

end;
let x be Element of ET;

existence

ex b

proof end;

definition

let ET be non empty strict U_FMT_filter FMT_Space_Str ;

let A be Subset of ET;

ex b_{1} being Subset of ET st

for x being Element of ET st x in A holds

b_{1} in U_FMT x

end;
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;

existence for x being Element of ET st x in A holds

it in U_FMT x;

ex b

for x being Element of ET st x in A holds

b

proof end;

:: deftheorem Def6 defines a_neighborhood FINTOPO7:def 6 :

for ET being non empty strict U_FMT_filter FMT_Space_Str

for A, b_{3} being Subset of ET holds

( b_{3} is a_neighborhood of A iff for x being Element of ET st x in A holds

b_{3} in U_FMT x );

for ET being non empty strict U_FMT_filter FMT_Space_Str

for A, b

( b

b

registration

let ET be non empty strict U_FMT_filter FMT_Space_Str ;

let A be Subset of ET;

existence

ex b_{1} being a_neighborhood of A st b_{1} is open

end;
let A be Subset of ET;

existence

ex b

proof 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

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;

coherence

{ N where N is a_neighborhood of A : verum } is Subset-Family of ET;

end;
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 } ;

correctness { N where N is a_neighborhood of A : verum } ;

coherence

{ N where N is a_neighborhood of A : verum } is Subset-Family of ET;

proof end;

:: deftheorem defines Neighborhood FINTOPO7:def 7 :

for ET being non empty strict U_FMT_filter FMT_Space_Str

for A being Subset of ET holds Neighborhood A = { N where N is a_neighborhood of A : verum } ;

for ET being non empty strict U_FMT_filter FMT_Space_Str

for A being Subset of ET holds Neighborhood A = { N where N is a_neighborhood of A : verum } ;

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

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 ;

end;
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;

for x being Element of the carrier of ET holds U_FMT x is filter_base of the carrier of ET;

:: deftheorem defines U_FMT_filter_base FINTOPO7:def 8 :

for ET being non empty strict FMT_Space_Str holds

( ET is U_FMT_filter_base iff for x being Element of the carrier of ET holds U_FMT x is filter_base of the carrier of ET );

for ET being non empty strict FMT_Space_Str holds

( ET is U_FMT_filter_base iff for x being Element of the carrier of ET holds U_FMT x is filter_base of the carrier of ET );

definition

let ET be non empty FMT_Space_Str ;

ex b_{1} being Function of the carrier of ET,(bool (bool the carrier of ET)) st

for x being Element of the carrier of ET holds b_{1} . x = <.(U_FMT x).]

for b_{1}, b_{2} being Function of the carrier of ET,(bool (bool the carrier of ET)) st ( for x being Element of the carrier of ET holds b_{1} . x = <.(U_FMT x).] ) & ( for x being Element of the carrier of ET holds b_{2} . x = <.(U_FMT x).] ) holds

b_{1} = b_{2}

end;
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).];

existence for x being Element of the carrier of ET holds it . x = <.(U_FMT x).];

ex b

for x being Element of the carrier of ET holds b

proof end;

uniqueness for b

b

proof end;

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

for ET being non empty FMT_Space_Str

for b_{2} being Function of the carrier of ET,(bool (bool the carrier of ET)) holds

( b_{2} = <.ET.] iff for x being Element of the carrier of ET holds b_{2} . x = <.(U_FMT x).] );

for ET being non empty FMT_Space_Str

for b

( b

definition

let ET be non empty strict FMT_Space_Str ;

coherence

FMT_Space_Str(# the carrier of ET,<.ET.] #) is non empty strict FMT_Space_Str ;

;

end;
func gen_filter ET -> non empty strict FMT_Space_Str equals :: FINTOPO7:def 10

FMT_Space_Str(# the carrier of ET,<.ET.] #);

correctness FMT_Space_Str(# the carrier of ET,<.ET.] #);

coherence

FMT_Space_Str(# the carrier of ET,<.ET.] #) is non empty strict FMT_Space_Str ;

;

:: deftheorem defines gen_filter FINTOPO7:def 10 :

for ET being non empty strict FMT_Space_Str holds gen_filter ET = FMT_Space_Str(# the carrier of ET,<.ET.] #);

for ET being non empty strict FMT_Space_Str holds gen_filter ET = FMT_Space_Str(# the carrier of ET,<.ET.] #);

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

gen_filter ET is U_FMT_filter

proof end;

definition
end;

notation
end;

registration
end;

definition

let ET be FMT_TopSpace;

coherence

{ O where O is open Subset of ET : verum } is non empty Subset-Family of the carrier of ET;

end;
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 } ;

correctness { O where O is open Subset of ET : verum } ;

coherence

{ O where O is open Subset of ET : verum } is non empty Subset-Family of the carrier of ET;

proof end;

:: deftheorem defines Family_open_set FINTOPO7:def 11 :

for ET being FMT_TopSpace holds Family_open_set ET = { O where O is open Subset of ET : verum } ;

for ET being FMT_TopSpace holds Family_open_set ET = { O where O is open Subset of ET : verum } ;

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 ) )

( {} 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 )

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 ) )

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;

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;

coherence

{ N where N is open a_neighborhood of A : verum } is Subset-Family of the carrier of ET;

end;
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 } ;

correctness { N where N is open a_neighborhood of A : verum } ;

coherence

{ N where N is open a_neighborhood of A : verum } is Subset-Family of the carrier of ET;

proof end;

:: deftheorem defines OpenNeighborhoods FINTOPO7:def 12 :

for ET being FMT_TopSpace

for A being non empty Subset of ET holds OpenNeighborhoods A = { N where N is open a_neighborhood of A : verum } ;

for ET being FMT_TopSpace

for A being non empty Subset of ET holds OpenNeighborhoods A = { N where N is open a_neighborhood of A : verum } ;

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

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 )

( 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 ) }

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;

:: deftheorem Def8 defines quasi_basis FINTOPO7:def 13 :

for ET being FMT_TopSpace

for F being Subset-Family of ET holds

( F is quasi_basis iff Family_open_set ET c= UniCl F );

for ET being FMT_TopSpace

for F being Subset-Family of ET holds

( F is quasi_basis iff Family_open_set ET c= UniCl F );

registration

let ET be FMT_TopSpace;

existence

ex b_{1} being Subset-Family of ET st b_{1} is quasi_basis

end;
existence

ex b

proof end;

:: deftheorem defines open FINTOPO7:def 14 :

for ET being FMT_TopSpace

for S being Subset-Family of ET holds

( S is open iff S c= Family_open_set ET );

for ET being FMT_TopSpace

for S being Subset-Family of ET holds

( S is open iff S c= Family_open_set ET );

registration
end;

registration

let ET be FMT_TopSpace;

existence

ex b_{1} being Subset-Family of ET st

( b_{1} is open & b_{1} is quasi_basis )

end;
existence

ex b

( 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 )

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 )

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;

ex b_{1} being FMT_TopSpace st

( the carrier of b_{1} = the carrier of T & Family_open_set b_{1} = the topology of T )
by Th12;

uniqueness

for b_{1}, b_{2} being FMT_TopSpace st the carrier of b_{1} = the carrier of T & Family_open_set b_{1} = the topology of T & the carrier of b_{2} = the carrier of T & Family_open_set b_{2} = the topology of T holds

b_{1} = b_{2}

end;
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 ( the carrier of it = the carrier of T & Family_open_set it = the topology of T );

ex b

( the carrier of b

uniqueness

for b

b

proof end;

:: deftheorem Def9 defines TopSpace2FMT FINTOPO7:def 15 :

for T being non empty TopSpace

for b_{2} being FMT_TopSpace holds

( b_{2} = TopSpace2FMT T iff ( the carrier of b_{2} = the carrier of T & Family_open_set b_{2} = the topology of T ) );

for T being non empty TopSpace

for b

( b

definition

let ET be FMT_TopSpace;

ex b_{1} being strict TopSpace st

( the carrier of b_{1} = the carrier of ET & Family_open_set ET = the topology of b_{1} )

for b_{1}, b_{2} being strict TopSpace st the carrier of b_{1} = the carrier of ET & Family_open_set ET = the topology of b_{1} & the carrier of b_{2} = the carrier of ET & Family_open_set ET = the topology of b_{2} holds

b_{1} = b_{2}
;

end;
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 );

existence ( the carrier of it = the carrier of ET & Family_open_set ET = the topology of it );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def10 defines FMT2TopSpace FINTOPO7:def 16 :

for ET being FMT_TopSpace

for b_{2} being strict TopSpace holds

( b_{2} = FMT2TopSpace ET iff ( the carrier of b_{2} = the carrier of ET & Family_open_set ET = the topology of b_{2} ) );

for ET being FMT_TopSpace

for b

( b