:: WAYBEL16 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: WAYBEL16:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being with_suprema Poset
for X, Y being Subset of L
for X', Y' being Subset of (L opp ) st X = X' & Y = Y' holds
X "\/" Y = X' "/\" Y'
proof end;

theorem :: WAYBEL16:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being with_infima Poset
for X, Y being Subset of L
for X', Y' being Subset of (L opp ) st X = X' & Y = Y' holds
X "/\" Y = X' "\/" Y'
proof end;

theorem Th7: :: WAYBEL16:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive RelStr holds Filt L = Ids (L opp )
proof end;

theorem :: WAYBEL16:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive RelStr holds Ids L = Filt (L opp )
proof end;

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 h' being CLHomomorphism of S,T st h' | A = f holds
h' = 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 h' being CLHomomorphism of S,T st h' | A = f holds
h' = 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds bool X is Filter of (BoolePoset X)
proof end;

theorem Th12: :: WAYBEL16:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds {X} is Filter of (BoolePoset X)
proof end;

theorem :: WAYBEL16:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds InclPoset (Filt (BoolePoset X)) is upper-bounded
proof end;

theorem :: WAYBEL16:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds InclPoset (Filt (BoolePoset X)) is lower-bounded
proof end;

theorem :: WAYBEL16:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds Top (InclPoset (Filt (BoolePoset X))) = bool X
proof end;

theorem :: WAYBEL16:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds Bottom (InclPoset (Filt (BoolePoset X))) = {X}
proof end;

theorem :: WAYBEL16:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty upper-bounded Poset holds not Top L in Irr L
proof end;

theorem Th22: :: WAYBEL16:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Semilattice holds Irr L c= IRR L
proof end;

theorem Th23: :: WAYBEL16:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete distributive 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete distributive 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;