:: Completely-Irreducible Elements
:: by Robert Milewski
::
:: Received February 9, 1998
:: Copyright (c) 1998-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies WAYBEL_0, SUBSET_1, LATTICES, XBOOLE_0, EQREL_1, ORDERS_2,
ORDERS_1, STRUCT_0, XXREAL_0, TARSKI, ARYTM_3, LATTICE3, ARYTM_0,
RELAT_1, RELAT_2, CARD_FIL, REWRITE1, FUNCT_1, FUNCOP_1, YELLOW_0,
SEQM_3, FINSET_1, ORDINAL2, YELLOW_1, SETFAM_1, WELLORD2, ZFMISC_1,
WAYBEL_1, WAYBEL_6, YELLOW_8, WAYBEL_2, INT_2, WAYBEL_3, WAYBEL_8,
RCOMP_1, WAYBEL16;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FINSET_1, RELSET_1, FUNCT_2,
FUNCOP_1, DOMAIN_1, ORDERS_1, STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0,
YELLOW_1, YELLOW_4, YELLOW_7, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3,
WAYBEL_4, WAYBEL_6, WAYBEL_8;
constructors DOMAIN_1, ORDERS_3, WAYBEL_1, YELLOW_4, WAYBEL_2, WAYBEL_3,
WAYBEL_4, WAYBEL_6, WAYBEL_8, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, LATTICE3,
YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_2, WAYBEL_3, YELLOW_7,
WAYBEL_6, WAYBEL_8;
requirements BOOLE, SUBSET;
begin :: Preliminaries
theorem :: WAYBEL16:1
for L be sup-Semilattice for x,y be Element of L holds "/\"((
uparrow x) /\ (uparrow y),L) = x "\/" y;
theorem :: WAYBEL16:2
for L be Semilattice for x,y be Element of L holds "\/"((downarrow x)
/\ (downarrow y),L) = x "/\" y;
theorem :: WAYBEL16:3
for L be non empty RelStr for x,y be Element of L st x
is_maximal_in (the carrier of L) \ uparrow y holds (uparrow x) \ {x} = (uparrow
x) /\ (uparrow y);
theorem :: WAYBEL16:4
for L be non empty RelStr for x,y be Element of L st x is_minimal_in (
the carrier of L) \ downarrow y holds (downarrow x) \ {x} = (downarrow x) /\ (
downarrow y);
theorem :: WAYBEL16:5
for L be with_suprema Poset for X,Y be Subset of L for X9,Y9 be
Subset of L opp st X = X9 & Y = Y9 holds X "\/" Y = X9 "/\" Y9;
theorem :: WAYBEL16:6
for L be with_infima Poset for X,Y be Subset of L for X9,Y9 be Subset
of L opp st X = X9 & Y = Y9 holds X "/\" Y = X9 "\/" Y9;
theorem :: WAYBEL16:7
for L be non empty reflexive transitive RelStr holds Filt L = Ids (L opp);
theorem :: WAYBEL16:8
for L be non empty reflexive transitive RelStr holds Ids L = Filt (L opp);
begin :: Free Generation Set
definition
let S,T be complete non empty Poset;
mode CLHomomorphism of S,T -> Function of S,T means
:: WAYBEL16:def 1
it is directed-sups-preserving infs-preserving;
end;
definition
let S be continuous complete non empty Poset;
let A be Subset of S;
pred A is_FG_set means
:: WAYBEL16:def 2
for T be continuous complete non empty Poset for f
be Function of A,the carrier of T ex h be CLHomomorphism of S,T st h|A = f &
for h9 be CLHomomorphism of S,T st h9|A = f holds h9 = h;
end;
registration
let L be upper-bounded non empty Poset;
cluster Filt L -> non empty;
end;
theorem :: WAYBEL16:9
for X be set for Y be non empty Subset of InclPoset Filt
BoolePoset X holds meet Y is Filter of BoolePoset X;
theorem :: WAYBEL16:10
for X be set for Y be non empty Subset of InclPoset Filt BoolePoset X
holds ex_inf_of Y,InclPoset Filt BoolePoset X & "/\"(Y,InclPoset Filt
BoolePoset X) = meet Y;
theorem :: WAYBEL16:11
for X be set holds bool X is Filter of BoolePoset X;
theorem :: WAYBEL16:12
for X be set holds {X} is Filter of BoolePoset X;
theorem :: WAYBEL16:13
for X be set holds InclPoset Filt BoolePoset X is upper-bounded;
theorem :: WAYBEL16:14
for X be set holds InclPoset Filt BoolePoset X is lower-bounded;
theorem :: WAYBEL16:15
for X be set holds Top (InclPoset Filt BoolePoset X) = bool X;
theorem :: WAYBEL16:16
for X be set holds Bottom (InclPoset Filt BoolePoset X) = {X};
theorem :: WAYBEL16:17
for X be non empty set for Y be non empty Subset of InclPoset X st
ex_sup_of Y,InclPoset X holds union Y c= sup Y;
theorem :: WAYBEL16:18
for L be upper-bounded Semilattice holds InclPoset Filt L is complete;
registration
let L be upper-bounded Semilattice;
cluster InclPoset Filt L -> complete;
end;
begin :: Completely-irreducible Elements
definition
let L be non empty RelStr;
let p be Element of L;
attr p is completely-irreducible means
:: WAYBEL16:def 3
ex_min_of (uparrow p)\{p},L;
end;
theorem :: WAYBEL16:19
for L be non empty RelStr for p be Element of L st p is
completely-irreducible holds "/\"((uparrow p)\{p},L) <> p;
definition
let L be non empty RelStr;
func Irr L -> Subset of L means
:: WAYBEL16:def 4
for x be Element of L holds x in it iff x is completely-irreducible;
end;
theorem :: WAYBEL16:20 :: THEOREM 4.19 (i)
for L be non empty Poset for p be Element of L holds p is
completely-irreducible iff ex q be Element of L st p < q & (for s be Element of
L st p < s holds q <= s) & uparrow p = {p} \/ uparrow q;
theorem :: WAYBEL16:21 :: THEOREM 4.19 (ii)
for L be upper-bounded non empty Poset holds not Top L in Irr L;
theorem :: WAYBEL16:22 :: THEOREM 4.19 (iii)
for L be Semilattice holds Irr L c= IRR L;
theorem :: WAYBEL16:23
for L be Semilattice for x be Element of L holds x is
completely-irreducible implies x is irreducible;
theorem :: WAYBEL16:24
for L be non empty Poset for x be Element of L holds x is
completely-irreducible implies for X be Subset of L st ex_inf_of X,L & x = inf
X holds x in X;
theorem :: WAYBEL16:25 :: REMARK 4.20
for L be non empty Poset for X be Subset of L st X is
order-generating holds Irr L c= X;
theorem :: WAYBEL16:26 :: PROPOSITION 4.21 (i)
for L be complete LATTICE for p be Element of L holds (ex k be
Element of L st p is_maximal_in (the carrier of L) \ uparrow k) implies p is
completely-irreducible;
theorem :: WAYBEL16:27
for L be transitive antisymmetric with_suprema RelStr for p,q,u
be Element of L st p < q & (for s be Element of L st p < s holds q <= s) & not
u <= p holds p "\/" u = q "\/" u;
theorem :: WAYBEL16:28
for L be distributive LATTICE for p,q,u be Element of L st p < q
& (for s be Element of L st p < s holds q <= s) & not u <= p holds not u "/\" q
<= p;
theorem :: WAYBEL16:29
for L be distributive complete LATTICE st L opp is
meet-continuous for p be Element of L st p is completely-irreducible holds (the
carrier of L) \ downarrow p is Open Filter of L;
theorem :: WAYBEL16:30 :: PROPOSITION 4.21 (ii)
for L be distributive complete LATTICE st L opp is meet-continuous for
p be Element of L holds p is completely-irreducible implies ex k be Element of
L st k in the carrier of CompactSublatt L & p is_maximal_in (the carrier of L)
\ uparrow k;
theorem :: WAYBEL16:31 :: THEOREM 4.22
for L be lower-bounded algebraic LATTICE for x,y be Element of L
holds not y <= x implies ex p be Element of L st p is completely-irreducible &
x <= p & not y <= p;
theorem :: WAYBEL16:32 :: THEOREM 4.23 (i)
for L be lower-bounded algebraic LATTICE holds Irr L is
order-generating & for X be Subset of L st X is order-generating holds Irr L c=
X;
theorem :: WAYBEL16:33 :: THEOREM 4.23 (ii)
for L be lower-bounded algebraic LATTICE for s be Element of L holds s
= "/\" (uparrow s /\ Irr L,L);
theorem :: WAYBEL16:34
for L be complete non empty Poset for X be Subset of L for p
be Element of L st p is completely-irreducible & p = inf X holds p in X;
theorem :: WAYBEL16:35
for L be complete algebraic LATTICE for p be Element of L st p
is completely-irreducible holds p = "/\" ({ x where x is Element of L : x in
uparrow p & ex k be Element of L st k in the carrier of CompactSublatt L & x
is_maximal_in (the carrier of L) \ uparrow k },L);
theorem :: WAYBEL16:36 :: COROLLARY 4.24
for L be complete algebraic LATTICE for p be Element of L holds (ex k
be 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;