:: WAYBEL_8 semantic presentation

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines CompactSublatt WAYBEL_8:def 1 :

registration

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

proof end;

end;

theorem Th1: :: WAYBEL_8:1

for b₁ being complete LATTICE
for b₂, b₃, b₄ being Element of b₁ st b₂ <= b₄ & b₄ <= b₃ & b₄ in the carrier of (CompactSublatt b₁) holds
b₂ << b₃

proof end;

theorem Th2: :: WAYBEL_8:2

for b₁ being complete LATTICE
for b₂ being Element of b₁ holds
( uparrow b₂ is Open Filter of b₁ iff b₂ is compact )

proof end;

theorem Th3: :: WAYBEL_8:3

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

proof end;

definition

let c₁ be non empty reflexive RelStr ;
let c₂ be Element of c₁;
func compactbelow c₂ -> Subset of a₁ equals :: WAYBEL_8:def 2
{ b₁ where B is Element of a₁ : ( a₂ >= b₁ & b₁ is compact ) } ;
coherence

proof end;

end;

:: deftheorem Def2 defines compactbelow WAYBEL_8:def 2 :

theorem Th4: :: WAYBEL_8:4

for b₁ being non empty reflexive RelStr
for b₂, b₃ being Element of b₁ holds
( b₃ in compactbelow b₂ iff ( b₂ >= b₃ & b₃ is compact ) )

proof end;

theorem Th5: :: WAYBEL_8:5

for b₁ being non empty reflexive RelStr
for b₂ being Element of b₁ holds compactbelow b₂ = (downarrow b₂) /\ the carrier of (CompactSublatt b₁)

proof end;

theorem Th6: :: WAYBEL_8:6

for b₁ being non empty reflexive transitive RelStr
for b₂ being Element of b₁ holds compactbelow b₂ c= waybelow b₂

proof end;

registration

let c₁ be non empty reflexive antisymmetric lower-bounded RelStr ;
let c₂ be Element of c₁;
cluster compactbelow a₂ -> non empty ;
coherence

proof end;

end;

definition

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

end;

:: deftheorem Def3 defines satisfying_axiom_K WAYBEL_8:def 3 :

definition

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

end;

:: deftheorem Def4 defines algebraic WAYBEL_8:def 4 :

theorem Th7: :: WAYBEL_8:7

for b₁ being LATTICE holds
( b₁ is algebraic iff ( b₁ is continuous & ( for b₂, b₃ being Element of b₁ st b₂ << b₃ holds
ex b₄ being Element of b₁ st
( b₄ in the carrier of (CompactSublatt b₁) & b₂ <= b₄ & b₄ <= b₃ ) ) ) )

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 c₁ be non empty with_suprema Poset;
cluster CompactSublatt a₁ -> strict full join-inheriting ;
coherence

proof end;

end;

definition

let c₁ be non empty reflexive RelStr ;
attr a₁ is arithmetic means :Def5: :: WAYBEL_8:def 5
( a₁ is algebraic & CompactSublatt a₁ 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 b₁, b₂ being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₁ is up-complete holds
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ st b₃ = b₅ & b₄ = b₆ & b₃ << b₄ holds
b₅ << b₆

proof end;

theorem Th9: :: WAYBEL_8:9

for b₁, b₂ being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₁ is up-complete holds
for b₃ being Element of b₁
for b₄ being Element of b₂ st b₃ = b₄ & b₃ is compact holds
b₄ is compact

proof end;

theorem Th10: :: WAYBEL_8:10

for b₁, b₂ being non empty reflexive antisymmetric up-complete RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₃ being Element of b₁
for b₄ being Element of b₂ st b₃ = b₄ holds
compactbelow b₃ = compactbelow b₄

proof end;

theorem Th11: :: WAYBEL_8:11

for b₁, b₂ being RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & not b₁ is empty holds
not b₂ is empty

proof end;

theorem Th12: :: WAYBEL_8:12

for b₁, b₂ being non empty RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₁ is reflexive holds
b₂ is reflexive

proof end;

theorem Th13: :: WAYBEL_8:13

for b₁, b₂ being RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₁ is transitive holds
b₂ is transitive

proof end;

theorem Th14: :: WAYBEL_8:14

for b₁, b₂ being RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₁ is antisymmetric holds
b₂ is antisymmetric

proof end;

theorem Th15: :: WAYBEL_8:15

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

proof end;

theorem Th16: :: WAYBEL_8:16

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

proof end;

theorem Th17: :: WAYBEL_8:17

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

proof end;

theorem Th18: :: WAYBEL_8:18

for b₁, b₂ being LATTICE st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₁ is arithmetic holds
b₂ is arithmetic

proof end;

registration

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

end;

registration

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

end;

registration

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

end;

registration

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

end;

registration

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

end;

registration

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

end;

registration

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

end;

registration

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

end;

registration

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

end;

theorem Th19: :: WAYBEL_8:19

canceled;

theorem Th20: :: WAYBEL_8:20

canceled;

theorem Th21: :: WAYBEL_8:21

for b₁ being algebraic LATTICE holds
( b₁ is arithmetic iff CompactSublatt b₁ is LATTICE )

proof end;

theorem Th22: :: WAYBEL_8:22

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

proof end;

theorem Th23: :: WAYBEL_8:23

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

proof end;

theorem Th24: :: WAYBEL_8:24

for b₁ being lower-bounded distributive algebraic LATTICE st ( for b₂ being Element of b₁ st b₂ is pseudoprime holds
b₂ is prime ) holds
b₁ is arithmetic

proof end;

registration

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

proof end;

end;

theorem Th25: :: WAYBEL_8:25

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

proof end;

theorem Th26: :: WAYBEL_8:26

for b₁ being lower-bounded algebraic LATTICE
for b₂ being closure Function of b₁,b₁ st b₂ is directed-sups-preserving holds
Image b₂ is algebraic LATTICE

proof end;

theorem Th27: :: WAYBEL_8:27

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

proof end;

theorem Th28: :: WAYBEL_8:28

for b₁, b₂ being set holds
( b₂ is Element of (BoolePoset b₁) iff b₂ c= b₁ )

proof end;

theorem Th29: :: WAYBEL_8:29

for b₁ being set
for b₂, b₃ being Element of (BoolePoset b₁) holds
( b₂ << b₃ iff for b₄ being Subset-Family of b₁ st b₃ c= union b₄ holds
ex b₅ being finite Subset of b₄ st b₂ c= union b₅ )

proof end;

theorem Th30: :: WAYBEL_8:30

for b₁ being set
for b₂ being Element of (BoolePoset b₁) holds
( b₂ is finite iff b₂ is compact )

proof end;

theorem Th31: :: WAYBEL_8:31

for b₁ being set
for b₂ being Element of (BoolePoset b₁) holds compactbelow b₂ = { b₃ where B is finite Subset of b₂ : verum }

proof end;

theorem Th32: :: WAYBEL_8:32

for b₁ being set
for b₂ being Subset of b₁ holds
( b₂ in the carrier of (CompactSublatt (BoolePoset b₁)) iff b₂ is finite )

proof end;

registration

let c₁ be set ;
let c₂ be Element of (BoolePoset c₁);
cluster compactbelow a₂ -> non empty directed lower ;
coherence

proof end;

end;

theorem Th33: :: WAYBEL_8:33

for b₁ being set holds BoolePoset b₁ is algebraic

proof end;

registration

let c₁ be set ;
cluster BoolePoset a₁ -> continuous satisfying_axiom_K algebraic ;
coherence by Th33;

end;