:: WAYBEL16 semantic presentation

theorem Th1: :: WAYBEL16:1

for b₁ being sup-Semilattice
for b₂, b₃ being Element of b₁ holds "/\" ((uparrow b₂) /\ (uparrow b₃)),b₁ = b₂ "\/" b₃

proof end;

theorem Th2: :: WAYBEL16:2

for b₁ being Semilattice
for b₂, b₃ being Element of b₁ holds "\/" ((downarrow b₂) /\ (downarrow b₃)),b₁ = b₂ "/\" b₃

proof end;

theorem Th3: :: WAYBEL16:3

for b₁ being non empty RelStr
for b₂, b₃ being Element of b₁ st b₂ is_maximal_in the carrier of b₁ \ (uparrow b₃) holds
(uparrow b₂) \ {b₂} = (uparrow b₂) /\ (uparrow b₃)

proof end;

theorem Th4: :: WAYBEL16:4

for b₁ being non empty RelStr
for b₂, b₃ being Element of b₁ st b₂ is_minimal_in the carrier of b₁ \ (downarrow b₃) holds
(downarrow b₂) \ {b₂} = (downarrow b₂) /\ (downarrow b₃)

proof end;

theorem Th5: :: WAYBEL16:5

for b₁ being with_suprema Poset
for b₂, b₃ being Subset of b₁
for b₄, b₅ being Subset of (b₁ opp ) st b₂ = b₄ & b₃ = b₅ holds
b₂ "\/" b₃ = b₄ "/\" b₅

proof end;

theorem Th6: :: WAYBEL16:6

for b₁ being with_infima Poset
for b₂, b₃ being Subset of b₁
for b₄, b₅ being Subset of (b₁ opp ) st b₂ = b₄ & b₃ = b₅ holds
b₂ "/\" b₃ = b₄ "\/" b₅

proof end;

theorem Th7: :: WAYBEL16:7

for b₁ being non empty reflexive transitive RelStr holds Filt b₁ = Ids (b₁ opp )

proof end;

theorem Th8: :: WAYBEL16:8

for b₁ being non empty reflexive transitive RelStr holds Ids b₁ = Filt (b₁ opp )

proof end;

definition

let c₁, c₂ be non empty complete Poset;
mode CLHomomorphism of c₁,c₂ -> Function of a₁,a₂ means :: WAYBEL16:def 1
( a₃ is directed-sups-preserving & a₃ is infs-preserving );
existence

proof end;

end;

:: deftheorem Def1 defines CLHomomorphism WAYBEL16:def 1 :

definition

let c₁ be non empty complete continuous Poset;
let c₂ be Subset of c₁;
pred c₂ is_FG_set means :: WAYBEL16:def 2
for b₁ being non empty complete continuous Poset
for b₂ being Function of a₂,the carrier of b₁ ex b₃ being CLHomomorphism of a₁,b₁ st
( b₃ | a₂ = b₂ & ( for b₄ being CLHomomorphism of a₁,b₁ st b₄ | a₂ = b₂ holds
b₄ = b₃ ) );

end;

:: deftheorem Def2 defines is_FG_set WAYBEL16:def 2 :

registration

let c₁ be non empty upper-bounded Poset;
cluster Filt a₁ -> non empty ;
coherence

proof end;

end;

theorem Th9: :: WAYBEL16:9

for b₁ being set
for b₂ being non empty Subset of (InclPoset (Filt (BoolePoset b₁))) holds meet b₂ is Filter of (BoolePoset b₁)

proof end;

theorem Th10: :: WAYBEL16:10

for b₁ being set
for b₂ being non empty Subset of (InclPoset (Filt (BoolePoset b₁))) holds
( ex_inf_of b₂, InclPoset (Filt (BoolePoset b₁)) & "/\" b₂,(InclPoset (Filt (BoolePoset b₁))) = meet b₂ )

proof end;

theorem Th11: :: WAYBEL16:11

for b₁ being set holds bool b₁ is Filter of (BoolePoset b₁)

proof end;

theorem Th12: :: WAYBEL16:12

for b₁ being set holds {b₁} is Filter of (BoolePoset b₁)

proof end;

theorem Th13: :: WAYBEL16:13

for b₁ being set holds InclPoset (Filt (BoolePoset b₁)) is upper-bounded

proof end;

theorem Th14: :: WAYBEL16:14

for b₁ being set holds InclPoset (Filt (BoolePoset b₁)) is lower-bounded

proof end;

theorem Th15: :: WAYBEL16:15

for b₁ being set holds Top (InclPoset (Filt (BoolePoset b₁))) = bool b₁

proof end;

theorem Th16: :: WAYBEL16:16

for b₁ being set holds Bottom (InclPoset (Filt (BoolePoset b₁))) = {b₁}

proof end;

theorem Th17: :: WAYBEL16:17

for b₁ being non empty set
for b₂ being non empty Subset of (InclPoset b₁) st ex_sup_of b₂, InclPoset b₁ holds
union b₂ c= sup b₂

proof end;

theorem Th18: :: WAYBEL16:18

for b₁ being upper-bounded Semilattice holds InclPoset (Filt b₁) is complete

proof end;

registration

let c₁ be upper-bounded Semilattice;
cluster InclPoset (Filt a₁) -> complete ;
coherence by Th18;

end;

definition

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
attr a₂ is completely-irreducible means :Def3: :: WAYBEL16:def 3
ex_min_of (uparrow a₂) \ {a₂},a₁;

end;

:: deftheorem Def3 defines completely-irreducible WAYBEL16:def 3 :

theorem Th19: :: WAYBEL16:19

for b₁ being non empty RelStr
for b₂ being Element of b₁ st b₂ is completely-irreducible holds
"/\" ((uparrow b₂) \ {b₂}),b₁ <> b₂

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Irr WAYBEL16:def 4 :

theorem Th20: :: WAYBEL16:20

for b₁ being non empty Poset
for b₂ being Element of b₁ holds
( b₂ is completely-irreducible iff ex b₃ being Element of b₁ st
( b₂ < b₃ & ( for b₄ being Element of b₁ st b₂ < b₄ holds
b₃ <= b₄ ) & uparrow b₂ = {b₂} \/ (uparrow b₃) ) )

proof end;

theorem Th21: :: WAYBEL16:21

for b₁ being non empty upper-bounded Poset holds not Top b₁ in Irr b₁

proof end;

theorem Th22: :: WAYBEL16:22

for b₁ being Semilattice holds Irr b₁ c= IRR b₁

proof end;

theorem Th23: :: WAYBEL16:23

for b₁ being Semilattice
for b₂ being Element of b₁ st b₂ is completely-irreducible holds
b₂ is meet-irreducible

proof end;

theorem Th24: :: WAYBEL16:24

for b₁ being non empty Poset
for b₂ being Element of b₁ st b₂ is completely-irreducible holds
for b₃ being Subset of b₁ st ex_inf_of b₃,b₁ & b₂ = inf b₃ holds
b₂ in b₃

proof end;

theorem Th25: :: WAYBEL16:25

for b₁ being non empty Poset
for b₂ being Subset of b₁ st b₂ is order-generating holds
Irr b₁ c= b₂

proof end;

theorem Th26: :: WAYBEL16:26

for b₁ being complete LATTICE
for b₂ being Element of b₁ st ex b₃ being Element of b₁ st b₂ is_maximal_in the carrier of b₁ \ (uparrow b₃) holds
b₂ is completely-irreducible

proof end;

theorem Th27: :: WAYBEL16:27

for b₁ being transitive antisymmetric with_suprema RelStr
for b₂, b₃, b₄ being Element of b₁ st b₂ < b₃ & ( for b₅ being Element of b₁ st b₂ < b₅ holds
b₃ <= b₅ ) & not b₄ <= b₂ holds
b₂ "\/" b₄ = b₃ "\/" b₄

proof end;

theorem Th28: :: WAYBEL16:28

for b₁ being distributive LATTICE
for b₂, b₃, b₄ being Element of b₁ st b₂ < b₃ & ( for b₅ being Element of b₁ st b₂ < b₅ holds
b₃ <= b₅ ) & not b₄ <= b₂ holds
not b₄ "/\" b₃ <= b₂

proof end;

theorem Th29: :: WAYBEL16:29

for b₁ being complete distributive LATTICE st b₁ opp is meet-continuous holds
for b₂ being Element of b₁ st b₂ is completely-irreducible holds
the carrier of b₁ \ (downarrow b₂) is Open Filter of b₁

proof end;

theorem Th30: :: WAYBEL16:30

for b₁ being complete distributive LATTICE st b₁ opp is meet-continuous holds
for b₂ being Element of b₁ st b₂ is completely-irreducible holds
ex b₃ being Element of b₁ st
( b₃ in the carrier of (CompactSublatt b₁) & b₂ is_maximal_in the carrier of b₁ \ (uparrow b₃) )

proof end;

theorem Th31: :: WAYBEL16:31

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

proof end;

theorem Th32: :: WAYBEL16:32

for b₁ being lower-bounded algebraic LATTICE holds
( Irr b₁ is order-generating & ( for b₂ being Subset of b₁ st b₂ is order-generating holds
Irr b₁ c= b₂ ) )

proof end;

theorem Th33: :: WAYBEL16:33

for b₁ being lower-bounded algebraic LATTICE
for b₂ being Element of b₁ holds b₂ = "/\" ((uparrow b₂) /\ (Irr b₁)),b₁

proof end;

theorem Th34: :: WAYBEL16:34

for b₁ being non empty complete Poset
for b₂ being Subset of b₁
for b₃ being Element of b₁ st b₃ is completely-irreducible & b₃ = inf b₂ holds
b₃ in b₂

proof end;

theorem Th35: :: WAYBEL16:35

for b₁ being complete algebraic LATTICE
for b₂ being Element of b₁ st b₂ is completely-irreducible holds
b₂ = "/\" { b₃ where B is Element of b₁ : ( b₃ in uparrow b₂ & ex b₁ being Element of b₁ st
( b₄ in the carrier of (CompactSublatt b₁) & b₃ is_maximal_in the carrier of b₁ \ (uparrow b₄) ) ) } ,b₁

proof end;

theorem Th36: :: WAYBEL16:36

for b₁ being complete algebraic LATTICE
for b₂ being Element of b₁ holds
( ex b₃ being Element of b₁ st
( b₃ in the carrier of (CompactSublatt b₁) & b₂ is_maximal_in the carrier of b₁ \ (uparrow b₃) ) iff b₂ is completely-irreducible )

proof end;