:: WAYBEL_7 semantic presentation

theorem Th1: :: WAYBEL_7:1

canceled;

theorem Th2: :: WAYBEL_7:2

canceled;

theorem Th3: :: WAYBEL_7:3

for b₁ being complete LATTICE
for b₂, b₃ being set st b₂ c= b₃ holds
( "\/" b₂,b₁ <= "\/" b₃,b₁ & "/\" b₂,b₁ >= "/\" b₃,b₁ )

proof end;

theorem Th4: :: WAYBEL_7:4

for b₁ being set holds the carrier of (BoolePoset b₁) = bool b₁

proof end;

theorem Th5: :: WAYBEL_7:5

for b₁ being non empty antisymmetric bounded RelStr holds
( b₁ is trivial iff Top b₁ = Bottom b₁ )

proof end;

registration

let c₁ be set ;
cluster BoolePoset a₁ -> Boolean ;
coherence ;

end;

registration

let c₁ be non empty set ;
cluster BoolePoset a₁ -> non trivial Boolean ;
coherence

proof end;

end;

theorem Th6: :: WAYBEL_7:6

canceled;

theorem Th7: :: WAYBEL_7:7

canceled;

theorem Th8: :: WAYBEL_7:8

for b₁ being non empty lower-bounded Poset
for b₂ being Filter of b₁ holds
( b₂ is proper iff not Bottom b₁ in b₂ )

proof end;

registration

cluster non trivial strict Boolean RelStr ;
existence

proof end;

end;

registration

let c₁ be set ;
cluster non empty finite Element of bool (bool a₁);
existence

proof end;

end;

registration

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

proof end;

end;

registration

let c₁ be non empty non trivial upper-bounded Poset;
cluster proper Element of bool the carrier of a₁;
existence

proof end;

end;

theorem Th9: :: WAYBEL_7:9

for b₁ being set
for b₂ being Element of (BoolePoset b₁) holds 'not' b₂ = b₁ \ b₂

proof end;

theorem Th10: :: WAYBEL_7:10

for b₁ being set
for b₂ being Subset of (BoolePoset b₁) holds
( b₂ is lower iff for b₃, b₄ being set st b₃ c= b₄ & b₄ in b₂ holds
b₃ in b₂ )

proof end;

theorem Th11: :: WAYBEL_7:11

for b₁ being set
for b₂ being Subset of (BoolePoset b₁) holds
( b₂ is upper iff for b₃, b₄ being set st b₃ c= b₄ & b₄ c= b₁ & b₃ in b₂ holds
b₄ in b₂ )

proof end;

theorem Th12: :: WAYBEL_7:12

for b₁ being set
for b₂ being lower Subset of (BoolePoset b₁) holds
( b₂ is directed iff for b₃, b₄ being set st b₃ in b₂ & b₄ in b₂ holds
b₃ \/ b₄ in b₂ )

proof end;

theorem Th13: :: WAYBEL_7:13

for b₁ being set
for b₂ being upper Subset of (BoolePoset b₁) holds
( b₂ is filtered iff for b₃, b₄ being set st b₃ in b₂ & b₄ in b₂ holds
b₃ /\ b₄ in b₂ )

proof end;

theorem Th14: :: WAYBEL_7:14

for b₁ being set
for b₂ being non empty lower Subset of (BoolePoset b₁) holds
( b₂ is directed iff for b₃ being finite Subset-Family of b₁ st b₃ c= b₂ holds
union b₃ in b₂ )

proof end;

theorem Th15: :: WAYBEL_7:15

for b₁ being set
for b₂ being non empty upper Subset of (BoolePoset b₁) holds
( b₂ is filtered iff for b₃ being finite Subset-Family of b₁ st b₃ c= b₂ holds
Intersect b₃ in b₂ )

proof end;

definition

let c₁ be with_infima Poset;
let c₂ be Ideal of c₁;
attr a₂ is prime means :Def1: :: WAYBEL_7:def 1
for b₁, b₂ being Element of a₁ holds
( not b₁ "/\" b₂ in a₂ or b₁ in a₂ or b₂ in a₂ );

end;

:: deftheorem Def1 defines prime WAYBEL_7:def 1 :

theorem Th16: :: WAYBEL_7:16

for b₁ being with_infima Poset
for b₂ being Ideal of b₁ holds
( b₂ is prime iff for b₃ being non empty finite Subset of b₁ st inf b₃ in b₂ holds
ex b₄ being Element of b₁ st
( b₄ in b₃ & b₄ in b₂ ) )

proof end;

registration

let c₁ be LATTICE;
cluster prime Element of bool the carrier of a₁;
existence

proof end;

end;

theorem Th17: :: WAYBEL_7:17

for b₁, b₂ being LATTICE st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₃ being set st b₃ is prime Ideal of b₁ holds
b₃ is prime Ideal of b₂

proof end;

definition

let c₁ be with_suprema Poset;
let c₂ be Filter of c₁;
attr a₂ is prime means :Def2: :: WAYBEL_7:def 2
for b₁, b₂ being Element of a₁ holds
( not b₁ "\/" b₂ in a₂ or b₁ in a₂ or b₂ in a₂ );

end;

:: deftheorem Def2 defines prime WAYBEL_7:def 2 :

theorem Th18: :: WAYBEL_7:18

for b₁ being with_suprema Poset
for b₂ being Filter of b₁ holds
( b₂ is prime iff for b₃ being non empty finite Subset of b₁ st sup b₃ in b₂ holds
ex b₄ being Element of b₁ st
( b₄ in b₃ & b₄ in b₂ ) )

proof end;

registration

let c₁ be LATTICE;
cluster prime Element of bool the carrier of a₁;
existence

proof end;

end;

theorem Th19: :: WAYBEL_7:19

for b₁, b₂ being LATTICE st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₃ being set st b₃ is prime Filter of b₁ holds
b₃ is prime Filter of b₂

proof end;

theorem Th20: :: WAYBEL_7:20

for b₁ being LATTICE
for b₂ being set holds
( b₂ is prime Ideal of b₁ iff b₂ is prime Filter of (b₁ opp ) )

proof end;

theorem Th21: :: WAYBEL_7:21

for b₁ being LATTICE
for b₂ being set holds
( b₂ is prime Filter of b₁ iff b₂ is prime Ideal of (b₁ opp ) )

proof end;

theorem Th22: :: WAYBEL_7:22

for b₁ being with_infima Poset
for b₂ being Ideal of b₁ holds
( b₂ is prime iff ( b₂ ` is Filter of b₁ or b₂ ` = {} ) )

proof end;

theorem Th23: :: WAYBEL_7:23

for b₁ being LATTICE
for b₂ being Ideal of b₁ holds
( b₂ is prime iff b₂ in PRIME (InclPoset (Ids b₁)) )

proof end;

theorem Th24: :: WAYBEL_7:24

for b₁ being Boolean LATTICE
for b₂ being Filter of b₁ holds
( b₂ is prime iff for b₃ being Element of b₁ holds
( b₃ in b₂ or 'not' b₃ in b₂ ) )

proof end;

theorem Th25: :: WAYBEL_7:25

for b₁ being set
for b₂ being Filter of (BoolePoset b₁) holds
( b₂ is prime iff for b₃ being Subset of b₁ holds
( b₃ in b₂ or b₁ \ b₃ in b₂ ) )

proof end;

definition

let c₁ be non empty Poset;
let c₂ be Filter of c₁;
attr a₂ is ultra means :Def3: :: WAYBEL_7:def 3
( a₂ is proper & ( for b₁ being Filter of a₁ holds
( not a₂ c= b₁ or a₂ = b₁ or b₁ = the carrier of a₁ ) ) );

end;

:: deftheorem Def3 defines ultra WAYBEL_7:def 3 :

registration

let c₁ be non empty Poset;
cluster ultra -> proper Element of bool the carrier of a₁;
coherence by Def3;

end;

Lemma18: for b₁ being with_infima Poset
for b₂ being Filter of b₁
for b₃ being non empty finite Subset of b₁
for b₄ being Element of b₁ st b₄ in uparrow (fininfs (b₂ \/ b₃)) holds
ex b₅ being Element of b₁ st
( b₅ in b₂ & b₄ >= b₅ "/\" (inf b₃) )

proof end;

theorem Th26: :: WAYBEL_7:26

for b₁ being Boolean LATTICE
for b₂ being Filter of b₁ holds
( ( b₂ is proper & b₂ is prime ) iff b₂ is ultra )

proof end;

Lemma20: for b₁ being with_suprema Poset
for b₂ being Ideal of b₁
for b₃ being non empty finite Subset of b₁
for b₄ being Element of b₁ st b₄ in downarrow (finsups (b₂ \/ b₃)) holds
ex b₅ being Element of b₁ st
( b₅ in b₂ & b₄ <= b₅ "\/" (sup b₃) )

proof end;

theorem Th27: :: WAYBEL_7:27

for b₁ being distributive LATTICE
for b₂ being Ideal of b₁
for b₃ being Filter of b₁ st b₂ misses b₃ holds
ex b₄ being Ideal of b₁ st
( b₄ is prime & b₂ c= b₄ & b₄ misses b₃ )

proof end;

theorem Th28: :: WAYBEL_7:28

for b₁ being distributive LATTICE
for b₂ being Ideal of b₁
for b₃ being Element of b₁ st not b₃ in b₂ holds
ex b₄ being Ideal of b₁ st
( b₄ is prime & b₂ c= b₄ & not b₃ in b₄ )

proof end;

theorem Th29: :: WAYBEL_7:29

for b₁ being distributive LATTICE
for b₂ being Ideal of b₁
for b₃ being Filter of b₁ st b₂ misses b₃ holds
ex b₄ being Filter of b₁ st
( b₄ is prime & b₃ c= b₄ & b₂ misses b₄ )

proof end;

theorem Th30: :: WAYBEL_7:30

for b₁ being non trivial Boolean LATTICE
for b₂ being proper Filter of b₁ ex b₃ being Filter of b₁ st
( b₂ c= b₃ & b₃ is ultra )

proof end;

definition

let c₁ be TopSpace;
let c₂, c₃ be set ;
pred c₃ is_a_cluster_point_of c₂,c₁ means :Def4: :: WAYBEL_7:def 4
for b₁ being Subset of a₁ st b₁ is open & a₃ in b₁ holds
for b₂ being set st b₂ in a₂ holds
b₁ meets b₂;
pred c₃ is_a_convergence_point_of c₂,c₁ means :Def5: :: WAYBEL_7:def 5
for b₁ being Subset of a₁ st b₁ is open & a₃ in b₁ holds
b₁ in a₂;

end;

:: deftheorem Def4 defines is_a_cluster_point_of WAYBEL_7:def 4 :

:: deftheorem Def5 defines is_a_convergence_point_of WAYBEL_7:def 5 :

registration

let c₁ be non empty set ;
cluster proper ultra Element of bool the carrier of (BoolePoset a₁);
existence

proof end;

end;

theorem Th31: :: WAYBEL_7:31

for b₁ being non empty TopSpace
for b₂ being ultra Filter of (BoolePoset the carrier of b₁)
for b₃ being set holds
( b₃ is_a_cluster_point_of b₂,b₁ iff b₃ is_a_convergence_point_of b₂,b₁ )

proof end;

theorem Th32: :: WAYBEL_7:32

for b₁ being non empty TopSpace
for b₂, b₃ being Element of (InclPoset the topology of b₁) st b₂ << b₃ holds
for b₄ being proper Filter of (BoolePoset the carrier of b₁) st b₂ in b₄ holds
ex b₅ being Element of b₁ st
( b₅ in b₃ & b₅ is_a_cluster_point_of b₄,b₁ )

proof end;

theorem Th33: :: WAYBEL_7:33

for b₁ being non empty TopSpace
for b₂, b₃ being Element of (InclPoset the topology of b₁) st b₂ << b₃ holds
for b₄ being ultra Filter of (BoolePoset the carrier of b₁) st b₂ in b₄ holds
ex b₅ being Element of b₁ st
( b₅ in b₃ & b₅ is_a_convergence_point_of b₄,b₁ )

proof end;

theorem Th34: :: WAYBEL_7:34

for b₁ being non empty TopSpace
for b₂, b₃ being Element of (InclPoset the topology of b₁) st b₂ c= b₃ & ( for b₄ being ultra Filter of (BoolePoset the carrier of b₁) st b₂ in b₄ holds
ex b₅ being Element of b₁ st
( b₅ in b₃ & b₅ is_a_convergence_point_of b₄,b₁ ) ) holds
b₂ << b₃

proof end;

theorem Th35: :: WAYBEL_7:35

for b₁ being non empty TopSpace
for b₂ being prebasis of b₁
for b₃, b₄ being Element of (InclPoset the topology of b₁) st b₃ c= b₄ holds
( b₃ << b₄ iff for b₅ being Subset of b₂ st b₄ c= union b₅ holds
ex b₆ being finite Subset of b₅ st b₃ c= union b₆ )

proof end;

theorem Th36: :: WAYBEL_7:36

for b₁ being distributive complete LATTICE
for b₂, b₃ being Element of b₁ holds
( b₂ << b₃ iff for b₄ being prime Ideal of b₁ st b₃ <= sup b₄ holds
b₂ in b₄ )

proof end;

theorem Th37: :: WAYBEL_7:37

for b₁ being LATTICE
for b₂ being Element of b₁ st b₂ is prime holds
downarrow b₂ is prime

proof end;

definition

let c₁ be LATTICE;
let c₂ be Element of c₁;
attr a₂ is pseudoprime means :Def6: :: WAYBEL_7:def 6
ex b₁ being prime Ideal of a₁ st a₂ = sup b₁;

end;

:: deftheorem Def6 defines pseudoprime WAYBEL_7:def 6 :

theorem Th38: :: WAYBEL_7:38

for b₁ being LATTICE
for b₂ being Element of b₁ st b₂ is prime holds
b₂ is pseudoprime

proof end;

theorem Th39: :: WAYBEL_7:39

for b₁ being continuous LATTICE
for b₂ being Element of b₁ st b₂ is pseudoprime holds
for b₃ being non empty finite Subset of b₁ st inf b₃ << b₂ holds
ex b₄ being Element of b₁ st
( b₄ in b₃ & b₄ <= b₂ )

proof end;

theorem Th40: :: WAYBEL_7:40

for b₁ being continuous LATTICE
for b₂ being Element of b₁ st ( b₂ <> Top b₁ or not Top b₁ is compact ) & ( for b₃ being non empty finite Subset of b₁ st inf b₃ << b₂ holds
ex b₄ being Element of b₁ st
( b₄ in b₃ & b₄ <= b₂ ) ) holds
uparrow (fininfs ((downarrow b₂) ` )) misses waybelow b₂

proof end;

theorem Th41: :: WAYBEL_7:41

for b₁ being continuous LATTICE st Top b₁ is compact holds
( ( for b₂ being non empty finite Subset of b₁ st inf b₂ << Top b₁ holds
ex b₃ being Element of b₁ st
( b₃ in b₂ & b₃ <= Top b₁ ) ) & uparrow (fininfs ((downarrow (Top b₁)) ` )) meets waybelow (Top b₁) )

proof end;

theorem Th42: :: WAYBEL_7:42

for b₁ being continuous LATTICE
for b₂ being Element of b₁ st uparrow (fininfs ((downarrow b₂) ` )) misses waybelow b₂ holds
for b₃ being non empty finite Subset of b₁ st inf b₃ << b₂ holds
ex b₄ being Element of b₁ st
( b₄ in b₃ & b₄ <= b₂ )

proof end;

theorem Th43: :: WAYBEL_7:43

for b₁ being distributive continuous LATTICE
for b₂ being Element of b₁ st uparrow (fininfs ((downarrow b₂) ` )) misses waybelow b₂ holds
b₂ is pseudoprime

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be Relation of the carrier of c₁;
attr a₂ is multiplicative means :Def7: :: WAYBEL_7:def 7
for b₁, b₂, b₃ being Element of a₁ st [b₁,b₂] in a₂ & [b₁,b₃] in a₂ holds
[b₁,(b₂ "/\" b₃)] in a₂;

end;

:: deftheorem Def7 defines multiplicative WAYBEL_7:def 7 :

registration

let c₁ be lower-bounded sup-Semilattice;
let c₂ be auxiliary Relation of c₁;
let c₃ be Element of c₁;
cluster a₂ -above a₃ -> upper ;
coherence

proof end;

end;

theorem Th44: :: WAYBEL_7:44

for b₁ being lower-bounded LATTICE
for b₂ being auxiliary Relation of b₁ holds
( b₂ is multiplicative iff for b₃ being Element of b₁ holds b₂ -above b₃ is filtered )

proof end;

theorem Th45: :: WAYBEL_7:45

for b₁ being lower-bounded LATTICE
for b₂ being auxiliary Relation of b₁ holds
( b₂ is multiplicative iff for b₃, b₄, b₅, b₆ being Element of b₁ st [b₃,b₅] in b₂ & [b₄,b₆] in b₂ holds
[(b₃ "/\" b₄),(b₅ "/\" b₆)] in b₂ )

proof end;

theorem Th46: :: WAYBEL_7:46

for b₁ being lower-bounded LATTICE
for b₂ being auxiliary Relation of b₁ holds
( b₂ is multiplicative iff for b₃ being full SubRelStr of [:b₁,b₁:] st the carrier of b₃ = b₂ holds
b₃ is meet-inheriting )

proof end;

theorem Th47: :: WAYBEL_7:47

for b₁ being lower-bounded LATTICE
for b₂ being auxiliary Relation of b₁ holds
( b₂ is multiplicative iff b₂ -below is meet-preserving )

proof end;

E36: now

let c₁ be lower-bounded continuous LATTICE;
let c₂ be Element of c₁;
assume that
E37: c₁ -waybelow is multiplicative and
E38: for b₁, b₂ being Element of c₁ holds
( not b₁ "/\" b₂ << c₂ or b₁ <= c₂ or b₂ <= c₂ ) and
E39: not c₂ is prime ;
consider c₃, c₄ being Element of c₁ such that
E40: ( c₃ "/\" c₄ <= c₂ & not c₃ <= c₂ & not c₄ <= c₂ ) by E39, WAYBEL_6:def 6;
E41: for b₁ being Element of c₁ holds
( not waybelow b₁ is empty & waybelow b₁ is directed ) ;
then consider c₅ being Element of c₁ such that
E42: ( c₅ << c₃ & not c₅ <= c₂ ) by E40, WAYBEL_3:24;
consider c₆ being Element of c₁ such that
E43: ( c₆ << c₄ & not c₆ <= c₂ ) by E40, E41, WAYBEL_3:24;
( [c₅,c₃] in c₁ -waybelow & [c₆,c₄] in c₁ -waybelow ) by E42, E43, WAYBEL_4:def 2;
then [(c₅ "/\" c₆),(c₃ "/\" c₄)] in c₁ -waybelow by E37, Th45;
then c₅ "/\" c₆ << c₃ "/\" c₄ by WAYBEL_4:def 2;
then c₅ "/\" c₆ << c₂ by E40, WAYBEL_3:2;
hence contradiction by E38, E42, E43;

end;

theorem Th48: :: WAYBEL_7:48

for b₁ being lower-bounded continuous LATTICE st b₁ -waybelow is multiplicative holds
for b₂ being Element of b₁ holds
( b₂ is pseudoprime iff for b₃, b₄ being Element of b₁ holds
( not b₃ "/\" b₄ << b₂ or b₃ <= b₂ or b₄ <= b₂ ) )

proof end;

theorem Th49: :: WAYBEL_7:49

for b₁ being lower-bounded continuous LATTICE st b₁ -waybelow is multiplicative holds
for b₂ being Element of b₁ st b₂ is pseudoprime holds
b₂ is prime

proof end;

theorem Th50: :: WAYBEL_7:50

for b₁ being lower-bounded distributive continuous LATTICE st ( for b₂ being Element of b₁ st b₂ is pseudoprime holds
b₂ is prime ) holds
b₁ -waybelow is multiplicative

proof end;