:: WAYBEL12 semantic presentation

Lm1: for L being non empty RelStr
for f being Function of NAT ,the carrier of L
for n being Nat holds { (f . k) where k is Nat : k <= n } is non empty finite Subset of L

proof end;

definition

let T be TopStruct ;
let P be Subset of T;
redefine attr P is closed means :: WAYBEL12:def 1
P ` is open;
compatibility

proof end;

end;

:: deftheorem defines closed WAYBEL12:def 1 :

definition

let T be TopStruct ;
let F be Subset-Family of T;
attr F is dense means :Def2: :: WAYBEL12:def 2
for X being Subset of T st X in F holds
X is dense;

end;

:: deftheorem Def2 defines dense WAYBEL12:def 2 :

registration

cluster empty 1-sorted ;
existence

proof end;

end;

registration

let S be empty 1-sorted ;
cluster the carrier of S -> empty ;
coherence by STRUCT_0:def 1;

end;

registration

let S be empty 1-sorted ;
cluster -> empty Element of bool the carrier of S;
coherence by XBOOLE_1:3;

end;

registration

cluster finite -> countable set ;
coherence by CARD_4:43;

end;

registration

cluster empty countable set ;
existence

proof end;

end;

registration

let S be 1-sorted ;
cluster empty countable Element of bool the carrier of S;
existence

proof end;

end;

registration

cluster non empty finite countable set ;
existence

proof end;

end;

registration

let L be non empty RelStr ;
cluster non empty finite countable Element of bool the carrier of L;
existence

proof end;

end;

registration

cluster infinite countable set ;
existence by CARD_4:44;

end;

registration

let S be 1-sorted ;
cluster empty countable Element of bool (bool the carrier of S);
existence

proof end;

end;

theorem :: WAYBEL12:1

canceled;

theorem Th2: :: WAYBEL12:2

for X, Y being set st Card X <=` Card Y & Y is countable holds
X is countable

proof end;

theorem Th3: :: WAYBEL12:3

for A being infinite countable set holds NAT ,A are_equipotent

proof end;

theorem Th4: :: WAYBEL12:4

for A being non empty countable set ex f being Function of NAT ,A st rng f = A

proof end;

Lm2: for S being 1-sorted
for X, Y being Subset of S holds (X \/ Y) ` = (X ` ) /\ (Y ` )
by SUBSET_1:29;

Lm3: for S being 1-sorted
for X, Y being Subset of S holds (X /\ Y) ` = (X ` ) \/ (Y ` )
by SUBSET_1:30;

theorem :: WAYBEL12:5

canceled;

theorem :: WAYBEL12:6

canceled;

theorem :: WAYBEL12:7

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

proof end;

theorem Th8: :: WAYBEL12:8

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

proof end;

theorem :: WAYBEL12:9

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

proof end;

theorem :: WAYBEL12:10

for L being non empty antisymmetric lower-bounded RelStr
for X being non empty lower Subset of L holds Bottom L in X

proof end;

theorem :: WAYBEL12:11

for L being non empty antisymmetric lower-bounded RelStr
for X being non empty Subset of L holds Bottom L in downarrow X

proof end;

theorem Th12: :: WAYBEL12:12

for L being non empty antisymmetric upper-bounded RelStr
for X being non empty upper Subset of L holds Top L in X

proof end;

theorem Th13: :: WAYBEL12:13

for L being non empty antisymmetric upper-bounded RelStr
for X being non empty Subset of L holds Top L in uparrow X

proof end;

theorem Th14: :: WAYBEL12:14

for L being antisymmetric lower-bounded with_infima RelStr
for X being Subset of L holds X "/\" {(Bottom L)} c= {(Bottom L)}

proof end;

theorem :: WAYBEL12:15

for L being antisymmetric lower-bounded with_infima RelStr
for X being non empty Subset of L holds X "/\" {(Bottom L)} = {(Bottom L)}

proof end;

theorem Th16: :: WAYBEL12:16

for L being antisymmetric upper-bounded with_suprema RelStr
for X being Subset of L holds X "\/" {(Top L)} c= {(Top L)}

proof end;

theorem :: WAYBEL12:17

for L being antisymmetric upper-bounded with_suprema RelStr
for X being non empty Subset of L holds X "\/" {(Top L)} = {(Top L)}

proof end;

theorem Th18: :: WAYBEL12:18

for L being upper-bounded Semilattice
for X being Subset of L holds {(Top L)} "/\" X = X

proof end;

theorem :: WAYBEL12:19

for L being lower-bounded with_suprema Poset
for X being Subset of L holds {(Bottom L)} "\/" X = X

proof end;

theorem Th20: :: WAYBEL12:20

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 )

proof end;

theorem Th21: :: WAYBEL12:21

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

proof end;

theorem :: WAYBEL12:22

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

proof end;

theorem Th23: :: WAYBEL12:23

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

proof end;

theorem :: WAYBEL12:24

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

proof end;

theorem Th25: :: WAYBEL12:25

for L being Semilattice
for F being filtered upper Subset of L holds F "/\" F = F

proof end;

theorem :: WAYBEL12:26

for L being sup-Semilattice
for I being directed lower Subset of L holds I "\/" I = I

proof end;

Lm4: 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 Th27: :: WAYBEL12:27

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

proof end;

theorem Th28: :: WAYBEL12:28

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

proof end;

theorem Th29: :: WAYBEL12:29

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

proof end;

theorem Th30: :: WAYBEL12:30

for L being with_infima Poset
for X being Subset of L st X is Open & X is lower holds
X is filtered

proof end;

registration

let L be with_infima Poset;
cluster Open lower -> filtered Element of bool the carrier of L;
coherence by Th30;

end;

registration

let L be non empty reflexive antisymmetric continuous RelStr ;
cluster lower -> Open Element of bool the carrier of L;
coherence

proof end;

end;

registration

let L be continuous Semilattice;
let x be Element of L;
cluster (downarrow x) ` -> Open ;
coherence

proof end;

end;

theorem Th31: :: WAYBEL12:31

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

proof end;

theorem :: WAYBEL12:32

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

proof end;

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

proof end;

definition

let L be Semilattice;
let F be Filter of L;
mode GeneratorSet of F -> Subset of L means :Def3: :: WAYBEL12:def 3
F = uparrow (fininfs it);
existence

proof end;

end;

:: deftheorem Def3 defines GeneratorSet WAYBEL12:def 3 :

registration

let L be Semilattice;
let F be Filter of L;
cluster non empty GeneratorSet of F;
existence

proof end;

end;

Lm6: for L being Semilattice
for F being Filter of L
for G being GeneratorSet of F holds G c= F

proof end;

theorem Th33: :: WAYBEL12:33

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

proof end;

theorem Th34: :: WAYBEL12:34

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

proof end;

theorem Th35: :: WAYBEL12:35

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

proof end;

theorem Th36: :: WAYBEL12:36

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

proof end;

theorem Th37: :: WAYBEL12:37

for L being lower-bounded continuous LATTICE
for V being Open upper 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;

theorem Th38: :: WAYBEL12:38

for L being lower-bounded continuous LATTICE
for V being Open upper 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;

theorem Th39: :: WAYBEL12:39

for L being lower-bounded continuous LATTICE
for V being Open upper 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;

theorem Th40: :: WAYBEL12:40

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

proof end;

definition

let L be non empty RelStr ;
let u be Element of L;
attr u is dense means :Def4: :: WAYBEL12:def 4
for v being Element of L st v <> Bottom L holds
u "/\" v <> Bottom L;

end;

:: deftheorem Def4 defines dense WAYBEL12:def 4 :

registration

let L be upper-bounded Semilattice;
cluster Top L -> dense ;
coherence

proof end;

end;

registration

let L be upper-bounded Semilattice;
cluster dense Element of the carrier of L;
existence

proof end;

end;

theorem :: WAYBEL12:41

for L being bounded non trivial Semilattice
for x being Element of L st x is dense holds
x <> Bottom L

proof end;

definition

let L be non empty RelStr ;
let D be Subset of L;
attr D is dense means :Def5: :: WAYBEL12:def 5
for d being Element of L st d in D holds
d is dense;

end;

:: deftheorem Def5 defines dense WAYBEL12:def 5 :

theorem Th42: :: WAYBEL12:42

for L being upper-bounded Semilattice holds {(Top L)} is dense

proof end;

registration

let L be upper-bounded Semilattice;
cluster non empty finite countable dense Element of bool the carrier of L;
existence

proof end;

end;

theorem Th43: :: WAYBEL12:43

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

proof end;

theorem Th44: :: WAYBEL12:44

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 meet-irreducible

proof end;

theorem Th45: :: WAYBEL12:45

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 meet-irreducible iff B ` is irreducible )

proof end;

theorem Th46: :: WAYBEL12:46

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 )

proof end;

theorem Th47: :: WAYBEL12:47

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

proof end;

definition

let T be non empty TopSpace;
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

proof end;

end;

:: deftheorem defines Baire WAYBEL12:def 6 :

theorem :: WAYBEL12:48

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

proof end;