WAYBEL16: Completely-Irreducible Elements

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

proof end;

end;

:: deftheorem defines CLHomomorphism WAYBEL16:def 1 :

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 :

registration

let L be non empty upper-bounded Poset;
cluster Filt L -> non empty ;
coherence

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

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

proof end;

proof end;

end;

:: deftheorem Def4 defines Irr WAYBEL16:def 4 :

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;