:: by Artur Korni{\l}owicz

::

:: Received February 5, 1997

:: Copyright (c) 1997-2018 Association of Mizar Users

Lm1: for L being non empty RelStr

for f being sequence of the carrier of L

for n being Element of NAT holds { (f . k) where k is Element of NAT : k <= n } is non empty finite Subset of L

proof end;

definition
end;

:: deftheorem defines closed WAYBEL12:def 1 :

for T being TopStruct

for P being Subset of T holds

( P is closed iff P ` is open );

for T being TopStruct

for P being Subset of T holds

( P is closed iff P ` is open );

:: deftheorem defines dense WAYBEL12:def 2 :

for T being TopStruct

for F being Subset-Family of T holds

( F is dense iff for X being Subset of T st X in F holds

X is dense );

for T being TopStruct

for F being Subset-Family of T holds

( F is dense iff for X being Subset of T st X in F holds

X is dense );

theorem :: WAYBEL12:3

for L being non empty transitive RelStr

for A, B being Subset of L st A is_finer_than B holds

downarrow A c= downarrow B

for A, B being Subset of L st A is_finer_than B holds

downarrow A c= downarrow B

proof end;

theorem Th4: :: WAYBEL12:4

for L being non empty transitive RelStr

for A, B being Subset of L st A is_coarser_than B holds

uparrow A c= uparrow B

for A, B being Subset of L st A is_coarser_than B holds

uparrow A c= uparrow B

proof end;

theorem :: WAYBEL12:5

for L being non empty Poset

for D being non empty finite filtered Subset of L st ex_inf_of D,L holds

inf D in D

for D being non empty finite filtered Subset of L st ex_inf_of D,L holds

inf D in D

proof end;

theorem :: WAYBEL12:6

for L being non empty antisymmetric lower-bounded RelStr

for X being non empty lower Subset of L holds Bottom L in X

for X being non empty lower Subset of L holds Bottom L in X

proof end;

theorem :: WAYBEL12:7

for L being non empty antisymmetric lower-bounded RelStr

for X being non empty Subset of L holds Bottom L in downarrow X

for X being non empty Subset of L holds Bottom L in downarrow X

proof end;

theorem Th8: :: WAYBEL12:8

for L being non empty antisymmetric upper-bounded RelStr

for X being non empty upper Subset of L holds Top L in X

for X being non empty upper Subset of L holds Top L in X

proof end;

theorem Th9: :: WAYBEL12:9

for L being non empty antisymmetric upper-bounded RelStr

for X being non empty Subset of L holds Top L in uparrow X

for X being non empty Subset of L holds Top L in uparrow X

proof end;

theorem Th10: :: WAYBEL12:10

for L being antisymmetric lower-bounded with_infima RelStr

for X being Subset of L holds X "/\" {(Bottom L)} c= {(Bottom L)}

for X being Subset of L holds X "/\" {(Bottom L)} c= {(Bottom L)}

proof end;

theorem :: WAYBEL12:11

for L being antisymmetric lower-bounded with_infima RelStr

for X being non empty Subset of L holds X "/\" {(Bottom L)} = {(Bottom L)}

for X being non empty Subset of L holds X "/\" {(Bottom L)} = {(Bottom L)}

proof end;

theorem Th12: :: WAYBEL12:12

for L being antisymmetric upper-bounded with_suprema RelStr

for X being Subset of L holds X "\/" {(Top L)} c= {(Top L)}

for X being Subset of L holds X "\/" {(Top L)} c= {(Top L)}

proof end;

theorem :: WAYBEL12:13

for L being antisymmetric upper-bounded with_suprema RelStr

for X being non empty Subset of L holds X "\/" {(Top L)} = {(Top L)}

for X being non empty Subset of L holds X "\/" {(Top L)} = {(Top L)}

proof end;

theorem Th16: :: WAYBEL12:16

for L being non empty reflexive RelStr

for A, B being Subset of L st A c= B holds

( A is_finer_than B & A is_coarser_than B )

for A, B being Subset of L st A c= B holds

( A is_finer_than B & A is_coarser_than B )

proof end;

theorem Th17: :: WAYBEL12:17

for L being transitive antisymmetric with_infima RelStr

for V being Subset of L

for x, y being Element of L st x <= y holds

{y} "/\" V is_coarser_than {x} "/\" V

for V being Subset of L

for x, y being Element of L st x <= y holds

{y} "/\" V is_coarser_than {x} "/\" V

proof end;

theorem :: WAYBEL12:18

for L being transitive antisymmetric with_suprema RelStr

for V being Subset of L

for x, y being Element of L st x <= y holds

{x} "\/" V is_finer_than {y} "\/" V

for V being Subset of L

for x, y being Element of L st x <= y holds

{x} "\/" V is_finer_than {y} "\/" V

proof end;

theorem Th19: :: WAYBEL12:19

for L being non empty RelStr

for V, S, T being Subset of L st S is_coarser_than T & V is upper & T c= V holds

S c= V

for V, S, T being Subset of L st S is_coarser_than T & V is upper & T c= V holds

S c= V

proof end;

theorem :: WAYBEL12:20

for L being non empty RelStr

for V, S, T being Subset of L st S is_finer_than T & V is lower & T c= V holds

S c= V

for V, S, T being Subset of L st S is_finer_than T & V is lower & T c= V holds

S c= V

proof end;

Lm2: for L being non empty RelStr

for V being Subset of L holds { x where x is Element of L : V "/\" {x} c= V } is Subset of L

proof end;

theorem Th23: :: WAYBEL12:23

for L being upper-bounded Semilattice

for V being Subset of L holds not { x where x is Element of L : V "/\" {x} c= V } is empty

for V being Subset of L holds not { x where x is Element of L : V "/\" {x} c= V } is empty

proof end;

theorem Th24: :: WAYBEL12:24

for L being transitive antisymmetric with_infima RelStr

for V being Subset of L holds { x where x is Element of L : V "/\" {x} c= V } is filtered Subset of L

for V being Subset of L holds { x where x is Element of L : V "/\" {x} c= V } is filtered Subset of L

proof end;

theorem Th25: :: WAYBEL12:25

for L being transitive antisymmetric with_infima RelStr

for V being upper Subset of L holds { x where x is Element of L : V "/\" {x} c= V } is upper Subset of L

for V being upper Subset of L holds { x where x is Element of L : V "/\" {x} c= V } is upper Subset of L

proof end;

registration

let L be with_infima Poset;

coherence

for b_{1} being Subset of L st b_{1} is Open & b_{1} is lower holds

b_{1} is filtered
by Th26;

end;
coherence

for b

b

registration

let L be non empty reflexive antisymmetric continuous RelStr ;

coherence

for b_{1} being Subset of L st b_{1} is lower holds

b_{1} is Open

end;
coherence

for b

b

proof end;

registration
end;

theorem Th27: :: WAYBEL12:27

for L being Semilattice

for C being non empty Subset of L st ( for x, y being Element of L st x in C & y in C & not x <= y holds

y <= x ) holds

for Y being non empty finite Subset of C holds "/\" (Y,L) in Y

for C being non empty Subset of L st ( for x, y being Element of L st x in C & y in C & not x <= y holds

y <= x ) holds

for Y being non empty finite Subset of C holds "/\" (Y,L) in Y

proof end;

theorem :: WAYBEL12:28

for L being sup-Semilattice

for C being non empty Subset of L st ( for x, y being Element of L st x in C & y in C & not x <= y holds

y <= x ) holds

for Y being non empty finite Subset of C holds "\/" (Y,L) in Y

for C being non empty Subset of L st ( for x, y being Element of L st x in C & y in C & not x <= y holds

y <= x ) holds

for Y being non empty finite Subset of C holds "\/" (Y,L) in Y

proof end;

Lm3: for L being Semilattice

for F being Filter of L holds F = uparrow (fininfs F)

by WAYBEL_0:62;

definition

let L be Semilattice;

let F be Filter of L;

existence

ex b_{1} being Subset of L st F = uparrow (fininfs b_{1})

end;
let F be Filter of L;

existence

ex b

proof end;

:: deftheorem Def3 defines GeneratorSet WAYBEL12:def 3 :

for L being Semilattice

for F being Filter of L

for b_{3} being Subset of L holds

( b_{3} is GeneratorSet of F iff F = uparrow (fininfs b_{3}) );

for L being Semilattice

for F being Filter of L

for b

( b

registration

let L be Semilattice;

let F be Filter of L;

existence

not for b_{1} being GeneratorSet of F holds b_{1} is empty

end;
let F be Filter of L;

existence

not for b

proof end;

Lm4: for L being Semilattice

for F being Filter of L

for G being GeneratorSet of F holds G c= F

proof end;

theorem Th29: :: WAYBEL12:29

for L being Semilattice

for A being Subset of L

for B being non empty Subset of L st A is_coarser_than B holds

fininfs A is_coarser_than fininfs B

for A being Subset of L

for B being non empty Subset of L st A is_coarser_than B holds

fininfs A is_coarser_than fininfs B

proof end;

theorem Th30: :: WAYBEL12:30

for L being Semilattice

for F being Filter of L

for G being GeneratorSet of F

for A being non empty Subset of L st G is_coarser_than A & A is_coarser_than F holds

A is GeneratorSet of F

for F being Filter of L

for G being GeneratorSet of F

for A being non empty Subset of L st G is_coarser_than A & A is_coarser_than F holds

A is GeneratorSet of F

proof end;

theorem Th31: :: WAYBEL12:31

for L being Semilattice

for A being Subset of L

for f, g being sequence of the carrier of L st rng f = A & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) holds

A is_coarser_than rng g

for A being Subset of L

for f, g being sequence of the carrier of L st rng f = A & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) holds

A is_coarser_than rng g

proof end;

theorem Th32: :: WAYBEL12:32

for L being Semilattice

for F being Filter of L

for G being GeneratorSet of F

for f, g being sequence of the carrier of L st rng f = G & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) holds

rng g is GeneratorSet of F

for F being Filter of L

for G being GeneratorSet of F

for f, g being sequence of the carrier of L st rng f = G & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) holds

rng g is GeneratorSet of F

proof end;

:: Proposition 3.43.1

theorem Th33: :: WAYBEL12:33

for L being lower-bounded continuous LATTICE

for V being upper Open Subset of L

for F being Filter of L

for v being Element of L st V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable holds

ex O being Open Filter of L st

( O c= V & v in O & F c= O )

for V being upper Open Subset of L

for F being Filter of L

for v being Element of L st V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable holds

ex O being Open Filter of L st

( O c= V & v in O & F c= O )

proof end;

:: Corolarry 3.43.2

theorem Th34: :: WAYBEL12:34

for L being lower-bounded continuous LATTICE

for V being upper Open Subset of L

for N being non empty countable Subset of L

for v being Element of L st V "/\" N c= V & v in V holds

ex O being Open Filter of L st

( {v} "/\" N c= O & O c= V & v in O )

for V being upper Open Subset of L

for N being non empty countable Subset of L

for v being Element of L st V "/\" N c= V & v in V holds

ex O being Open Filter of L st

( {v} "/\" N c= O & O c= V & v in O )

proof end;

:: Proposition 3.43.3

theorem Th35: :: WAYBEL12:35

for L being lower-bounded continuous LATTICE

for V being upper Open Subset of L

for N being non empty countable Subset of L

for x, y being Element of L st V "/\" N c= V & y in V & not x in V holds

ex p being irreducible Element of L st

( x <= p & not p in uparrow ({y} "/\" N) )

for V being upper Open Subset of L

for N being non empty countable Subset of L

for x, y being Element of L st V "/\" N c= V & y in V & not x in V holds

ex p being irreducible Element of L st

( x <= p & not p in uparrow ({y} "/\" N) )

proof end;

:: Corollary 3.43.4

theorem Th36: :: WAYBEL12:36

for L being lower-bounded continuous LATTICE

for x being Element of L

for N being non empty countable Subset of L st ( for n, y being Element of L st not y <= x & n in N holds

not y "/\" n <= x ) holds

for y being Element of L st not y <= x holds

ex p being irreducible Element of L st

( x <= p & not p in uparrow ({y} "/\" N) )

for x being Element of L

for N being non empty countable Subset of L st ( for n, y being Element of L st not y <= x & n in N holds

not y "/\" n <= x ) holds

for y being Element of L st not y <= x holds

ex p being irreducible Element of L st

( x <= p & not p in uparrow ({y} "/\" N) )

proof end;

:: Definition 3.43.5

:: deftheorem defines dense WAYBEL12:def 4 :

for L being non empty RelStr

for u being Element of L holds

( u is dense iff for v being Element of L st v <> Bottom L holds

u "/\" v <> Bottom L );

for L being non empty RelStr

for u being Element of L holds

( u is dense iff for v being Element of L st v <> Bottom L holds

u "/\" v <> Bottom L );

registration

let L be upper-bounded Semilattice;

existence

ex b_{1} being Element of L st b_{1} is dense

end;
existence

ex b

proof end;

theorem :: WAYBEL12:37

for L being non trivial bounded Semilattice

for x being Element of L st x is dense holds

x <> Bottom L

for x being Element of L st x is dense holds

x <> Bottom L

proof end;

:: deftheorem Def5 defines dense WAYBEL12:def 5 :

for L being non empty RelStr

for D being Subset of L holds

( D is dense iff for d being Element of L st d in D holds

d is dense );

for L being non empty RelStr

for D being Subset of L holds

( D is dense iff for d being Element of L st d in D holds

d is dense );

registration

let L be upper-bounded Semilattice;

existence

ex b_{1} being Subset of L st

( not b_{1} is empty & b_{1} is finite & b_{1} is countable & b_{1} is dense )

end;
existence

ex b

( not b

proof end;

theorem Th39: :: WAYBEL12:39

for L being lower-bounded continuous LATTICE

for D being non empty countable dense Subset of L

for u being Element of L st u <> Bottom L holds

ex p being irreducible Element of L st

( p <> Top L & not p in uparrow ({u} "/\" D) )

for D being non empty countable dense Subset of L

for u being Element of L st u <> Bottom L holds

ex p being irreducible Element of L st

( p <> Top L & not p in uparrow ({u} "/\" D) )

proof end;

theorem Th40: :: WAYBEL12:40

for T being non empty TopSpace

for A being Element of (InclPoset the topology of T)

for B being Subset of T st A = B & B ` is irreducible holds

A is irreducible

for A being Element of (InclPoset the topology of T)

for B being Subset of T st A = B & B ` is irreducible holds

A is irreducible

proof end;

theorem Th41: :: WAYBEL12:41

for T being non empty TopSpace

for A being Element of (InclPoset the topology of T)

for B being Subset of T st A = B & A <> Top (InclPoset the topology of T) holds

( A is irreducible iff B ` is irreducible )

for A being Element of (InclPoset the topology of T)

for B being Subset of T st A = B & A <> Top (InclPoset the topology of T) holds

( A is irreducible iff B ` is irreducible )

proof end;

theorem Th42: :: WAYBEL12:42

for T being non empty TopSpace

for A being Element of (InclPoset the topology of T)

for B being Subset of T st A = B holds

( A is dense iff B is everywhere_dense )

for A being Element of (InclPoset the topology of T)

for B being Subset of T st A = B holds

( A is dense iff B is everywhere_dense )

proof end;

:: Theorem 3.43.8

theorem Th43: :: WAYBEL12:43

for T being non empty TopSpace st T is locally-compact holds

for D being countable Subset-Family of T st not D is empty & D is dense & D is open holds

for O being non empty Subset of T st O is open holds

ex A being irreducible Subset of T st

for V being Subset of T st V in D holds

A /\ O meets V

for D being countable Subset-Family of T st not D is empty & D is dense & D is open holds

for O being non empty Subset of T st O is open holds

ex A being irreducible Subset of T st

for V being Subset of T st V in D holds

A /\ O meets V

proof end;

definition

let T be non empty TopSpace;

( T is Baire iff for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds

( S is open & S is dense ) ) holds

ex I being Subset of T st

( I = Intersect F & I is dense ) )

end;
redefine attr T is Baire means :: WAYBEL12:def 6

for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds

( S is open & S is dense ) ) holds

ex I being Subset of T st

( I = Intersect F & I is dense );

compatibility for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds

( S is open & S is dense ) ) holds

ex I being Subset of T st

( I = Intersect F & I is dense );

( T is Baire iff for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds

( S is open & S is dense ) ) holds

ex I being Subset of T st

( I = Intersect F & I is dense ) )

proof end;

:: deftheorem defines Baire WAYBEL12:def 6 :

for T being non empty TopSpace holds

( T is Baire iff for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds

( S is open & S is dense ) ) holds

ex I being Subset of T st

( I = Intersect F & I is dense ) );

for T being non empty TopSpace holds

( T is Baire iff for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds

( S is open & S is dense ) ) holds

ex I being Subset of T st

( I = Intersect F & I is dense ) );

:: Corolarry 3.43.10