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

definition

let ETV be non empty strict FMT_Space_Str ;

attr ETV is PP0 means :def01: :: FINTOPO7:def 1
for x being Element of ETV holds U_FMT x is Filter of the carrier of ETV;

attr ETV is PP1 means :def02: :: FINTOPO7:def 2
for x being Element of ETV
for V being Element of U_FMT x holds x in V;

attr ETV is PP2 means :def03: :: FINTOPO7:def 3
for x being Element of ETV
for V being Element of U_FMT x ex W being Element of U_FMT x st
for y being Element of ETV st y is Element of W holds
V is Element of U_FMT y;

end;

:: deftheorem def01 defines PP0 FINTOPO7:def 1 :
for ETV being non empty strict FMT_Space_Str holds
( ETV is PP0 iff for x being Element of ETV holds U_FMT x is Filter of the carrier of ETV );

:: deftheorem def02 defines PP1 FINTOPO7:def 2 :
for ETV being non empty strict FMT_Space_Str holds
( ETV is PP1 iff for x being Element of ETV
for V being Element of U_FMT x holds x in V );

:: deftheorem def03 defines PP2 FINTOPO7:def 3 :
for ETV being non empty strict FMT_Space_Str holds
( ETV is PP2 iff for x being Element of ETV
for V being Element of U_FMT x ex W being Element of U_FMT x st
for y being Element of ETV st y is Element of W holds
V is Element of U_FMT y );

registration

cluster non empty strict PP0 PP1 PP2 for FMT_Space_Str ;

existence
ex b₁ being non empty strict FMT_Space_Str st
( b₁ is PP2 & b₁ is PP1 & b₁ is PP0 )

proof end;

end;

definition

mode FMT_TopSpace is non empty strict PP0 PP1 PP2 FMT_Space_Str ;

end;

definition

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

attr O is open means :def04: :: FINTOPO7:def 4
for x being Element of ETV st x in O holds
O in U_FMT x;

end;

:: deftheorem def04 defines open FINTOPO7:def 4 :
for ETV being non empty strict FMT_Space_Str
for O being Subset of ETV holds
( O is open iff for x being Element of ETV st x in O holds
O in U_FMT x );

registration

let ETV be FMT_TopSpace;

cluster open for Element of K10( the carrier of ETV);

existence
ex b₁ being Subset of ETV st b₁ is open

proof end;

end;

definition

let ETV be FMT_TopSpace;

func OOpen ETV -> non empty Subset-Family of the carrier of ETV equals :: FINTOPO7:def 5
{ O where O is open Subset of ETV : verum } ;

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

proof end;

end;

:: deftheorem defines OOpen FINTOPO7:def 5 :
for ETV being FMT_TopSpace holds OOpen ETV = { O where O is open Subset of ETV : verum } ;

theorem Th01: :: FINTOPO7:1

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

proof end;

theorem Th02: :: FINTOPO7:2

for ETV being non empty strict PP0 FMT_Space_Str
for x being Element of ETV holds the carrier of ETV in U_FMT x

proof end;

definition

let ETV be non empty strict PP0 FMT_Space_Str ;
let x be Element of ETV;

mode a_neighborhood of x -> Subset of ETV means :def06: :: FINTOPO7:def 6
it in U_FMT x;

existence
ex b₁ being Subset of ETV st b₁ in U_FMT x

proof end;

end;

:: deftheorem def06 defines a_neighborhood FINTOPO7:def 6 :
for ETV being non empty strict PP0 FMT_Space_Str
for x being Element of ETV
for b₃ being Subset of ETV holds
( b₃ is a_neighborhood of x iff b₃ in U_FMT x );

registration

let ETV be non empty strict PP0 FMT_Space_Str ;
let x be Element of ETV;

cluster open for a_neighborhood of x;

existence
ex b₁ being a_neighborhood of x st b₁ is open

proof end;

end;

definition

let ETV be non empty strict PP0 FMT_Space_Str ;
let A be Subset of ETV;

mode a_neighborhood of A -> Subset of ETV means :def07: :: FINTOPO7:def 7
for x being Element of ETV st x in A holds
it in U_FMT x;

existence
ex b₁ being Subset of ETV st
for x being Element of ETV st x in A holds
b₁ in U_FMT x

proof end;

end;

:: deftheorem def07 defines a_neighborhood FINTOPO7:def 7 :
for ETV being non empty strict PP0 FMT_Space_Str
for A, b₃ being Subset of ETV holds
( b₃ is a_neighborhood of A iff for x being Element of ETV st x in A holds
b₃ in U_FMT x );

registration

let ETV be non empty strict PP0 FMT_Space_Str ;
let A be Subset of ETV;

cluster open for a_neighborhood of A;

existence
ex b₁ being a_neighborhood of A st b₁ is open

proof end;

end;

theorem Th03: :: FINTOPO7:3

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

proof end;

definition

let ETV be non empty strict PP0 FMT_Space_Str ;
let A be Subset of ETV;

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

correctness
coherence
{ N where N is a_neighborhood of A : verum } is Subset-Family of ETV;

proof end;

end;

:: deftheorem defines Neighborhood FINTOPO7:def 8 :
for ETV being non empty strict PP0 FMT_Space_Str
for A being Subset of ETV holds Neighborhood A = { N where N is a_neighborhood of A : verum } ;

theorem :: FINTOPO7:4

for ETV being non empty strict PP0 FMT_Space_Str
for A being non empty Subset of ETV holds { F where F is a_neighborhood of A : verum } is Filter of the carrier of ETV

proof end;

theorem Th04: :: FINTOPO7:5

for ETV being non empty strict FMT_Space_Str st ETV is PP0 holds
for x being Element of ETV holds not U_FMT x is empty ;

theorem Th05: :: FINTOPO7:6

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

proof end;

theorem Th06: :: FINTOPO7:7

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

proof end;

theorem :: FINTOPO7:8

for ETV being FMT_TopSpace
for A being non empty Subset of ETV holds Neighborhood A is Filter of the carrier of ETV

proof end;

definition

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

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

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

proof end;

end;

:: deftheorem defines OpenNeighborhoods FINTOPO7:def 9 :
for ETV being FMT_TopSpace
for A being non empty Subset of ETV holds OpenNeighborhoods A = { N where N is open a_neighborhood of A : verum } ;

theorem :: FINTOPO7:9

for ETV being FMT_TopSpace
for F being Filter of the carrier of ETV
for S being non empty Subset of F
for A being non empty Subset of ETV st F = Neighborhood A & S = OpenNeighborhoods A holds
S is filter_basis

proof end;

definition

let ETV be non empty strict FMT_Space_Str ;

attr ETV is PP3 means :: FINTOPO7:def 10
for x being Element of the carrier of ETV holds U_FMT x is filter_base of the carrier of ETV;

end;

:: deftheorem defines PP3 FINTOPO7:def 10 :
for ETV being non empty strict FMT_Space_Str holds
( ETV is PP3 iff for x being Element of the carrier of ETV holds U_FMT x is filter_base of the carrier of ETV );

definition

let ETV be non empty FMT_Space_Str ;

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

existence
ex b₁ being Function of the carrier of ETV,(bool (bool the carrier of ETV)) st
for x being Element of the carrier of ETV holds b₁ . x = <.(U_FMT x).]

proof end;

uniqueness
for b₁, b₂ being Function of the carrier of ETV,(bool (bool the carrier of ETV)) st ( for x being Element of the carrier of ETV holds b₁ . x = <.(U_FMT x).] ) & ( for x being Element of the carrier of ETV holds b₂ . x = <.(U_FMT x).] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem def08 defines <. FINTOPO7:def 11 :
for ETV being non empty FMT_Space_Str
for b₂ being Function of the carrier of ETV,(bool (bool the carrier of ETV)) holds
( b₂ = <.ETV.] iff for x being Element of the carrier of ETV holds b₂ . x = <.(U_FMT x).] );

definition

let ETV be non empty strict FMT_Space_Str ;

func gen_top ETV -> non empty strict FMT_Space_Str equals :: FINTOPO7:def 12
FMT_Space_Str(# the carrier of ETV,<.ETV.] #);

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

end;

:: deftheorem defines gen_top FINTOPO7:def 12 :
for ETV being non empty strict FMT_Space_Str holds gen_top ETV = FMT_Space_Str(# the carrier of ETV,<.ETV.] #);

theorem Th07: :: FINTOPO7:10

for ETV being non empty strict FMT_Space_Str st ETV is PP3 holds
gen_top ETV is PP0

proof end;

theorem Th08: :: FINTOPO7:11

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

proof end;

theorem Th09: :: FINTOPO7:12

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

proof end;

definition

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

attr F is quasi_basis means :def10: :: FINTOPO7:def 13
OOpen X c= UniCl F;

end;

:: deftheorem def10 defines quasi_basis FINTOPO7:def 13 :
for X being FMT_TopSpace
for F being Subset-Family of X holds
( F is quasi_basis iff OOpen X c= UniCl F );

registration

let X be FMT_TopSpace;

cluster OOpen X -> non empty quasi_basis ;

coherence
OOpen X is quasi_basis

proof end;

end;

registration

let X be FMT_TopSpace;

cluster quasi_basis for Element of K10(K10( the carrier of X));

existence
ex b₁ being Subset-Family of X st b₁ is quasi_basis

proof end;

end;

definition

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

attr S is open means :: FINTOPO7:def 14
S c= OOpen X;

end;

:: deftheorem defines open FINTOPO7:def 14 :
for X being FMT_TopSpace
for S being Subset-Family of X holds
( S is open iff S c= OOpen X );

registration

let X be FMT_TopSpace;

cluster open for Element of K10(K10( the carrier of X));

existence
ex b₁ being Subset-Family of X st b₁ is open

proof end;

end;

registration

let X be FMT_TopSpace;

cluster quasi_basis open for Element of K10(K10( the carrier of X));

existence
ex b₁ being Subset-Family of X st
( b₁ is open & b₁ is quasi_basis )

proof end;

end;

definition

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

end;

theorem :: FINTOPO7:13

for X being FMT_TopSpace
for B being Basis of X holds OOpen X = UniCl B

proof end;

theorem :: FINTOPO7:14

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 Th10: :: FINTOPO7:15

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 Th11: :: FINTOPO7:16

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 Th12: :: FINTOPO7:17

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

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 TV being FMT_TopSpace st
( the carrier of TV = X & B is Basis of TV )

proof end;

theorem :: FINTOPO7:19

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

proof end;

definition

let T be non empty TopSpace;

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

existence
ex b₁ being FMT_TopSpace st
( the carrier of b₁ = the carrier of T & OOpen b₁ = the topology of T ) by Th08;
uniqueness
for b₁, b₂ being FMT_TopSpace st the carrier of b₁ = the carrier of T & OOpen b₁ = the topology of T & the carrier of b₂ = the carrier of T & OOpen b₂ = the topology of T holds
b₁ = b₂

proof end;

end;

:: deftheorem def11 defines TopSpace2FMT FINTOPO7:def 15 :
for T being non empty TopSpace
for b₂ being FMT_TopSpace holds
( b₂ = TopSpace2FMT T iff ( the carrier of b₂ = the carrier of T & OOpen b₂ = the topology of T ) );

definition

let ETV be FMT_TopSpace;

func FMT2TopSpace ETV -> strict TopSpace means :def12: :: FINTOPO7:def 16
( the carrier of it = the carrier of ETV & OOpen ETV = the topology of it );

existence
ex b₁ being strict TopSpace st
( the carrier of b₁ = the carrier of ETV & OOpen ETV = the topology of b₁ )

proof end;

uniqueness
for b₁, b₂ being strict TopSpace st the carrier of b₁ = the carrier of ETV & OOpen ETV = the topology of b₁ & the carrier of b₂ = the carrier of ETV & OOpen ETV = the topology of b₂ holds
b₁ = b₂ ;

end;

:: deftheorem def12 defines FMT2TopSpace FINTOPO7:def 16 :
for ETV being FMT_TopSpace
for b₂ being strict TopSpace holds
( b₂ = FMT2TopSpace ETV iff ( the carrier of b₂ = the carrier of ETV & OOpen ETV = the topology of b₂ ) );

registration

let ETV be FMT_TopSpace;

cluster FMT2TopSpace ETV -> non empty strict ;

coherence
not FMT2TopSpace ETV is empty by def12;

end;

theorem :: FINTOPO7:20

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

proof end;

theorem :: FINTOPO7:21

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

proof end;

theorem :: FINTOPO7:22

for T being non empty TopStruct holds NeighSp T is non empty FMT_Space_Str ;

theorem Th13: :: FINTOPO7:23

for X being non empty set
for F being non empty Subset of (BooleLatt X) holds
( F is Filter of (BooleLatt X) iff ( ( for p, q being Element of F holds p /\ q in F ) & ( for p being Element of F
for q being Element of (BooleLatt X) st p c= q holds
q in F ) ) )

proof end;

theorem Th14: :: FINTOPO7:24

for X being non empty set
for F being non empty Subset of (BooleLatt X) holds
( F is Filter of (BooleLatt X) iff for Y1, Y2 being Subset of X holds
( ( Y1 in F & Y2 in F implies Y1 /\ Y2 in F ) & ( Y1 in F & Y1 c= Y2 implies Y2 in F ) ) )

proof end;

theorem Th15: :: FINTOPO7:25

for X being non empty set
for FF being non empty Subset-Family of X st FF is Filter of (BooleLatt X) holds
FF is Filter of (BoolePoset X)

proof end;

theorem Th16: :: FINTOPO7:26

for X being non empty set
for F being Filter of (BoolePoset X) holds F is Filter of (BooleLatt X)

proof end;

theorem Th17: :: FINTOPO7:27

for X being non empty set
for F being non empty Subset of (BooleLatt X) holds
( ( F is with_non-empty_elements & F is Filter of (BooleLatt X) ) iff F is Filter of X )

proof end;

theorem Th18: :: FINTOPO7:28

for X being non empty set
for F being proper Filter of (BoolePoset X) holds F is Filter of X

proof end;

theorem :: FINTOPO7:29

for T being non empty TopSpace
for x being Point of T holds NeighborhoodSystem x is Filter of the carrier of T by Th18;

definition

let T be non empty TopSpace;
let F be proper Filter of (BoolePoset ([#] T));

func BOOL2F F -> Filter of the carrier of T equals :: FINTOPO7:def 17
F;

coherence
F is Filter of the carrier of T by Th18;

end;

:: deftheorem defines BOOL2F FINTOPO7:def 17 :
for T being non empty TopSpace
for F being proper Filter of (BoolePoset ([#] T)) holds BOOL2F F = F;

definition

let T be non empty TopSpace;
let F1 be Filter of the carrier of T;
let F2 be proper Filter of (BoolePoset ([#] T));

pred F1 is_filter-finer_than F2 means :: FINTOPO7:def 18
BOOL2F F2 c= F1;

end;

:: deftheorem defines is_filter-finer_than FINTOPO7:def 18 :
for T being non empty TopSpace
for F1 being Filter of the carrier of T
for F2 being proper Filter of (BoolePoset ([#] T)) holds
( F1 is_filter-finer_than F2 iff BOOL2F F2 c= F1 );

definition

let T be non empty TopSpace;
let F be Filter of the carrier of T;

func lim_filtre F -> Subset of T equals :: FINTOPO7:def 19
{ x where x is Point of T : F is_filter-finer_than NeighborhoodSystem x } ;

correctness
coherence
{ x where x is Point of T : F is_filter-finer_than NeighborhoodSystem x } is Subset of T;

proof end;

end;

:: deftheorem defines lim_filtre FINTOPO7:def 19 :
for T being non empty TopSpace
for F being Filter of the carrier of T holds lim_filtre F = { x where x is Point of T : F is_filter-finer_than NeighborhoodSystem x } ;

definition

let T be non empty TopSpace;
let B be filter_base of the carrier of T;

func Lim B -> Subset of T equals :: FINTOPO7:def 20
lim_filtre <.B.);

correctness
coherence
lim_filtre <.B.) is Subset of T;
;

end;

:: deftheorem defines Lim FINTOPO7:def 20 :
for T being non empty TopSpace
for B being filter_base of the carrier of T holds Lim B = lim_filtre <.B.);

theorem Th19: :: FINTOPO7:30

for T being non empty TopSpace
for F being Filter of the carrier of T holds F is proper Filter of (BoolePoset the carrier of T)

proof end;

definition

let T be non empty TopSpace;
let F be Filter of the carrier of T;

func F2BOOL (F,T) -> proper Filter of (BoolePoset ([#] T)) equals :: FINTOPO7:def 21
F;

coherence
F is proper Filter of (BoolePoset ([#] T))

proof end;

end;

:: deftheorem defines F2BOOL FINTOPO7:def 21 :
for T being non empty TopSpace
for F being Filter of the carrier of T holds F2BOOL (F,T) = F;

theorem :: FINTOPO7:31

for T being non empty TopSpace
for x being Point of T
for F being Filter of the carrier of T holds
( x is_a_convergence_point_of F,T iff x is_a_convergence_point_of F2BOOL (F,T),T ) ;

theorem :: FINTOPO7:32

for T being non empty TopSpace
for x being Point of T
for F being Filter of the carrier of T holds
( x is_a_convergence_point_of F,T iff x in lim_filtre F )

proof end;

definition

let T be non empty TopSpace;
let F be Filter of (BoolePoset ([#] T));

func lim_filtreb F -> Subset of T equals :: FINTOPO7:def 22
{ x where x is Point of T : NeighborhoodSystem x c= F } ;

correctness
coherence
{ x where x is Point of T : NeighborhoodSystem x c= F } is Subset of T;

proof end;

end;

:: deftheorem defines lim_filtreb FINTOPO7:def 22 :
for T being non empty TopSpace
for F being Filter of (BoolePoset ([#] T)) holds lim_filtreb F = { x where x is Point of T : NeighborhoodSystem x c= F } ;

theorem :: FINTOPO7:33

for T being non empty TopSpace
for F being Filter of the carrier of T holds lim_filtre F = lim_filtreb (F2BOOL (F,T))

proof end;

theorem :: FINTOPO7:34

for T being non empty TopSpace
for F being Filter of the carrier of T holds Lim (a_net (F2BOOL (F,T))) = lim_filtre F

proof end;

theorem Th20: :: FINTOPO7:35

for T being non empty Hausdorff TopSpace
for F being Filter of the carrier of T
for p, q being Point of T st p in lim_filtre F & q in lim_filtre F holds
p = q

proof end;

registration

let T be non empty Hausdorff TopSpace;
let F be Filter of the carrier of T;

cluster lim_filtre F -> trivial ;

coherence
lim_filtre F is trivial

proof end;

end;

definition

let ETV be FMT_TopSpace;
let x be Element of ETV;
let A be Subset of ETV;

pred x is_a_cluster_point_of A,ETV means :: FINTOPO7:def 23
for V being Element of U_FMT x holds V meets A;

end;

:: deftheorem defines is_a_cluster_point_of FINTOPO7:def 23 :
for ETV being FMT_TopSpace
for x being Element of ETV
for A being Subset of ETV holds
( x is_a_cluster_point_of A,ETV iff for V being Element of U_FMT x holds V meets A );

definition

let ETV be FMT_TopSpace;
let x be Element of ETV;

func FU_FMT x -> Filter of the carrier of ETV equals :: FINTOPO7:def 24
U_FMT x;

coherence
U_FMT x is Filter of the carrier of ETV by def01;

end;

:: deftheorem defines FU_FMT FINTOPO7:def 24 :
for ETV being FMT_TopSpace
for x being Element of ETV holds FU_FMT x = U_FMT x;

definition

let ETV be FMT_TopSpace;
let F be Filter of the carrier of ETV;
let x be Element of ETV;

pred x is_a_convergence_point_of F means :: FINTOPO7:def 25
FU_FMT x is_filter-coarser_than F;

end;

:: deftheorem defines is_a_convergence_point_of FINTOPO7:def 25 :
for ETV being FMT_TopSpace
for F being Filter of the carrier of ETV
for x being Element of ETV holds
( x is_a_convergence_point_of F iff FU_FMT x is_filter-coarser_than F );

definition

let ETV be FMT_TopSpace;
let F be Filter of the carrier of ETV;

func lim_filtre F -> Subset of ETV equals :: FINTOPO7:def 26
{ x where x is Element of ETV : x is_a_convergence_point_of F } ;

correctness
coherence
{ x where x is Element of ETV : x is_a_convergence_point_of F } is Subset of ETV;

proof end;

end;

:: deftheorem defines lim_filtre FINTOPO7:def 26 :
for ETV being FMT_TopSpace
for F being Filter of the carrier of ETV holds lim_filtre F = { x where x is Element of ETV : x is_a_convergence_point_of F } ;

theorem :: FINTOPO7:36

for ETV being FMT_TopSpace
for x being Element of ETV holds
( not the carrier of ETV is empty & U_FMT x is Filter of the carrier of ETV ) by def01;

definition

let ETV be FMT_TopSpace;
let F be Filter of the carrier of ETV;
let B be basis of F;

func lim_filtre B -> Subset of ETV equals :: FINTOPO7:def 27
lim_filtre F;

correctness
coherence
lim_filtre F is Subset of ETV;
;

end;

:: deftheorem defines lim_filtre FINTOPO7:def 27 :
for ETV being FMT_TopSpace
for F being Filter of the carrier of ETV
for B being basis of F holds lim_filtre B = lim_filtre F;

notation

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

end;

definition

let ETV be FMT_TopSpace;
let B be filter_base of the carrier of ETV;

func lim_filtre B -> Subset of ETV equals :: FINTOPO7:def 28
lim_filtre <.B.);

correctness
coherence
lim_filtre <.B.) is Subset of ETV;
;

end;

:: deftheorem defines lim_filtre FINTOPO7:def 28 :
for ETV being FMT_TopSpace
for B being filter_base of the carrier of ETV holds lim_filtre B = lim_filtre <.B.);

theorem :: FINTOPO7:37

for ETV being non empty strict FMT_Space_Str st ETV is PP1 holds
ETV is Fo_filled ;

theorem Th21: :: FINTOPO7:38

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

proof end;

theorem :: FINTOPO7:39

for ETV being non empty strict FMT_Space_Str st ETV is Fo_filled & ETV is PP0 holds
ETV is PP1

proof end;

theorem :: FINTOPO7:40

for T being non empty TopStruct holds NeighSp T is non empty FMT_Space_Str ;

registration

let T be non empty TopSpace;

cluster NeighSp T -> Fo_filled ;

coherence
NeighSp T is Fo_filled

proof end;

end;

theorem :: FINTOPO7:41

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;

definition

let ETV be non empty TopSpace;

attr ETV is PP4 means :: FINTOPO7:def 29
ex R being non empty FMT_Space_Str st
for x being Element of R
for y being Element of (NeighSp ETV)
for z being Subset-Family of the carrier of ETV st x = y & z = U_FMT y holds
the BNbd of R . x = <.z.];

end;

:: deftheorem defines PP4 FINTOPO7:def 29 :
for ETV being non empty TopSpace holds
( ETV is PP4 iff ex R being non empty FMT_Space_Str st
for x being Element of R
for y being Element of (NeighSp ETV)
for z being Subset-Family of the carrier of ETV st x = y & z = U_FMT y holds
the BNbd of R . x = <.z.] );

theorem :: FINTOPO7:42

for X being non empty set
for S being Element of bool (bool X) holds <.S.] is Element of bool (bool X) ;

theorem :: FINTOPO7:43

for ETV being non empty FMT_Space_Str holds bool (bool (rng the BNbd of ETV)) c= bool (bool (bool (bool the carrier of ETV)))

proof end;