:: WAYBEL_6 semantic presentation

scheme :: WAYBEL_6:sch 1
s1{ F₁() -> non empty RelStr , F₂() -> Subset of F₁(), F₃() -> non empty Subset of F₁(), P₁[ set , set ] } :

ex b₁ being Function of F₂(),F₃() st
for b₂ being Element of F₁() st b₂ in F₂() holds
ex b₃ being Element of F₁() st
( b₃ in F₃() & b₃ = b₁ . b₂ & P₁[b₂,b₃] )

provided

E1: for b₁ being Element of F₁() st b₁ in F₂() holds
ex b₂ being Element of F₁() st
( b₂ in F₃() & P₁[b₁,b₂] )

proof end;

definition

let c₁ be LATTICE;
let c₂ be non empty Subset of c₁;
let c₃ be Function of c₂,c₂;
let c₄ be Element of NAT ;
redefine func iter as iter c₃,c₄ -> Function of a₂,a₂;
coherence by FUNCT_7:85;

end;

definition

let c₁ be LATTICE;
let c₂, c₃ be non empty Subset of c₁;
let c₄ be Function of c₂,c₃;
let c₅ be Element of c₂;
redefine func . as c₄ . c₅ -> Element of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty Poset;
cluster -> directed filtered Element of bool the carrier of a₁;
coherence

proof end;

end;

registration

cluster strict lower-bounded distributive continuous RelStr ;
existence

proof end;

end;

theorem Th1: :: WAYBEL_6:1

for b₁, b₂ being Semilattice
for b₃ being Function of b₁,b₂ holds
( b₃ is meet-preserving iff for b₄, b₅ being Element of b₁ holds b₃ . (b₄ "/\" b₅) = (b₃ . b₄) "/\" (b₃ . b₅) )

proof end;

theorem Th2: :: WAYBEL_6:2

for b₁, b₂ being sup-Semilattice
for b₃ being Function of b₁,b₂ holds
( b₃ is join-preserving iff for b₄, b₅ being Element of b₁ holds b₃ . (b₄ "\/" b₅) = (b₃ . b₄) "\/" (b₃ . b₅) )

proof end;

theorem Th3: :: WAYBEL_6:3

for b₁, b₂ being LATTICE
for b₃ being Function of b₁,b₂ st b₂ is distributive & b₃ is meet-preserving & b₃ is join-preserving & b₃ is one-to-one holds
b₁ is distributive

proof end;

registration

let c₁, c₂ be complete LATTICE;
cluster sups-preserving M4(the carrier of a₁,the carrier of a₂);
existence

proof end;

end;

Lemma4: for b₁, b₂ being non empty with_suprema Poset
for b₃ being Function of b₁,b₂ st b₃ is directed-sups-preserving holds
b₃ is monotone

proof end;

theorem Th4: :: WAYBEL_6:4

for b₁, b₂ being complete LATTICE
for b₃ being sups-preserving Function of b₁,b₂ st b₂ is meet-continuous & b₃ is meet-preserving & b₃ is one-to-one holds
b₁ is meet-continuous

proof end;

definition

let c₁ be non empty reflexive RelStr ;
let c₂ be Subset of c₁;
attr a₂ is Open means :Def1: :: WAYBEL_6:def 1
for b₁ being Element of a₁ st b₁ in a₂ holds
ex b₂ being Element of a₁ st
( b₂ in a₂ & b₂ << b₁ );

end;

:: deftheorem Def1 defines Open WAYBEL_6:def 1 :

theorem Th5: :: WAYBEL_6:5

for b₁ being up-complete LATTICE
for b₂ being upper Subset of b₁ holds
( b₂ is Open iff for b₃ being Element of b₁ st b₃ in b₂ holds
waybelow b₃ meets b₂ )

proof end;

theorem Th6: :: WAYBEL_6:6

for b₁ being up-complete LATTICE
for b₂ being upper Subset of b₁ holds
( b₂ is Open iff b₂ = union { (wayabove b₃) where B is Element of b₁ : b₃ in b₂ } )

proof end;

registration

let c₁ be lower-bounded up-complete LATTICE;
cluster Open Element of bool the carrier of a₁;
existence

proof end;

end;

theorem Th7: :: WAYBEL_6:7

for b₁ being lower-bounded continuous LATTICE
for b₂ being Element of b₁ holds wayabove b₂ is Open

proof end;

theorem Th8: :: WAYBEL_6:8

for b₁ being lower-bounded continuous LATTICE
for b₂, b₃ being Element of b₁ st b₂ << b₃ holds
ex b₄ being Open Filter of b₁ st
( b₃ in b₄ & b₄ c= wayabove b₂ )

proof end;

theorem Th9: :: WAYBEL_6:9

for b₁ being complete LATTICE
for b₂ being upper Open Subset of b₁
for b₃ being Element of b₁ st b₃ in b₂ ` holds
ex b₄ being Element of b₁ st
( b₃ <= b₄ & b₄ is_maximal_in b₂ ` )

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
attr a₂ is meet-irreducible means :Def2: :: WAYBEL_6:def 2
for b₁, b₂ being Element of a₁ holds
( not a₂ = b₁ "/\" b₂ or b₁ = a₂ or b₂ = a₂ );

end;

:: deftheorem Def2 defines meet-irreducible WAYBEL_6:def 2 :

notation

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
synonym irreducible c₂ for meet-irreducible c₂;

end;

definition

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
attr a₂ is join-irreducible means :: WAYBEL_6:def 3
for b₁, b₂ being Element of a₁ holds
( not a₂ = b₁ "\/" b₂ or b₁ = a₂ or b₂ = a₂ );

end;

:: deftheorem Def3 defines join-irreducible WAYBEL_6:def 3 :

definition

let c₁ be non empty RelStr ;
func IRR c₁ -> Subset of a₁ means :Def4: :: WAYBEL_6:def 4
for b₁ being Element of a₁ holds
( b₁ in a₂ iff b₁ is meet-irreducible );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines IRR WAYBEL_6:def 4 :

theorem Th10: :: WAYBEL_6:10

for b₁ being non empty antisymmetric upper-bounded with_infima RelStr holds Top b₁ is meet-irreducible

proof end;

registration

let c₁ be non empty antisymmetric upper-bounded with_infima RelStr ;
cluster irreducible Element of the carrier of a₁;
existence

proof end;

end;

theorem Th11: :: WAYBEL_6:11

for b₁ being Semilattice
for b₂ being Element of b₁ holds
( b₂ is meet-irreducible iff for b₃ being non empty finite Subset of b₁ st b₂ = inf b₃ holds
b₂ in b₃ )

proof end;

theorem Th12: :: WAYBEL_6:12

for b₁ being LATTICE
for b₂ being Element of b₁ st (uparrow b₂) \ {b₂} is Filter of b₁ holds
b₂ is meet-irreducible

proof end;

theorem Th13: :: WAYBEL_6:13

for b₁ being LATTICE
for b₂ being Element of b₁
for b₃ being Filter of b₁ st b₂ is_maximal_in b₃ ` holds
b₂ is meet-irreducible

proof end;

theorem Th14: :: WAYBEL_6:14

for b₁ being lower-bounded continuous LATTICE
for b₂, b₃ being Element of b₁ st not b₃ <= b₂ holds
ex b₄ being Element of b₁ st
( b₄ is meet-irreducible & b₂ <= b₄ & not b₃ <= b₄ )

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be Subset of c₁;
attr a₂ is order-generating means :Def5: :: WAYBEL_6:def 5
for b₁ being Element of a₁ holds
( ex_inf_of (uparrow b₁) /\ a₂,a₁ & b₁ = inf ((uparrow b₁) /\ a₂) );

end;

:: deftheorem Def5 defines order-generating WAYBEL_6:def 5 :

theorem Th15: :: WAYBEL_6:15

for b₁ being lower-bounded up-complete LATTICE
for b₂ being Subset of b₁ holds
( b₂ is order-generating iff for b₃ being Element of b₁ ex b₄ being Subset of b₂ st b₃ = "/\" b₄,b₁ )

proof end;

theorem Th16: :: WAYBEL_6:16

for b₁ being lower-bounded up-complete LATTICE
for b₂ being Subset of b₁ holds
( b₂ is order-generating iff for b₃ being Subset of b₁ st b₂ c= b₃ & ( for b₄ being Subset of b₃ holds "/\" b₄,b₁ in b₃ ) holds
the carrier of b₁ = b₃ )

proof end;

theorem Th17: :: WAYBEL_6:17

for b₁ being lower-bounded up-complete LATTICE
for b₂ being Subset of b₁ holds
( b₂ is order-generating iff for b₃, b₄ being Element of b₁ st not b₄ <= b₃ holds
ex b₅ being Element of b₁ st
( b₅ in b₂ & b₃ <= b₅ & not b₄ <= b₅ ) )

proof end;

theorem Th18: :: WAYBEL_6:18

for b₁ being lower-bounded continuous LATTICE
for b₂ being Subset of b₁ st b₂ = (IRR b₁) \ {(Top b₁)} holds
b₂ is order-generating

proof end;

theorem Th19: :: WAYBEL_6:19

for b₁ being lower-bounded continuous LATTICE
for b₂, b₃ being Subset of b₁ st b₂ is order-generating & b₂ c= b₃ holds
b₃ is order-generating

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
attr a₂ is prime means :Def6: :: WAYBEL_6:def 6
for b₁, b₂ being Element of a₁ holds
( not b₁ "/\" b₂ <= a₂ or b₁ <= a₂ or b₂ <= a₂ );

end;

:: deftheorem Def6 defines prime WAYBEL_6:def 6 :

definition

let c₁ be non empty RelStr ;
func PRIME c₁ -> Subset of a₁ means :Def7: :: WAYBEL_6:def 7
for b₁ being Element of a₁ holds
( b₁ in a₂ iff b₁ is prime );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines PRIME WAYBEL_6:def 7 :

definition

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
attr a₂ is co-prime means :Def8: :: WAYBEL_6:def 8
a₂ ~ is prime;

end;

:: deftheorem Def8 defines co-prime WAYBEL_6:def 8 :

theorem Th20: :: WAYBEL_6:20

for b₁ being non empty antisymmetric upper-bounded RelStr holds Top b₁ is prime

proof end;

theorem Th21: :: WAYBEL_6:21

for b₁ being non empty antisymmetric lower-bounded RelStr holds Bottom b₁ is co-prime

proof end;

registration

let c₁ be non empty antisymmetric upper-bounded RelStr ;
cluster prime Element of the carrier of a₁;
existence

proof end;

end;

theorem Th22: :: WAYBEL_6:22

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

proof end;

theorem Th23: :: WAYBEL_6:23

for b₁ being sup-Semilattice
for b₂ being Element of b₁ holds
( b₂ is co-prime iff for b₃ being non empty finite Subset of b₁ st b₂ <= sup b₃ holds
ex b₄ being Element of b₁ st
( b₄ in b₃ & b₂ <= b₄ ) )

proof end;

theorem Th24: :: WAYBEL_6:24

for b₁ being LATTICE
for b₂ being Element of b₁ st b₂ is prime holds
b₂ is meet-irreducible

proof end;

theorem Th25: :: WAYBEL_6:25

for b₁ being LATTICE
for b₂ being Element of b₁ holds
( b₂ is prime iff for b₃ being set
for b₄ being Function of b₁,(BoolePoset {b₃}) st ( for b₅ being Element of b₁ holds
( b₄ . b₅ = {} iff b₅ <= b₂ ) ) holds
( b₄ is meet-preserving & b₄ is join-preserving ) )

proof end;

theorem Th26: :: WAYBEL_6:26

for b₁ being upper-bounded LATTICE
for b₂ being Element of b₁ st b₂ <> Top b₁ holds
( b₂ is prime iff (downarrow b₂) ` is Filter of b₁ )

proof end;

theorem Th27: :: WAYBEL_6:27

for b₁ being distributive LATTICE
for b₂ being Element of b₁ holds
( b₂ is prime iff b₂ is meet-irreducible )

proof end;

theorem Th28: :: WAYBEL_6:28

for b₁ being distributive LATTICE holds PRIME b₁ = IRR b₁

proof end;

theorem Th29: :: WAYBEL_6:29

for b₁ being Boolean LATTICE
for b₂ being Element of b₁ st b₂ <> Top b₁ holds
( b₂ is prime iff for b₃ being Element of b₁ st b₃ > b₂ holds
b₃ = Top b₁ )

proof end;

theorem Th30: :: WAYBEL_6:30

for b₁ being lower-bounded distributive continuous LATTICE
for b₂ being Element of b₁ st b₂ <> Top b₁ holds
( b₂ is prime iff ex b₃ being Open Filter of b₁ st b₂ is_maximal_in b₃ ` )

proof end;

theorem Th31: :: WAYBEL_6:31

for b₁ being RelStr
for b₂ being Subset of b₁ holds chi b₂,the carrier of b₁ is Function of b₁,(BoolePoset {{} })

proof end;

theorem Th32: :: WAYBEL_6:32

for b₁ being non empty RelStr
for b₂, b₃ being Element of b₁ holds
( (chi ((downarrow b₂) ` ),the carrier of b₁) . b₃ = {} iff b₃ <= b₂ )

proof end;

theorem Th33: :: WAYBEL_6:33

for b₁ being upper-bounded LATTICE
for b₂ being Function of b₁,(BoolePoset {{} })
for b₃ being prime Element of b₁ st chi ((downarrow b₃) ` ),the carrier of b₁ = b₂ holds
( b₂ is meet-preserving & b₂ is join-preserving )

proof end;

theorem Th34: :: WAYBEL_6:34

for b₁ being complete LATTICE st PRIME b₁ is order-generating holds
( b₁ is distributive & b₁ is meet-continuous )

proof end;

theorem Th35: :: WAYBEL_6:35

for b₁ being lower-bounded continuous LATTICE holds
( b₁ is distributive iff PRIME b₁ is order-generating )

proof end;

theorem Th36: :: WAYBEL_6:36

for b₁ being lower-bounded continuous LATTICE holds
( b₁ is distributive iff b₁ is Heyting )

proof end;

theorem Th37: :: WAYBEL_6:37

for b₁ being complete continuous LATTICE st ( for b₂ being Element of b₁ ex b₃ being Subset of b₁ st
( b₂ = sup b₃ & ( for b₄ being Element of b₁ st b₄ in b₃ holds
b₄ is co-prime ) ) ) holds
for b₂ being Element of b₁ holds b₂ = "\/" ((waybelow b₂) /\ (PRIME (b₁ opp ))),b₁

proof end;

Lemma36: for b₁ being complete continuous LATTICE st ( for b₂ being Element of b₁ ex b₃ being Subset of b₁ st
( b₂ = sup b₃ & ( for b₄ being Element of b₁ st b₄ in b₃ holds
b₄ is co-prime ) ) ) holds
b₁ is completely-distributive

proof end;

Lemma37: for b₁ being completely-distributive complete LATTICE holds
( b₁ is distributive & b₁ is continuous & b₁ ~ is continuous )

proof end;

Lemma38: for b₁ being complete LATTICE st b₁ is distributive & b₁ is continuous & b₁ ~ is continuous holds
for b₂ being Element of b₁ ex b₃ being Subset of b₁ st
( b₂ = sup b₃ & ( for b₄ being Element of b₁ st b₄ in b₃ holds
b₄ is co-prime ) )

proof end;

theorem Th38: :: WAYBEL_6:38

for b₁ being complete LATTICE holds
( b₁ is completely-distributive iff ( b₁ is continuous & ( for b₂ being Element of b₁ ex b₃ being Subset of b₁ st
( b₂ = sup b₃ & ( for b₄ being Element of b₁ st b₄ in b₃ holds
b₄ is co-prime ) ) ) ) )

proof end;

theorem Th39: :: WAYBEL_6:39

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

proof end;