:: Completely-Irreducible Elements
:: by Robert Milewski
::
:: Received February 9, 1998
:: Copyright (c) 1998-2011 Association of Mizar Users


begin

theorem Th1: :: WAYBEL16:1
for L being sup-Semilattice
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
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)
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)
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
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
proof end;

theorem Th7: :: WAYBEL16:7
for L being non empty reflexive transitive RelStr holds Filt L = Ids (L opp)
proof end;

theorem :: WAYBEL16:8
for L being non empty reflexive transitive RelStr holds Ids L = Filt (L opp)
proof end;

begin

definition
let S, T be non empty complete Poset;
mode CLHomomorphism of S,T -> Function of S,T means :: WAYBEL16:def 1
( it is directed-sups-preserving & it is infs-preserving );
existence
ex b1 being Function of S,T st
( b1 is directed-sups-preserving & b1 is infs-preserving )
proof end;
end;

:: deftheorem defines CLHomomorphism WAYBEL16:def 1 :
for S, T being non empty complete Poset
for b3 being Function of S,T holds
( b3 is CLHomomorphism of S,T iff ( b3 is directed-sups-preserving & b3 is infs-preserving ) );

definition
let S be non empty complete continuous Poset;
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 ) );
end;

:: 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 ) ) );

registration
let L be non empty upper-bounded Poset;
cluster Filt L -> non empty ;
coherence
not Filt L is empty
proof end;
end;

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)
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 )
proof end;

theorem Th11: :: WAYBEL16:11
for X being set holds bool X is Filter of (BoolePoset X)
proof end;

theorem Th12: :: WAYBEL16:12
for X being set holds {X} is Filter of (BoolePoset X)
proof end;

theorem :: WAYBEL16:13
for X being set holds InclPoset (Filt (BoolePoset X)) is upper-bounded
proof end;

theorem :: WAYBEL16:14
for X being set holds InclPoset (Filt (BoolePoset X)) is lower-bounded
proof end;

theorem :: WAYBEL16:15
for X being set holds Top (InclPoset (Filt (BoolePoset X))) = bool X
proof end;

theorem :: WAYBEL16:16
for X being set holds Bottom (InclPoset (Filt (BoolePoset X))) = {X}
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
proof end;

theorem Th18: :: WAYBEL16:18
for L being upper-bounded Semilattice holds InclPoset (Filt L) is complete
proof end;

registration
let L be upper-bounded Semilattice;
cluster InclPoset (Filt L) -> complete ;
coherence
InclPoset (Filt L) is complete
by Th18;
end;

begin

definition
let L be non empty RelStr ;
let p be Element of L;
attr p is completely-irreducible means :Def3: :: WAYBEL16:def 3
ex_min_of (uparrow p) \ {p},L;
end;

:: deftheorem Def3 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 );

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
proof end;

definition
let L be non empty RelStr ;
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
ex b1 being Subset of L st
for x being Element of L holds
( x in b1 iff x is completely-irreducible )
proof end;
uniqueness
for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff x is completely-irreducible ) ) & ( for x being Element of L holds
( x in b2 iff x is completely-irreducible ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Irr WAYBEL16:def 4 :
for L being non empty RelStr
for b2 being Subset of L holds
( b2 = Irr L iff for x being Element of L holds
( x in b2 iff x is completely-irreducible ) );

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) ) )
proof end;

theorem Th21: :: WAYBEL16:21
for L being non empty upper-bounded Poset holds not Top L in Irr L
proof end;

theorem Th22: :: WAYBEL16:22
for L being Semilattice holds Irr L c= IRR L
proof end;

theorem Th23: :: WAYBEL16:23
for L being Semilattice
for x being Element of L st x is completely-irreducible holds
x is meet-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
proof end;

theorem Th25: :: WAYBEL16:25
for L being non empty Poset
for X being Subset of L st X is order-generating holds
Irr L c= 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
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
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
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
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) )
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 )
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 ) )
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)
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
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)
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 )
proof end;