:: by Robert Milewski

::

:: Received February 9, 1998

:: Copyright (c) 1998-2021 Association of Mizar Users

theorem Th1: :: WAYBEL16:1

for L being sup-Semilattice

for x, y being Element of L holds "/\" (((uparrow x) /\ (uparrow y)),L) = x "\/" y

for x, y being Element of L holds "/\" (((uparrow x) /\ (uparrow y)),L) = x "\/" y

proof end;

theorem :: WAYBEL16:2

for L being Semilattice

for x, y being Element of L holds "\/" (((downarrow x) /\ (downarrow y)),L) = x "/\" y

for x, y being Element of L holds "\/" (((downarrow x) /\ (downarrow y)),L) = x "/\" y

proof end;

theorem Th3: :: WAYBEL16:3

for L being non empty RelStr

for x, y being Element of L st x is_maximal_in the carrier of L \ (uparrow y) holds

(uparrow x) \ {x} = (uparrow x) /\ (uparrow y)

for x, y being Element of L st x is_maximal_in the carrier of L \ (uparrow y) holds

(uparrow x) \ {x} = (uparrow x) /\ (uparrow y)

proof end;

theorem :: WAYBEL16:4

for L being non empty RelStr

for x, y being Element of L st x is_minimal_in the carrier of L \ (downarrow y) holds

(downarrow x) \ {x} = (downarrow x) /\ (downarrow y)

for x, y being Element of L st x is_minimal_in the carrier of L \ (downarrow y) holds

(downarrow x) \ {x} = (downarrow x) /\ (downarrow y)

proof end;

theorem Th5: :: WAYBEL16:5

for L being with_suprema Poset

for X, Y being Subset of L

for X9, Y9 being Subset of (L opp) st X = X9 & Y = Y9 holds

X "\/" Y = X9 "/\" Y9

for X, Y being Subset of L

for X9, Y9 being Subset of (L opp) st X = X9 & Y = Y9 holds

X "\/" Y = X9 "/\" Y9

proof end;

theorem :: WAYBEL16:6

for L being with_infima Poset

for X, Y being Subset of L

for X9, Y9 being Subset of (L opp) st X = X9 & Y = Y9 holds

X "/\" Y = X9 "\/" Y9

for X, Y being Subset of L

for X9, Y9 being Subset of (L opp) st X = X9 & Y = Y9 holds

X "/\" Y = X9 "\/" Y9

proof end;

definition

let S, T be non empty complete Poset;

ex b_{1} being Function of S,T st

( b_{1} is directed-sups-preserving & b_{1} is infs-preserving )

end;
mode CLHomomorphism of S,T -> Function of S,T means :: WAYBEL16:def 1

( it is directed-sups-preserving & it is infs-preserving );

existence ( it is directed-sups-preserving & it is infs-preserving );

ex b

( b

proof end;

:: deftheorem defines CLHomomorphism WAYBEL16:def 1 :

for S, T being non empty complete Poset

for b_{3} being Function of S,T holds

( b_{3} is CLHomomorphism of S,T iff ( b_{3} is directed-sups-preserving & b_{3} is infs-preserving ) );

for S, T being non empty complete Poset

for b

( b

definition

let S be non empty complete continuous Poset;

let A be Subset of S;

end;
let A be Subset of S;

pred A is_FG_set means :: WAYBEL16:def 2

for T being non empty complete continuous Poset

for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st

( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds

h9 = h ) );

for T being non empty complete continuous Poset

for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st

( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds

h9 = h ) );

:: deftheorem defines is_FG_set WAYBEL16:def 2 :

for S being non empty complete continuous Poset

for A being Subset of S holds

( A is_FG_set iff for T being non empty complete continuous Poset

for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st

( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds

h9 = h ) ) );

for S being non empty complete continuous Poset

for A being Subset of S holds

( A is_FG_set iff for T being non empty complete continuous Poset

for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st

( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds

h9 = h ) ) );

theorem Th9: :: WAYBEL16:9

for X being set

for Y being non empty Subset of (InclPoset (Filt (BoolePoset X))) holds meet Y is Filter of (BoolePoset X)

for Y being non empty Subset of (InclPoset (Filt (BoolePoset X))) holds meet Y is Filter of (BoolePoset X)

proof end;

theorem :: WAYBEL16:10

for X being set

for Y being non empty Subset of (InclPoset (Filt (BoolePoset X))) holds

( ex_inf_of Y, InclPoset (Filt (BoolePoset X)) & "/\" (Y,(InclPoset (Filt (BoolePoset X)))) = meet Y )

for Y being non empty Subset of (InclPoset (Filt (BoolePoset X))) holds

( ex_inf_of Y, InclPoset (Filt (BoolePoset X)) & "/\" (Y,(InclPoset (Filt (BoolePoset X)))) = meet Y )

proof end;

theorem :: WAYBEL16:17

for X being non empty set

for Y being non empty Subset of (InclPoset X) st ex_sup_of Y, InclPoset X holds

union Y c= sup Y

for Y being non empty Subset of (InclPoset X) st ex_sup_of Y, InclPoset X holds

union Y c= sup Y

proof end;

registration
end;

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

for L being non empty RelStr

for p being Element of L holds

( p is completely-irreducible iff ex_min_of (uparrow p) \ {p},L );

for L being non empty RelStr

for p being Element of L holds

( p is completely-irreducible iff ex_min_of (uparrow p) \ {p},L );

theorem Th19: :: WAYBEL16:19

for L being non empty RelStr

for p being Element of L st p is completely-irreducible holds

"/\" (((uparrow p) \ {p}),L) <> p

for p being Element of L st p is completely-irreducible holds

"/\" (((uparrow p) \ {p}),L) <> p

proof end;

definition

let L be non empty RelStr ;

ex b_{1} being Subset of L st

for x being Element of L holds

( x in b_{1} iff x is completely-irreducible )

for b_{1}, b_{2} being Subset of L st ( for x being Element of L holds

( x in b_{1} iff x is completely-irreducible ) ) & ( for x being Element of L holds

( x in b_{2} iff x is completely-irreducible ) ) holds

b_{1} = b_{2}

end;
func Irr L -> Subset of L means :Def4: :: WAYBEL16:def 4

for x being Element of L holds

( x in it iff x is completely-irreducible );

existence for x being Element of L holds

( x in it iff x is completely-irreducible );

ex b

for x being Element of L holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def4 defines Irr WAYBEL16:def 4 :

for L being non empty RelStr

for b_{2} being Subset of L holds

( b_{2} = Irr L iff for x being Element of L holds

( x in b_{2} iff x is completely-irreducible ) );

for L being non empty RelStr

for b

( b

( x in b

theorem Th20: :: WAYBEL16:20

for L being non empty Poset

for p being Element of L holds

( p is completely-irreducible iff ex q being Element of L st

( p < q & ( for s being Element of L st p < s holds

q <= s ) & uparrow p = {p} \/ (uparrow q) ) )

for p being Element of L holds

( p is completely-irreducible iff ex q being Element of L st

( p < q & ( for s being Element of L st p < s holds

q <= s ) & uparrow p = {p} \/ (uparrow q) ) )

proof end;

theorem Th23: :: WAYBEL16:23

for L being Semilattice

for x being Element of L st x is completely-irreducible holds

x is irreducible

for x being Element of L st x is completely-irreducible holds

x is irreducible

proof end;

theorem Th24: :: WAYBEL16:24

for L being non empty Poset

for x being Element of L st x is completely-irreducible holds

for X being Subset of L st ex_inf_of X,L & x = inf X holds

x in X

for x being Element of L st x is completely-irreducible holds

for X being Subset of L st ex_inf_of X,L & x = inf X holds

x in X

proof end;

theorem Th26: :: WAYBEL16:26

for L being complete LATTICE

for p being Element of L st ex k being Element of L st p is_maximal_in the carrier of L \ (uparrow k) holds

p is completely-irreducible

for p being Element of L st ex k being Element of L st p is_maximal_in the carrier of L \ (uparrow k) holds

p is completely-irreducible

proof end;

theorem Th27: :: WAYBEL16:27

for L being transitive antisymmetric with_suprema RelStr

for p, q, u being Element of L st p < q & ( for s being Element of L st p < s holds

q <= s ) & not u <= p holds

p "\/" u = q "\/" u

for p, q, u being Element of L st p < q & ( for s being Element of L st p < s holds

q <= s ) & not u <= p holds

p "\/" u = q "\/" u

proof end;

theorem Th28: :: WAYBEL16:28

for L being distributive LATTICE

for p, q, u being Element of L st p < q & ( for s being Element of L st p < s holds

q <= s ) & not u <= p holds

not u "/\" q <= p

for p, q, u being Element of L st p < q & ( for s being Element of L st p < s holds

q <= s ) & not u <= p holds

not u "/\" q <= p

proof end;

theorem Th29: :: WAYBEL16:29

for L being distributive complete LATTICE st L opp is meet-continuous holds

for p being Element of L st p is completely-irreducible holds

the carrier of L \ (downarrow p) is Open Filter of L

for p being Element of L st p is completely-irreducible holds

the carrier of L \ (downarrow p) is Open Filter of L

proof end;

theorem :: WAYBEL16:30

for L being distributive complete LATTICE st L opp is meet-continuous holds

for p being Element of L st p is completely-irreducible holds

ex k being Element of L st

( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) )

for p being Element of L st p is completely-irreducible holds

ex k being Element of L st

( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) )

proof end;

theorem Th31: :: WAYBEL16:31

for L being lower-bounded algebraic LATTICE

for x, y being Element of L st not y <= x holds

ex p being Element of L st

( p is completely-irreducible & x <= p & not y <= p )

for x, y being Element of L st not y <= x holds

ex p being Element of L st

( p is completely-irreducible & x <= p & not y <= p )

proof end;

theorem Th32: :: WAYBEL16:32

for L being lower-bounded algebraic LATTICE holds

( Irr L is order-generating & ( for X being Subset of L st X is order-generating holds

Irr L c= X ) )

( Irr L is order-generating & ( for X being Subset of L st X is order-generating holds

Irr L c= X ) )

proof end;

theorem :: WAYBEL16:33

for L being lower-bounded algebraic LATTICE

for s being Element of L holds s = "/\" (((uparrow s) /\ (Irr L)),L)

for s being Element of L holds s = "/\" (((uparrow s) /\ (Irr L)),L)

proof end;

theorem Th34: :: WAYBEL16:34

for L being non empty complete Poset

for X being Subset of L

for p being Element of L st p is completely-irreducible & p = inf X holds

p in X

for X being Subset of L

for p being Element of L st p is completely-irreducible & p = inf X holds

p in X

proof end;

theorem Th35: :: WAYBEL16:35

for L being complete algebraic LATTICE

for p being Element of L st p is completely-irreducible holds

p = "/\" ( { x where x is Element of L : ( x in uparrow p & ex k being Element of L st

( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) ) } ,L)

for p being Element of L st p is completely-irreducible holds

p = "/\" ( { x where x is Element of L : ( x in uparrow p & ex k being Element of L st

( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) ) } ,L)

proof end;

theorem :: WAYBEL16:36

for L being complete algebraic LATTICE

for p being Element of L holds

( ex k being Element of L st

( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) ) iff p is completely-irreducible )

for p being Element of L holds

( ex k being Element of L st

( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) ) iff p is completely-irreducible )

proof end;