:: WAYBEL_8 semantic presentation

definition

let L be non empty reflexive RelStr ;
func CompactSublatt L -> strict full SubRelStr of L means :Def1: :: WAYBEL_8:def 1
for x being Element of L holds
( x in the carrier of it iff x is compact );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines CompactSublatt WAYBEL_8:def 1 :

registration

let L be non empty reflexive antisymmetric lower-bounded RelStr ;
cluster CompactSublatt L -> non empty strict full ;
coherence

proof end;

end;

theorem :: WAYBEL_8:1

for L being complete LATTICE
for x, y, k being Element of L st x <= k & k <= y & k in the carrier of (CompactSublatt L) holds
x << y

proof end;

theorem :: WAYBEL_8:2

for L being complete LATTICE
for x being Element of L holds
( uparrow x is Open Filter of L iff x is compact )

proof end;

theorem :: WAYBEL_8:3

for L being non empty with_suprema lower-bounded Poset holds
( CompactSublatt L is join-inheriting & Bottom L in the carrier of (CompactSublatt L) )

proof end;

definition

let L be non empty reflexive RelStr ;
let x be Element of L;
func compactbelow x -> Subset of L equals :: WAYBEL_8:def 2
{ y where y is Element of L : ( x >= y & y is compact ) } ;
coherence

proof end;

end;

:: deftheorem defines compactbelow WAYBEL_8:def 2 :

theorem Th4: :: WAYBEL_8:4

for L being non empty reflexive RelStr
for x, y being Element of L holds
( y in compactbelow x iff ( x >= y & y is compact ) )

proof end;

theorem Th5: :: WAYBEL_8:5

for L being non empty reflexive RelStr
for x being Element of L holds compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L)

proof end;

theorem Th6: :: WAYBEL_8:6

for L being non empty reflexive transitive RelStr
for x being Element of L holds compactbelow x c= waybelow x

proof end;

registration

let L be non empty reflexive antisymmetric lower-bounded RelStr ;
let x be Element of L;
cluster compactbelow x -> non empty ;
coherence

proof end;

end;

definition

let L be non empty reflexive RelStr ;
attr L is satisfying_axiom_K means :Def3: :: WAYBEL_8:def 3
for x being Element of L holds x = sup (compactbelow x);

end;

:: deftheorem Def3 defines satisfying_axiom_K WAYBEL_8:def 3 :

definition

let L be non empty reflexive RelStr ;
attr L is algebraic means :Def4: :: WAYBEL_8:def 4
( ( for x being Element of L holds
( not compactbelow x is empty & compactbelow x is directed ) ) & L is up-complete & L is satisfying_axiom_K );

end;

:: deftheorem Def4 defines algebraic WAYBEL_8:def 4 :

theorem Th7: :: WAYBEL_8:7

for L being LATTICE holds
( L is algebraic iff ( L is continuous & ( for x, y being Element of L st x << y holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) ) )

proof end;

registration

cluster algebraic -> continuous RelStr ;
coherence by Th7;

end;

registration

cluster non empty reflexive algebraic -> non empty reflexive up-complete satisfying_axiom_K RelStr ;
coherence by Def4;

end;

registration

let L be non empty with_suprema Poset;
cluster CompactSublatt L -> strict full join-inheriting ;
coherence

proof end;

end;

definition

let L be non empty reflexive RelStr ;
attr L is arithmetic means :Def5: :: WAYBEL_8:def 5
( L is algebraic & CompactSublatt L is meet-inheriting );

end;

:: deftheorem Def5 defines arithmetic WAYBEL_8:def 5 :

registration

cluster arithmetic -> continuous satisfying_axiom_K algebraic RelStr ;
coherence by Def5;

end;

registration

cluster trivial -> continuous satisfying_axiom_K algebraic arithmetic RelStr ;
coherence

proof end;

end;

registration

cluster strict continuous trivial satisfying_axiom_K algebraic arithmetic RelStr ;
existence

proof end;

end;

theorem Th8: :: WAYBEL_8:8

for L1, L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & L1 is up-complete holds
for x1, y1 being Element of L1
for x2, y2 being Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds
x2 << y2

proof end;

theorem Th9: :: WAYBEL_8:9

for L1, L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & L1 is up-complete holds
for x being Element of L1
for y being Element of L2 st x = y & x is compact holds
y is compact

proof end;

theorem Th10: :: WAYBEL_8:10

for L1, L2 being non empty reflexive antisymmetric up-complete RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) holds
for x being Element of L1
for y being Element of L2 st x = y holds
compactbelow x = compactbelow y

proof end;

theorem Th11: :: WAYBEL_8:11

for L1, L2 being RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & not L1 is empty holds
not L2 is empty

proof end;

theorem Th12: :: WAYBEL_8:12

for L1, L2 being non empty RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & L1 is reflexive holds
L2 is reflexive

proof end;

theorem Th13: :: WAYBEL_8:13

for L1, L2 being RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & L1 is transitive holds
L2 is transitive

proof end;

theorem Th14: :: WAYBEL_8:14

for L1, L2 being RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & L1 is antisymmetric holds
L2 is antisymmetric

proof end;

theorem Th15: :: WAYBEL_8:15

for L1, L2 being non empty reflexive RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & L1 is up-complete holds
L2 is up-complete

proof end;

theorem Th16: :: WAYBEL_8:16

for L1, L2 being non empty reflexive antisymmetric up-complete RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & L1 is satisfying_axiom_K & ( for x being Element of L1 holds
( not compactbelow x is empty & compactbelow x is directed ) ) holds
L2 is satisfying_axiom_K

proof end;

theorem Th17: :: WAYBEL_8:17

for L1, L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & L1 is algebraic holds
L2 is algebraic

proof end;

theorem Th18: :: WAYBEL_8:18

for L1, L2 being LATTICE st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & L1 is arithmetic holds
L2 is arithmetic

proof end;

registration

let L be non empty RelStr ;
cluster RelStr(# the carrier of L,the InternalRel of L #) -> non empty ;
coherence by Th11;

end;

registration

let L be non empty reflexive RelStr ;
cluster RelStr(# the carrier of L,the InternalRel of L #) -> non empty reflexive ;
coherence by Th12;

end;

registration

let L be transitive RelStr ;
cluster RelStr(# the carrier of L,the InternalRel of L #) -> transitive ;
coherence by Th13;

end;

registration

let L be antisymmetric RelStr ;
cluster RelStr(# the carrier of L,the InternalRel of L #) -> antisymmetric ;
coherence by Th14;

end;

registration

let L be with_infima RelStr ;
cluster RelStr(# the carrier of L,the InternalRel of L #) -> non empty with_infima ;
coherence by YELLOW_7:14;

end;

registration

let L be with_suprema RelStr ;
cluster RelStr(# the carrier of L,the InternalRel of L #) -> non empty with_suprema ;
coherence by YELLOW_7:15;

end;

registration

let L be non empty reflexive up-complete RelStr ;
cluster RelStr(# the carrier of L,the InternalRel of L #) -> non empty reflexive up-complete ;
coherence by Th15;

end;

registration

let L be non empty reflexive antisymmetric algebraic RelStr ;
cluster RelStr(# the carrier of L,the InternalRel of L #) -> non empty reflexive antisymmetric up-complete satisfying_axiom_K algebraic ;
coherence by Th17;

end;

registration

let L be arithmetic LATTICE;
cluster RelStr(# the carrier of L,the InternalRel of L #) -> non empty reflexive transitive antisymmetric with_suprema with_infima up-complete continuous satisfying_axiom_K algebraic arithmetic ;
coherence by Th18;

end;

theorem :: WAYBEL_8:19

canceled;

theorem :: WAYBEL_8:20

canceled;

theorem :: WAYBEL_8:21

for L being algebraic LATTICE holds
( L is arithmetic iff CompactSublatt L is LATTICE )

proof end;

theorem Th22: :: WAYBEL_8:22

for L being lower-bounded algebraic LATTICE holds
( L is arithmetic iff L -waybelow is multiplicative )

proof end;

theorem :: WAYBEL_8:23

for L being lower-bounded arithmetic LATTICE
for p being Element of L st p is pseudoprime holds
p is prime

proof end;

theorem :: WAYBEL_8:24

for L being lower-bounded distributive algebraic LATTICE st ( for p being Element of L st p is pseudoprime holds
p is prime ) holds
L is arithmetic

proof end;

registration

let L be algebraic LATTICE;
let c be closure Function of L,L;
cluster non empty directed Element of bool the carrier of (Image c);
existence

proof end;

end;

theorem Th25: :: WAYBEL_8:25

for L being algebraic LATTICE
for c being closure Function of L,L st c is directed-sups-preserving holds
c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c))

proof end;

theorem :: WAYBEL_8:26

for L being lower-bounded algebraic LATTICE
for c being closure Function of L,L st c is directed-sups-preserving holds
Image c is algebraic LATTICE

proof end;

theorem :: WAYBEL_8:27

for L being lower-bounded algebraic LATTICE
for c being closure Function of L,L st c is directed-sups-preserving holds
c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c))

proof end;

theorem Th28: :: WAYBEL_8:28

for X, x being set holds
( x is Element of (BoolePoset X) iff x c= X )

proof end;

theorem Th29: :: WAYBEL_8:29

for X being set
for x, y being Element of (BoolePoset X) holds
( x << y iff for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z )

proof end;

theorem Th30: :: WAYBEL_8:30

for X being set
for x being Element of (BoolePoset X) holds
( x is finite iff x is compact )

proof end;

theorem Th31: :: WAYBEL_8:31

for X being set
for x being Element of (BoolePoset X) holds compactbelow x = { y where y is finite Subset of x : verum }

proof end;

theorem :: WAYBEL_8:32

for X being set
for F being Subset of X holds
( F in the carrier of (CompactSublatt (BoolePoset X)) iff F is finite )

proof end;

registration

let X be set ;
let x be Element of (BoolePoset X);
cluster compactbelow x -> non empty directed lower ;
coherence

proof end;

end;

theorem Th33: :: WAYBEL_8:33

for X being set holds BoolePoset X is algebraic

proof end;

registration

let X be set ;
cluster BoolePoset X -> continuous satisfying_axiom_K algebraic ;
coherence by Th33;

end;