:: WAYBEL12 semantic presentation

Lemma1: for b₁ being non empty RelStr
for b₂ being Function of NAT ,the carrier of b₁
for b₃ being Nat holds { (b₂ . b₄) where B is Nat : b₄ <= b₃ } is non empty finite Subset of b₁

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
redefine attr a₂ is closed means :: WAYBEL12:def 1
a₂ ` is open;
compatibility

proof end;

end;

:: deftheorem Def1 defines closed WAYBEL12:def 1 :

definition

let c₁ be TopStruct ;
let c₂ be Subset-Family of c₁;
attr a₂ is dense means :Def2: :: WAYBEL12:def 2
for b₁ being Subset of a₁ st b₁ in a₂ holds
b₁ is dense;

end;

:: deftheorem Def2 defines dense WAYBEL12:def 2 :

registration

cluster empty 1-sorted ;
existence

proof end;

end;

registration

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

end;

registration

let c₁ be empty 1-sorted ;
cluster -> empty Element of bool the carrier of a₁;
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 c₁ be 1-sorted ;
cluster empty countable Element of bool the carrier of a₁;
existence

proof end;

end;

registration

cluster non empty finite countable set ;
existence

proof end;

end;

registration

let c₁ be non empty RelStr ;
cluster non empty finite countable Element of bool the carrier of a₁;
existence

proof end;

end;

registration

cluster infinite countable set ;
existence by CARD_4:44;

end;

registration

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

proof end;

end;

theorem Th1: :: WAYBEL12:1

canceled;

theorem Th2: :: WAYBEL12:2

for b₁, b₂ being set st Card b₁ <=` Card b₂ & b₂ is countable holds
b₁ is countable

proof end;

theorem Th3: :: WAYBEL12:3

for b₁ being infinite countable set holds NAT ,b₁ are_equipotent

proof end;

theorem Th4: :: WAYBEL12:4

for b₁ being non empty countable set ex b₂ being Function of NAT ,b₁ st rng b₂ = b₁

proof end;

Lemma6: for b₁ being 1-sorted
for b₂, b₃ being Subset of b₁ holds (b₂ \/ b₃) ` = (b₂ ` ) /\ (b₃ ` )
by SUBSET_1:29;

Lemma7: for b₁ being 1-sorted
for b₂, b₃ being Subset of b₁ holds (b₂ /\ b₃) ` = (b₂ ` ) \/ (b₃ ` )
by SUBSET_1:30;

theorem Th5: :: WAYBEL12:5

canceled;

theorem Th6: :: WAYBEL12:6

canceled;

theorem Th7: :: WAYBEL12:7

for b₁ being non empty transitive RelStr
for b₂, b₃ being Subset of b₁ st b₂ is_finer_than b₃ holds
downarrow b₂ c= downarrow b₃

proof end;

theorem Th8: :: WAYBEL12:8

for b₁ being non empty transitive RelStr
for b₂, b₃ being Subset of b₁ st b₂ is_coarser_than b₃ holds
uparrow b₂ c= uparrow b₃

proof end;

theorem Th9: :: WAYBEL12:9

for b₁ being non empty Poset
for b₂ being non empty finite filtered Subset of b₁ st ex_inf_of b₂,b₁ holds
inf b₂ in b₂

proof end;

theorem Th10: :: WAYBEL12:10

for b₁ being non empty antisymmetric lower-bounded RelStr
for b₂ being non empty lower Subset of b₁ holds Bottom b₁ in b₂

proof end;

theorem Th11: :: WAYBEL12:11

for b₁ being non empty antisymmetric lower-bounded RelStr
for b₂ being non empty Subset of b₁ holds Bottom b₁ in downarrow b₂

proof end;

theorem Th12: :: WAYBEL12:12

for b₁ being non empty antisymmetric upper-bounded RelStr
for b₂ being non empty upper Subset of b₁ holds Top b₁ in b₂

proof end;

theorem Th13: :: WAYBEL12:13

for b₁ being non empty antisymmetric upper-bounded RelStr
for b₂ being non empty Subset of b₁ holds Top b₁ in uparrow b₂

proof end;

theorem Th14: :: WAYBEL12:14

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

proof end;

theorem Th15: :: WAYBEL12:15

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

proof end;

theorem Th16: :: WAYBEL12:16

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

proof end;

theorem Th17: :: WAYBEL12:17

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

proof end;

theorem Th18: :: WAYBEL12:18

for b₁ being upper-bounded Semilattice
for b₂ being Subset of b₁ holds {(Top b₁)} "/\" b₂ = b₂

proof end;

theorem Th19: :: WAYBEL12:19

for b₁ being lower-bounded with_suprema Poset
for b₂ being Subset of b₁ holds {(Bottom b₁)} "\/" b₂ = b₂

proof end;

theorem Th20: :: WAYBEL12:20

for b₁ being non empty reflexive RelStr
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
( b₂ is_finer_than b₃ & b₂ is_coarser_than b₃ )

proof end;

theorem Th21: :: WAYBEL12:21

for b₁ being transitive antisymmetric with_infima RelStr
for b₂ being Subset of b₁
for b₃, b₄ being Element of b₁ st b₃ <= b₄ holds
{b₄} "/\" b₂ is_coarser_than {b₃} "/\" b₂

proof end;

theorem Th22: :: WAYBEL12:22

for b₁ being transitive antisymmetric with_suprema RelStr
for b₂ being Subset of b₁
for b₃, b₄ being Element of b₁ st b₃ <= b₄ holds
{b₃} "\/" b₂ is_finer_than {b₄} "\/" b₂

proof end;

theorem Th23: :: WAYBEL12:23

for b₁ being non empty RelStr
for b₂, b₃, b₄ being Subset of b₁ st b₃ is_coarser_than b₄ & b₂ is upper & b₄ c= b₂ holds
b₃ c= b₂

proof end;

theorem Th24: :: WAYBEL12:24

for b₁ being non empty RelStr
for b₂, b₃, b₄ being Subset of b₁ st b₃ is_finer_than b₄ & b₂ is lower & b₄ c= b₂ holds
b₃ c= b₂

proof end;

theorem Th25: :: WAYBEL12:25

for b₁ being Semilattice
for b₂ being filtered upper Subset of b₁ holds b₂ "/\" b₂ = b₂

proof end;

theorem Th26: :: WAYBEL12:26

for b₁ being sup-Semilattice
for b₂ being directed lower Subset of b₁ holds b₂ "\/" b₂ = b₂

proof end;

Lemma18: for b₁ being non empty RelStr
for b₂ being Subset of b₁ holds { b₃ where B is Element of b₁ : b₂ "/\" {b₃} c= b₂ } is Subset of b₁

proof end;

theorem Th27: :: WAYBEL12:27

for b₁ being upper-bounded Semilattice
for b₂ being Subset of b₁ holds not { b₃ where B is Element of b₁ : b₂ "/\" {b₃} c= b₂ } is empty

proof end;

theorem Th28: :: WAYBEL12:28

for b₁ being transitive antisymmetric with_infima RelStr
for b₂ being Subset of b₁ holds { b₃ where B is Element of b₁ : b₂ "/\" {b₃} c= b₂ } is filtered Subset of b₁

proof end;

theorem Th29: :: WAYBEL12:29

for b₁ being transitive antisymmetric with_infima RelStr
for b₂ being upper Subset of b₁ holds { b₃ where B is Element of b₁ : b₂ "/\" {b₃} c= b₂ } is upper Subset of b₁

proof end;

theorem Th30: :: WAYBEL12:30

for b₁ being with_infima Poset
for b₂ being Subset of b₁ st b₂ is Open & b₂ is lower holds
b₂ is filtered

proof end;

registration

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

end;

registration

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

proof end;

end;

registration

let c₁ be continuous Semilattice;
let c₂ be Element of c₁;
cluster (downarrow a₂) ` -> Open ;
coherence

proof end;

end;

theorem Th31: :: WAYBEL12:31

for b₁ being Semilattice
for b₂ being non empty Subset of b₁ st ( for b₃, b₄ being Element of b₁ st b₃ in b₂ & b₄ in b₂ & not b₃ <= b₄ holds
b₄ <= b₃ ) holds
for b₃ being non empty finite Subset of b₂ holds "/\" b₃,b₁ in b₃

proof end;

theorem Th32: :: WAYBEL12:32

for b₁ being sup-Semilattice
for b₂ being non empty Subset of b₁ st ( for b₃, b₄ being Element of b₁ st b₃ in b₂ & b₄ in b₂ & not b₃ <= b₄ holds
b₄ <= b₃ ) holds
for b₃ being non empty finite Subset of b₂ holds "\/" b₃,b₁ in b₃

proof end;

Lemma24: for b₁ being Semilattice
for b₂ being Filter of b₁ holds b₂ = uparrow (fininfs b₂)

proof end;

definition

let c₁ be Semilattice;
let c₂ be Filter of c₁;
mode GeneratorSet of c₂ -> Subset of a₁ means :Def3: :: WAYBEL12:def 3
a₂ = uparrow (fininfs a₃);
existence

proof end;

end;

:: deftheorem Def3 defines GeneratorSet WAYBEL12:def 3 :

registration

let c₁ be Semilattice;
let c₂ be Filter of c₁;
cluster non empty GeneratorSet of a₂;
existence

proof end;

end;

Lemma26: for b₁ being Semilattice
for b₂ being Filter of b₁
for b₃ being GeneratorSet of b₂ holds b₃ c= b₂

proof end;

theorem Th33: :: WAYBEL12:33

for b₁ being Semilattice
for b₂ being Subset of b₁
for b₃ being non empty Subset of b₁ st b₂ is_coarser_than b₃ holds
fininfs b₂ is_coarser_than fininfs b₃

proof end;

theorem Th34: :: WAYBEL12:34

for b₁ being Semilattice
for b₂ being Filter of b₁
for b₃ being GeneratorSet of b₂
for b₄ being non empty Subset of b₁ st b₃ is_coarser_than b₄ & b₄ is_coarser_than b₂ holds
b₄ is GeneratorSet of b₂

proof end;

theorem Th35: :: WAYBEL12:35

for b₁ being Semilattice
for b₂ being Subset of b₁
for b₃, b₄ being Function of NAT ,the carrier of b₁ st rng b₃ = b₂ & ( for b₅ being Element of NAT holds b₄ . b₅ = "/\" { (b₃ . b₆) where B is Nat : b₆ <= b₅ } ,b₁ ) holds
b₂ is_coarser_than rng b₄

proof end;

theorem Th36: :: WAYBEL12:36

for b₁ being Semilattice
for b₂ being Filter of b₁
for b₃ being GeneratorSet of b₂
for b₄, b₅ being Function of NAT ,the carrier of b₁ st rng b₄ = b₃ & ( for b₆ being Element of NAT holds b₅ . b₆ = "/\" { (b₄ . b₇) where B is Nat : b₇ <= b₆ } ,b₁ ) holds
rng b₅ is GeneratorSet of b₂

proof end;

theorem Th37: :: WAYBEL12:37

for b₁ being lower-bounded continuous LATTICE
for b₂ being Open upper Subset of b₁
for b₃ being Filter of b₁
for b₄ being Element of b₁ st b₂ "/\" b₃ c= b₂ & b₄ in b₂ & ex b₅ being non empty GeneratorSet of b₃ st b₅ is countable holds
ex b₅ being Open Filter of b₁ st
( b₅ c= b₂ & b₄ in b₅ & b₃ c= b₅ )

proof end;

theorem Th38: :: WAYBEL12:38

for b₁ being lower-bounded continuous LATTICE
for b₂ being Open upper Subset of b₁
for b₃ being non empty countable Subset of b₁
for b₄ being Element of b₁ st b₂ "/\" b₃ c= b₂ & b₄ in b₂ holds
ex b₅ being Open Filter of b₁ st
( {b₄} "/\" b₃ c= b₅ & b₅ c= b₂ & b₄ in b₅ )

proof end;

theorem Th39: :: WAYBEL12:39

for b₁ being lower-bounded continuous LATTICE
for b₂ being Open upper Subset of b₁
for b₃ being non empty countable Subset of b₁
for b₄, b₅ being Element of b₁ st b₂ "/\" b₃ c= b₂ & b₅ in b₂ & not b₄ in b₂ holds
ex b₆ being irreducible Element of b₁ st
( b₄ <= b₆ & not b₆ in uparrow ({b₅} "/\" b₃) )

proof end;

theorem Th40: :: WAYBEL12:40

for b₁ being lower-bounded continuous LATTICE
for b₂ being Element of b₁
for b₃ being non empty countable Subset of b₁ st ( for b₄, b₅ being Element of b₁ st not b₅ <= b₂ & b₄ in b₃ holds
not b₅ "/\" b₄ <= b₂ ) holds
for b₄ being Element of b₁ st not b₄ <= b₂ holds
ex b₅ being irreducible Element of b₁ st
( b₂ <= b₅ & not b₅ in uparrow ({b₄} "/\" b₃) )

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
attr a₂ is dense means :Def4: :: WAYBEL12:def 4
for b₁ being Element of a₁ st b₁ <> Bottom a₁ holds
a₂ "/\" b₁ <> Bottom a₁;

end;

:: deftheorem Def4 defines dense WAYBEL12:def 4 :

registration

let c₁ be upper-bounded Semilattice;
cluster Top a₁ -> dense ;
coherence

proof end;

end;

registration

let c₁ be upper-bounded Semilattice;
cluster dense Element of the carrier of a₁;
existence

proof end;

end;

theorem Th41: :: WAYBEL12:41

for b₁ being bounded non trivial Semilattice
for b₂ being Element of b₁ st b₂ is dense holds
b₂ <> Bottom b₁

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be Subset of c₁;
attr a₂ is dense means :Def5: :: WAYBEL12:def 5
for b₁ being Element of a₁ st b₁ in a₂ holds
b₁ is dense;

end;

:: deftheorem Def5 defines dense WAYBEL12:def 5 :

theorem Th42: :: WAYBEL12:42

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

proof end;

registration

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

proof end;

end;

theorem Th43: :: WAYBEL12:43

for b₁ being lower-bounded continuous LATTICE
for b₂ being non empty countable dense Subset of b₁
for b₃ being Element of b₁ st b₃ <> Bottom b₁ holds
ex b₄ being irreducible Element of b₁ st
( b₄ <> Top b₁ & not b₄ in uparrow ({b₃} "/\" b₂) )

proof end;

theorem Th44: :: WAYBEL12:44

for b₁ being non empty TopSpace
for b₂ being Element of (InclPoset the topology of b₁)
for b₃ being Subset of b₁ st b₂ = b₃ & b₃ ` is irreducible holds
b₂ is meet-irreducible

proof end;

theorem Th45: :: WAYBEL12:45

for b₁ being non empty TopSpace
for b₂ being Element of (InclPoset the topology of b₁)
for b₃ being Subset of b₁ st b₂ = b₃ & b₂ <> Top (InclPoset the topology of b₁) holds
( b₂ is meet-irreducible iff b₃ ` is irreducible )

proof end;

theorem Th46: :: WAYBEL12:46

for b₁ being non empty TopSpace
for b₂ being Element of (InclPoset the topology of b₁)
for b₃ being Subset of b₁ st b₂ = b₃ holds
( b₂ is dense iff b₃ is everywhere_dense )

proof end;

theorem Th47: :: WAYBEL12:47

for b₁ being non empty TopSpace st b₁ is locally-compact holds
for b₂ being countable Subset-Family of b₁ st not b₂ is empty & b₂ is dense & b₂ is open holds
for b₃ being non empty Subset of b₁ st b₃ is open holds
ex b₄ being irreducible Subset of b₁ st
for b₅ being Subset of b₁ st b₅ in b₂ holds
b₄ /\ b₃ meets b₅

proof end;

definition

let c₁ be non empty TopSpace;
redefine attr a₁ is Baire means :: WAYBEL12:def 6
for b₁ being Subset-Family of a₁ st b₁ is countable & ( for b₂ being Subset of a₁ st b₂ in b₁ holds
( b₂ is open & b₂ is dense ) ) holds
ex b₂ being Subset of a₁ st
( b₂ = Intersect b₁ & b₂ is dense );
compatibility

proof end;

end;

:: deftheorem Def6 defines Baire WAYBEL12:def 6 :

theorem Th48: :: WAYBEL12:48

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

proof end;