:: WAYBEL15 semantic presentation

theorem Th1: :: WAYBEL15:1

for b₁ being RelStr
for b₂ being full SubRelStr of b₁
for b₃ being full SubRelStr of b₂ holds b₃ is full SubRelStr of b₁

proof end;

theorem Th2: :: WAYBEL15:2

for b₁ being 1-sorted
for b₂, b₃ being non empty 1-sorted
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st b₄ is onto & b₅ is onto holds
b₅ * b₄ is onto

proof end;

theorem Th3: :: WAYBEL15:3

for b₁ being 1-sorted
for b₂ being Subset of b₁ holds (id b₁) .: b₂ = b₂

proof end;

theorem Th4: :: WAYBEL15:4

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

proof end;

theorem Th5: :: WAYBEL15:5

for b₁ being non empty antisymmetric upper-bounded RelStr
for b₂ being Element of b₁ st Top b₁ <= b₂ holds
b₂ = Top b₁

proof end;

theorem Th6: :: WAYBEL15:6

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st b₃ is onto & [b₃,b₄] is Galois holds
b₂, Image b₄ are_isomorphic

proof end;

theorem Th7: :: WAYBEL15:7

for b₁, b₂, b₃ being non empty Poset
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃
for b₆ being Function of b₂,b₁
for b₇ being Function of b₃,b₂ st [b₄,b₆] is Galois & [b₅,b₇] is Galois holds
[(b₅ * b₄),(b₆ * b₇)] is Galois

proof end;

theorem Th8: :: WAYBEL15:8

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st b₄ = b₃ " & b₃ is isomorphic holds
( [b₃,b₄] is Galois & [b₄,b₃] is Galois )

proof end;

theorem Th9: :: WAYBEL15:9

for b₁ being set holds BoolePoset b₁ is arithmetic

proof end;

registration

let c₁ be set ;
cluster BoolePoset a₁ -> arithmetic ;
coherence by Th9;

end;

Lemma8: for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂ st b₃ is sups-preserving holds
b₃ is directed-sups-preserving

proof end;

theorem Th10: :: WAYBEL15:10

for b₁, b₂ being non empty up-complete Poset
for b₃ being Function of b₁,b₂ st b₃ is isomorphic holds
for b₄ being Element of b₁ holds b₃ .: (waybelow b₄) = waybelow (b₃ . b₄)

proof end;

theorem Th11: :: WAYBEL15:11

for b₁, b₂ being non empty Poset st b₁,b₂ are_isomorphic & b₁ is continuous holds
b₂ is continuous

proof end;

theorem Th12: :: WAYBEL15:12

for b₁, b₂ being LATTICE st b₁,b₂ are_isomorphic & b₁ is lower-bounded & b₁ is arithmetic holds
b₂ is arithmetic

proof end;

Lemma12: for b₁ being lower-bounded LATTICE st b₁ is continuous holds
ex b₂ being lower-bounded arithmetic LATTICEex b₃ being Function of b₂,b₁ st
( b₃ is onto & b₃ is infs-preserving & b₃ is directed-sups-preserving )

proof end;

theorem Th13: :: WAYBEL15:13

for b₁, b₂, b₃ being non empty Poset
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st b₄ is directed-sups-preserving & b₅ is directed-sups-preserving holds
b₅ * b₄ is directed-sups-preserving

proof end;

theorem Th14: :: WAYBEL15:14

for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂
for b₄ being Subset of (Image b₃) holds (inclusion b₃) .: b₄ = b₄

proof end;

theorem Th15: :: WAYBEL15:15

for b₁ being set
for b₂ being Function of (BoolePoset b₁),(BoolePoset b₁) st b₂ is idempotent & b₂ is directed-sups-preserving holds
inclusion b₂ is directed-sups-preserving

proof end;

Lemma16: for b₁ being lower-bounded LATTICE st ex b₂ being lower-bounded algebraic LATTICEex b₃ being Function of b₂,b₁ st
( b₃ is onto & b₃ is infs-preserving & b₃ is directed-sups-preserving ) holds
ex b₂ being non empty set ex b₃ being projection Function of (BoolePoset b₂),(BoolePoset b₂) st
( b₃ is directed-sups-preserving & b₁, Image b₃ are_isomorphic )

proof end;

theorem Th16: :: WAYBEL15:16

for b₁ being complete continuous LATTICE
for b₂ being kernel Function of b₁,b₁ st b₂ is directed-sups-preserving holds
Image b₂ is continuous LATTICE

proof end;

theorem Th17: :: WAYBEL15:17

for b₁ being complete continuous LATTICE
for b₂ being projection Function of b₁,b₁ st b₂ is directed-sups-preserving holds
Image b₂ is continuous LATTICE

proof end;

Lemma19: for b₁ being LATTICE st ex b₂ being set ex b₃ being projection Function of (BoolePoset b₂),(BoolePoset b₂) st
( b₃ is directed-sups-preserving & b₁, Image b₃ are_isomorphic ) holds
b₁ is continuous

proof end;

theorem Th18: :: WAYBEL15:18

for b₁ being lower-bounded LATTICE holds
( b₁ is continuous iff ex b₂ being lower-bounded arithmetic LATTICEex b₃ being Function of b₂,b₁ st
( b₃ is onto & b₃ is infs-preserving & b₃ is directed-sups-preserving ) )

proof end;

theorem Th19: :: WAYBEL15:19

for b₁ being lower-bounded LATTICE holds
( b₁ is continuous iff ex b₂ being lower-bounded algebraic LATTICEex b₃ being Function of b₂,b₁ st
( b₃ is onto & b₃ is infs-preserving & b₃ is directed-sups-preserving ) )

proof end;

theorem Th20: :: WAYBEL15:20

for b₁ being lower-bounded LATTICE holds
( ( b₁ is continuous implies ex b₂ being non empty set ex b₃ being projection Function of (BoolePoset b₂),(BoolePoset b₂) st
( b₃ is directed-sups-preserving & b₁, Image b₃ are_isomorphic ) ) & ( ex b₂ being set ex b₃ being projection Function of (BoolePoset b₂),(BoolePoset b₂) st
( b₃ is directed-sups-preserving & b₁, Image b₃ are_isomorphic ) implies b₁ is continuous ) )

proof end;

theorem Th21: :: WAYBEL15:21

for b₁ being non empty RelStr
for b₂ being Element of b₁ holds
( b₂ in PRIME (b₁ opp ) iff b₂ is co-prime )

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
attr a₂ is atom means :Def1: :: WAYBEL15:def 1
( Bottom a₁ < a₂ & ( for b₁ being Element of a₁ st Bottom a₁ < b₁ & b₁ <= a₂ holds
b₁ = a₂ ) );

end;

:: deftheorem Def1 defines atom WAYBEL15:def 1 :

definition

let c₁ be non empty RelStr ;
func ATOM c₁ -> Subset of a₁ means :Def2: :: WAYBEL15:def 2
for b₁ being Element of a₁ holds
( b₁ in a₂ iff b₁ is atom );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines ATOM WAYBEL15:def 2 :

theorem Th22: :: WAYBEL15:22

canceled;

theorem Th23: :: WAYBEL15:23

for b₁ being Boolean LATTICE
for b₂ being Element of b₁ holds
( b₂ is atom iff ( b₂ is co-prime & b₂ <> Bottom b₁ ) )

proof end;

registration

let c₁ be Boolean LATTICE;
cluster atom -> co-prime Element of the carrier of a₁;
coherence by Th23;

end;

theorem Th24: :: WAYBEL15:24

for b₁ being Boolean LATTICE holds ATOM b₁ = (PRIME (b₁ opp )) \ {(Bottom b₁)}

proof end;

theorem Th25: :: WAYBEL15:25

for b₁ being Boolean LATTICE
for b₂, b₃ being Element of b₁ st b₃ is atom holds
( b₃ <= b₂ iff not b₃ <= 'not' b₂ )

proof end;

theorem Th26: :: WAYBEL15:26

for b₁ being complete Boolean LATTICE
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds b₃ "/\" (sup b₂) = "\/" { (b₃ "/\" b₄) where B is Element of b₁ : b₄ in b₂ } ,b₁

proof end;

theorem Th27: :: WAYBEL15:27

for b₁ being non empty antisymmetric with_infima lower-bounded RelStr
for b₂, b₃ being Element of b₁ st b₂ is atom & b₃ is atom & b₂ <> b₃ holds
b₂ "/\" b₃ = Bottom b₁

proof end;

theorem Th28: :: WAYBEL15:28

for b₁ being complete Boolean LATTICE
for b₂ being Element of b₁
for b₃ being Subset of b₁ st b₃ c= ATOM b₁ holds
( b₂ in b₃ iff ( b₂ is atom & b₂ <= sup b₃ ) )

proof end;

theorem Th29: :: WAYBEL15:29

for b₁ being complete Boolean LATTICE
for b₂, b₃ being Subset of b₁ st b₂ c= ATOM b₁ & b₃ c= ATOM b₁ holds
( b₂ c= b₃ iff sup b₂ <= sup b₃ )

proof end;

Lemma27: for b₁ being Boolean LATTICE st ex b₂ being set st b₁, BoolePoset b₂ are_isomorphic holds
b₁ is arithmetic

proof end;

Lemma28: for b₁ being Boolean LATTICE st b₁ is continuous holds
b₁ opp is continuous

proof end;

Lemma29: for b₁ being Boolean LATTICE holds
( ( b₁ is continuous & b₁ opp is continuous ) iff b₁ is completely-distributive )

proof end;

Lemma30: for b₁ being Boolean LATTICE st b₁ is completely-distributive holds
( b₁ is complete & ( for b₂ being Element of b₁ ex b₃ being Subset of b₁ st
( b₃ c= ATOM b₁ & b₂ = sup b₃ ) ) )

proof end;

Lemma31: for b₁ being Boolean LATTICE st b₁ is complete & ( for b₂ being Element of b₁ ex b₃ being Subset of b₁ st
( b₃ c= ATOM b₁ & b₂ = sup b₃ ) ) holds
ex b₂ being set st b₁, BoolePoset b₂ are_isomorphic

proof end;

theorem Th30: :: WAYBEL15:30

for b₁ being Boolean LATTICE holds
( b₁ is arithmetic iff ex b₂ being set st b₁, BoolePoset b₂ are_isomorphic )

proof end;

theorem Th31: :: WAYBEL15:31

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

proof end;

theorem Th32: :: WAYBEL15:32

for b₁ being Boolean LATTICE holds
( b₁ is arithmetic iff b₁ is continuous )

proof end;

theorem Th33: :: WAYBEL15:33

for b₁ being Boolean LATTICE holds
( b₁ is arithmetic iff ( b₁ is continuous & b₁ opp is continuous ) )

proof end;

theorem Th34: :: WAYBEL15:34

for b₁ being Boolean LATTICE holds
( b₁ is arithmetic iff b₁ is completely-distributive )

proof end;

theorem Th35: :: WAYBEL15:35

for b₁ being Boolean LATTICE holds
( b₁ is arithmetic iff ( b₁ is complete & ( for b₂ being Element of b₁ ex b₃ being Subset of b₁ st
( b₃ c= ATOM b₁ & b₂ = sup b₃ ) ) ) )

proof end;