:: by Grzegorz Bancerek , Noboru Endou and Yuji Sakai

::

:: Received July 29, 2001

:: Copyright (c) 2001-2012 Association of Mizar Users

begin

theorem Th1: :: YELLOW19:1

for X being non empty set

for F being proper Filter of (BoolePoset X)

for A being set st A in F holds

not A is empty

for F being proper Filter of (BoolePoset X)

for A being set st A in F holds

not A is empty

proof end;

definition

let T be non empty TopSpace;

let x be Point of T;

{ A where A is a_neighborhood of x : verum } is Subset of (BoolePoset ([#] T))

end;
let x be Point of T;

func NeighborhoodSystem x -> Subset of (BoolePoset ([#] T)) equals :: YELLOW19:def 1

{ A where A is a_neighborhood of x : verum } ;

coherence { A where A is a_neighborhood of x : verum } ;

{ A where A is a_neighborhood of x : verum } is Subset of (BoolePoset ([#] T))

proof end;

:: deftheorem defines NeighborhoodSystem YELLOW19:def 1 :

for T being non empty TopSpace

for x being Point of T holds NeighborhoodSystem x = { A where A is a_neighborhood of x : verum } ;

for T being non empty TopSpace

for x being Point of T holds NeighborhoodSystem x = { A where A is a_neighborhood of x : verum } ;

theorem Th2: :: YELLOW19:2

for T being non empty TopSpace

for x being Point of T

for A being set holds

( A in NeighborhoodSystem x iff A is a_neighborhood of x )

for x being Point of T

for A being set holds

( A in NeighborhoodSystem x iff A is a_neighborhood of x )

proof end;

registration

let T be non empty TopSpace;

let x be Point of T;

coherence

( not NeighborhoodSystem x is empty & NeighborhoodSystem x is proper & NeighborhoodSystem x is upper & NeighborhoodSystem x is filtered )

end;
let x be Point of T;

coherence

( not NeighborhoodSystem x is empty & NeighborhoodSystem x is proper & NeighborhoodSystem x is upper & NeighborhoodSystem x is filtered )

proof end;

theorem Th3: :: YELLOW19:3

for T being non empty TopSpace

for x being Point of T

for F being upper Subset of (BoolePoset ([#] T)) holds

( x is_a_convergence_point_of F,T iff NeighborhoodSystem x c= F )

for x being Point of T

for F being upper Subset of (BoolePoset ([#] T)) holds

( x is_a_convergence_point_of F,T iff NeighborhoodSystem x c= F )

proof end;

theorem :: YELLOW19:4

for T being non empty TopSpace

for x being Point of T holds x is_a_convergence_point_of NeighborhoodSystem x,T by Th3;

for x being Point of T holds x is_a_convergence_point_of NeighborhoodSystem x,T by Th3;

theorem :: YELLOW19:5

for T being non empty TopSpace

for A being Subset of T holds

( A is open iff for x being Point of T st x in A holds

for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds

A in F )

for A being Subset of T holds

( A is open iff for x being Point of T st x in A holds

for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds

A in F )

proof end;

definition

let S be non empty 1-sorted ;

let N be non empty NetStr over S;

ex b_{1} being Subset of S ex i being Element of N st b_{1} = rng the mapping of (N | i)

end;
let N be non empty NetStr over S;

mode Subset of S,N -> Subset of S means :Def2: :: YELLOW19:def 2

ex i being Element of N st it = rng the mapping of (N | i);

existence ex i being Element of N st it = rng the mapping of (N | i);

ex b

proof end;

:: deftheorem Def2 defines Subset YELLOW19:def 2 :

for S being non empty 1-sorted

for N being non empty NetStr over S

for b_{3} being Subset of S holds

( b_{3} is Subset of S,N iff ex i being Element of N st b_{3} = rng the mapping of (N | i) );

for S being non empty 1-sorted

for N being non empty NetStr over S

for b

( b

theorem :: YELLOW19:6

registration

let S be non empty 1-sorted ;

let N be non empty reflexive NetStr over S;

coherence

for b_{1} being Subset of S,N holds not b_{1} is empty

end;
let N be non empty reflexive NetStr over S;

coherence

for b

proof end;

theorem Th7: :: YELLOW19:7

for S being non empty 1-sorted

for N being net of S

for i being Element of N

for x being set holds

( x in rng the mapping of (N | i) iff ex j being Element of N st

( i <= j & x = N . j ) )

for N being net of S

for i being Element of N

for x being set holds

( x in rng the mapping of (N | i) iff ex j being Element of N st

( i <= j & x = N . j ) )

proof end;

theorem Th8: :: YELLOW19:8

for S being non empty 1-sorted

for N being net of S

for A being Subset of S,N holds N is_eventually_in A

for N being net of S

for A being Subset of S,N holds N is_eventually_in A

proof end;

theorem :: YELLOW19:9

for S being non empty 1-sorted

for N being net of S

for F being non empty finite set st ( for A being Element of F holds A is Subset of S,N ) holds

ex B being Subset of S,N st B c= meet F

for N being net of S

for F being non empty finite set st ( for A being Element of F holds A is Subset of S,N ) holds

ex B being Subset of S,N st B c= meet F

proof end;

definition

let T be non empty 1-sorted ;

let N be non empty NetStr over T;

{ A where A is Subset of T : N is_eventually_in A } is Subset of (BoolePoset ([#] T))

end;
let N be non empty NetStr over T;

func a_filter N -> Subset of (BoolePoset ([#] T)) equals :: YELLOW19:def 3

{ A where A is Subset of T : N is_eventually_in A } ;

coherence { A where A is Subset of T : N is_eventually_in A } ;

{ A where A is Subset of T : N is_eventually_in A } is Subset of (BoolePoset ([#] T))

proof end;

:: deftheorem defines a_filter YELLOW19:def 3 :

for T being non empty 1-sorted

for N being non empty NetStr over T holds a_filter N = { A where A is Subset of T : N is_eventually_in A } ;

for T being non empty 1-sorted

for N being non empty NetStr over T holds a_filter N = { A where A is Subset of T : N is_eventually_in A } ;

theorem Th10: :: YELLOW19:10

for T being non empty 1-sorted

for N being non empty NetStr over T

for A being set holds

( A in a_filter N iff ( N is_eventually_in A & A is Subset of T ) )

for N being non empty NetStr over T

for A being set holds

( A in a_filter N iff ( N is_eventually_in A & A is Subset of T ) )

proof end;

registration

let T be non empty 1-sorted ;

let N be non empty NetStr over T;

coherence

( not a_filter N is empty & a_filter N is upper )

end;
let N be non empty NetStr over T;

coherence

( not a_filter N is empty & a_filter N is upper )

proof end;

registration

let T be non empty 1-sorted ;

let N be net of T;

coherence

( a_filter N is proper & a_filter N is filtered )

end;
let N be net of T;

coherence

( a_filter N is proper & a_filter N is filtered )

proof end;

theorem Th11: :: YELLOW19:11

for T being non empty TopSpace

for N being net of T

for x being Point of T holds

( x is_a_cluster_point_of N iff x is_a_cluster_point_of a_filter N,T )

for N being net of T

for x being Point of T holds

( x is_a_cluster_point_of N iff x is_a_cluster_point_of a_filter N,T )

proof end;

theorem Th12: :: YELLOW19:12

for T being non empty TopSpace

for N being net of T

for x being Point of T holds

( x in Lim N iff x is_a_convergence_point_of a_filter N,T )

for N being net of T

for x being Point of T holds

( x in Lim N iff x is_a_convergence_point_of a_filter N,T )

proof end;

definition

let L be non empty 1-sorted ;

let O be non empty Subset of L;

let F be Filter of (BoolePoset O);

ex b_{1} being non empty strict NetStr over L st

( the carrier of b_{1} = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b_{1} holds

( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b_{1} holds b_{1} . i = i `1 ) )

for b_{1}, b_{2} being non empty strict NetStr over L st the carrier of b_{1} = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b_{1} holds

( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b_{1} holds b_{1} . i = i `1 ) & the carrier of b_{2} = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b_{2} holds

( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b_{2} holds b_{2} . i = i `1 ) holds

b_{1} = b_{2}

end;
let O be non empty Subset of L;

let F be Filter of (BoolePoset O);

func a_net F -> non empty strict NetStr over L means :Def4: :: YELLOW19:def 4

( the carrier of it = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of it holds

( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of it holds it . i = i `1 ) );

existence ( the carrier of it = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of it holds

( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of it holds it . i = i `1 ) );

ex b

( the carrier of b

( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b

proof end;

uniqueness for b

( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b

( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b

b

proof end;

:: deftheorem Def4 defines a_net YELLOW19:def 4 :

for L being non empty 1-sorted

for O being non empty Subset of L

for F being Filter of (BoolePoset O)

for b_{4} being non empty strict NetStr over L holds

( b_{4} = a_net F iff ( the carrier of b_{4} = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b_{4} holds

( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b_{4} holds b_{4} . i = i `1 ) ) );

for L being non empty 1-sorted

for O being non empty Subset of L

for F being Filter of (BoolePoset O)

for b

( b

( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b

registration

let L be non empty 1-sorted ;

let O be non empty Subset of L;

let F be Filter of (BoolePoset O);

coherence

( a_net F is reflexive & a_net F is transitive )

end;
let O be non empty Subset of L;

let F be Filter of (BoolePoset O);

coherence

( a_net F is reflexive & a_net F is transitive )

proof end;

registration

let L be non empty 1-sorted ;

let O be non empty Subset of L;

let F be proper Filter of (BoolePoset O);

coherence

a_net F is directed

end;
let O be non empty Subset of L;

let F be proper Filter of (BoolePoset O);

coherence

a_net F is directed

proof end;

theorem Th13: :: YELLOW19:13

for T being non empty 1-sorted

for F being Filter of (BoolePoset ([#] T)) holds F \ {{}} = a_filter (a_net F)

for F being Filter of (BoolePoset ([#] T)) holds F \ {{}} = a_filter (a_net F)

proof end;

theorem Th14: :: YELLOW19:14

for T being non empty 1-sorted

for F being proper Filter of (BoolePoset ([#] T)) holds F = a_filter (a_net F)

for F being proper Filter of (BoolePoset ([#] T)) holds F = a_filter (a_net F)

proof end;

theorem Th15: :: YELLOW19:15

for T being non empty 1-sorted

for F being Filter of (BoolePoset ([#] T))

for A being non empty Subset of T holds

( A in F iff a_net F is_eventually_in A )

for F being Filter of (BoolePoset ([#] T))

for A being non empty Subset of T holds

( A in F iff a_net F is_eventually_in A )

proof end;

theorem Th16: :: YELLOW19:16

for T being non empty TopSpace

for F being proper Filter of (BoolePoset ([#] T))

for x being Point of T holds

( x is_a_cluster_point_of a_net F iff x is_a_cluster_point_of F,T )

for F being proper Filter of (BoolePoset ([#] T))

for x being Point of T holds

( x is_a_cluster_point_of a_net F iff x is_a_cluster_point_of F,T )

proof end;

theorem Th17: :: YELLOW19:17

for T being non empty TopSpace

for F being proper Filter of (BoolePoset ([#] T))

for x being Point of T holds

( x in Lim (a_net F) iff x is_a_convergence_point_of F,T )

for F being proper Filter of (BoolePoset ([#] T))

for x being Point of T holds

( x in Lim (a_net F) iff x is_a_convergence_point_of F,T )

proof end;

theorem Th18: :: YELLOW19:18

for T being non empty TopSpace

for x being Point of T

for A being Subset of T st x in Cl A holds

for F being proper Filter of (BoolePoset ([#] T)) st F = NeighborhoodSystem x holds

a_net F is_often_in A

for x being Point of T

for A being Subset of T st x in Cl A holds

for F being proper Filter of (BoolePoset ([#] T)) st F = NeighborhoodSystem x holds

a_net F is_often_in A

proof end;

theorem Th19: :: YELLOW19:19

for T being non empty 1-sorted

for A being set

for N being net of T st N is_eventually_in A holds

for S being subnet of N holds S is_eventually_in A

for A being set

for N being net of T st N is_eventually_in A holds

for S being subnet of N holds S is_eventually_in A

proof end;

theorem Th20: :: YELLOW19:20

for T being non empty TopSpace

for F, G, x being set st F c= G & x is_a_convergence_point_of F,T holds

x is_a_convergence_point_of G,T

for F, G, x being set st F c= G & x is_a_convergence_point_of F,T holds

x is_a_convergence_point_of G,T

proof end;

theorem Th21: :: YELLOW19:21

for T being non empty TopSpace

for A being Subset of T

for x being Point of T holds

( x in Cl A iff ex N being net of T st

( N is_eventually_in A & x is_a_cluster_point_of N ) )

for A being Subset of T

for x being Point of T holds

( x in Cl A iff ex N being net of T st

( N is_eventually_in A & x is_a_cluster_point_of N ) )

proof end;

theorem Th22: :: YELLOW19:22

for T being non empty TopSpace

for A being Subset of T

for x being Point of T holds

( x in Cl A iff ex N being convergent net of T st

( N is_eventually_in A & x in Lim N ) )

for A being Subset of T

for x being Point of T holds

( x in Cl A iff ex N being convergent net of T st

( N is_eventually_in A & x in Lim N ) )

proof end;

theorem :: YELLOW19:23

for T being non empty TopSpace

for A being Subset of T holds

( A is closed iff for N being net of T st N is_eventually_in A holds

for x being Point of T st x is_a_cluster_point_of N holds

x in A )

for A being Subset of T holds

( A is closed iff for N being net of T st N is_eventually_in A holds

for x being Point of T st x is_a_cluster_point_of N holds

x in A )

proof end;

theorem :: YELLOW19:24

for T being non empty TopSpace

for A being Subset of T holds

( A is closed iff for N being convergent net of T st N is_eventually_in A holds

for x being Point of T st x in Lim N holds

x in A )

for A being Subset of T holds

( A is closed iff for N being convergent net of T st N is_eventually_in A holds

for x being Point of T st x in Lim N holds

x in A )

proof end;

theorem Th25: :: YELLOW19:25

for T being non empty TopSpace

for A being Subset of T

for x being Point of T holds

( x in Cl A iff ex F being proper Filter of (BoolePoset ([#] T)) st

( A in F & x is_a_cluster_point_of F,T ) )

for A being Subset of T

for x being Point of T holds

( x in Cl A iff ex F being proper Filter of (BoolePoset ([#] T)) st

( A in F & x is_a_cluster_point_of F,T ) )

proof end;

theorem Th26: :: YELLOW19:26

for T being non empty TopSpace

for A being Subset of T

for x being Point of T holds

( x in Cl A iff ex F being ultra Filter of (BoolePoset ([#] T)) st

( A in F & x is_a_convergence_point_of F,T ) )

for A being Subset of T

for x being Point of T holds

( x in Cl A iff ex F being ultra Filter of (BoolePoset ([#] T)) st

( A in F & x is_a_convergence_point_of F,T ) )

proof end;

theorem :: YELLOW19:27

for T being non empty TopSpace

for A being Subset of T holds

( A is closed iff for F being proper Filter of (BoolePoset ([#] T)) st A in F holds

for x being Point of T st x is_a_cluster_point_of F,T holds

x in A )

for A being Subset of T holds

( A is closed iff for F being proper Filter of (BoolePoset ([#] T)) st A in F holds

for x being Point of T st x is_a_cluster_point_of F,T holds

x in A )

proof end;

theorem :: YELLOW19:28

for T being non empty TopSpace

for A being Subset of T holds

( A is closed iff for F being ultra Filter of (BoolePoset ([#] T)) st A in F holds

for x being Point of T st x is_a_convergence_point_of F,T holds

x in A )

for A being Subset of T holds

( A is closed iff for F being ultra Filter of (BoolePoset ([#] T)) st A in F holds

for x being Point of T st x is_a_convergence_point_of F,T holds

x in A )

proof end;

theorem Th29: :: YELLOW19:29

for T being non empty TopSpace

for N being net of T

for s being Point of T holds

( s is_a_cluster_point_of N iff for A being Subset of T,N holds s in Cl A )

for N being net of T

for s being Point of T holds

( s is_a_cluster_point_of N iff for A being Subset of T,N holds s in Cl A )

proof end;

theorem :: YELLOW19:30

for T being non empty TopSpace

for F being Subset-Family of T st F is closed holds

FinMeetCl F is closed

for F being Subset-Family of T st F is closed holds

FinMeetCl F is closed

proof end;

Lm1: for T being non empty TopSpace st T is compact holds

for N being net of T ex x being Point of T st x is_a_cluster_point_of N

proof end;

Lm2: for T being non empty TopSpace st ( for N being net of T st N in NetUniv T holds

ex x being Point of T st x is_a_cluster_point_of N ) holds

T is compact

proof end;

theorem Th31: :: YELLOW19:31

for T being non empty TopSpace holds

( T is compact iff for F being ultra Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_convergence_point_of F,T )

( T is compact iff for F being ultra Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_convergence_point_of F,T )

proof end;

theorem :: YELLOW19:32

for T being non empty TopSpace holds

( T is compact iff for F being proper Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_cluster_point_of F,T )

( T is compact iff for F being proper Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_cluster_point_of F,T )

proof end;

theorem Th33: :: YELLOW19:33

for T being non empty TopSpace holds

( T is compact iff for N being net of T ex x being Point of T st x is_a_cluster_point_of N )

( T is compact iff for N being net of T ex x being Point of T st x is_a_cluster_point_of N )

proof end;

theorem :: YELLOW19:34

registration

let L be non empty 1-sorted ;

let N be transitive NetStr over L;

coherence

for b_{1} being full SubNetStr of N holds b_{1} is transitive

end;
let N be transitive NetStr over L;

coherence

for b

proof end;

registration

let L be non empty 1-sorted ;

let N be non empty directed NetStr over L;

existence

ex b_{1} being SubNetStr of N st

( b_{1} is strict & not b_{1} is empty & b_{1} is directed & b_{1} is full )

end;
let N be non empty directed NetStr over L;

existence

ex b

( b

proof end;

theorem :: YELLOW19:35

for T being non empty TopSpace holds

( T is compact iff for N being net of T ex S being subnet of N st S is convergent )

( T is compact iff for N being net of T ex S being subnet of N st S is convergent )

proof end;

definition

let S be non empty 1-sorted ;

let N be non empty NetStr over S;

end;
let N be non empty NetStr over S;

attr N is Cauchy means :: YELLOW19:def 5

for A being Subset of S holds

( N is_eventually_in A or N is_eventually_in A ` );

for A being Subset of S holds

( N is_eventually_in A or N is_eventually_in A ` );

:: deftheorem defines Cauchy YELLOW19:def 5 :

for S being non empty 1-sorted

for N being non empty NetStr over S holds

( N is Cauchy iff for A being Subset of S holds

( N is_eventually_in A or N is_eventually_in A ` ) );

for S being non empty 1-sorted

for N being non empty NetStr over S holds

( N is Cauchy iff for A being Subset of S holds

( N is_eventually_in A or N is_eventually_in A ` ) );

registration

let S be non empty 1-sorted ;

let F be ultra Filter of (BoolePoset ([#] S));

coherence

a_net F is Cauchy

end;
let F be ultra Filter of (BoolePoset ([#] S));

coherence

a_net F is Cauchy

proof end;

theorem :: YELLOW19:36

for T being non empty TopSpace holds

( T is compact iff for N being net of T st N is Cauchy holds

N is convergent )

( T is compact iff for N being net of T st N is Cauchy holds

N is convergent )

proof end;