:: Directed Sets, Nets, Ideals, Filters, and Maps
:: by Grzegorz Bancerek
::
:: Copyright (c) 1996-2012 Association of Mizar Users

begin

definition
let L be RelStr ;
let X be Subset of L;
attr X is directed means :Def1: :: WAYBEL_0:def 1
for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & x <= z & y <= z );
attr X is filtered means :Def2: :: WAYBEL_0:def 2
for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & z <= x & z <= y );
end;

:: deftheorem Def1 defines directed WAYBEL_0:def 1 :
for L being RelStr
for X being Subset of L holds
( X is directed iff for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & x <= z & y <= z ) );

:: deftheorem Def2 defines filtered WAYBEL_0:def 2 :
for L being RelStr
for X being Subset of L holds
( X is filtered iff for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & z <= x & z <= y ) );

:: Original "directed subset" is equivalent to "non empty directed subset"
:: in our terminology. It is shown bellow.
theorem Th1: :: WAYBEL_0:1
for L being non empty transitive RelStr
for X being Subset of L holds
( ( not X is empty & X is directed ) iff for Y being finite Subset of X ex x being Element of L st
( x in X & x is_>=_than Y ) )
proof end;

:: Original "filtered subset" is equivalent to "non empty filtered subset"
:: in our terminology. It is shown bellow.
theorem Th2: :: WAYBEL_0:2
for L being non empty transitive RelStr
for X being Subset of L holds
( ( not X is empty & X is filtered ) iff for Y being finite Subset of X ex x being Element of L st
( x in X & x is_<=_than Y ) )
proof end;

registration
let L be RelStr ;
cluster empty -> directed filtered for Element of K10( the carrier of L);
coherence
for b1 being Subset of L st b1 is empty holds
( b1 is directed & b1 is filtered )
proof end;
end;

registration
let L be RelStr ;
cluster directed filtered for Element of K10( the carrier of L);
existence
ex b1 being Subset of L st
( b1 is directed & b1 is filtered )
proof end;
end;

theorem Th3: :: WAYBEL_0:3
for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 & X1 is directed holds
X2 is directed
proof end;

theorem :: WAYBEL_0:4
for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 & X1 is filtered holds
X2 is filtered
proof end;

theorem Th5: :: WAYBEL_0:5
for L being non empty reflexive RelStr
for x being Element of L holds
( {x} is directed & {x} is filtered )
proof end;

registration
let L be non empty reflexive RelStr ;
cluster non empty finite directed filtered for Element of K10( the carrier of L);
existence
ex b1 being Subset of L st
( b1 is directed & b1 is filtered & not b1 is empty & b1 is finite )
proof end;
end;

registration
let L be with_suprema RelStr ;
coherence
[#] L is directed
proof end;
end;

registration
let L be non empty upper-bounded RelStr ;
coherence
[#] L is directed
proof end;
end;

registration
let L be with_infima RelStr ;
coherence
[#] L is filtered
proof end;
end;

registration
let L be non empty lower-bounded RelStr ;
coherence
[#] L is filtered
proof end;
end;

definition
let L be non empty RelStr ;
let S be SubRelStr of L;
attr S is filtered-infs-inheriting means :Def3: :: WAYBEL_0:def 3
for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds
"/\" (X,L) in the carrier of S;
attr S is directed-sups-inheriting means :Def4: :: WAYBEL_0:def 4
for X being directed Subset of S st X <> {} & ex_sup_of X,L holds
"\/" (X,L) in the carrier of S;
end;

:: deftheorem Def3 defines filtered-infs-inheriting WAYBEL_0:def 3 :
for L being non empty RelStr
for S being SubRelStr of L holds
( S is filtered-infs-inheriting iff for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds
"/\" (X,L) in the carrier of S );

:: deftheorem Def4 defines directed-sups-inheriting WAYBEL_0:def 4 :
for L being non empty RelStr
for S being SubRelStr of L holds
( S is directed-sups-inheriting iff for X being directed Subset of S st X <> {} & ex_sup_of X,L holds
"\/" (X,L) in the carrier of S );

registration
let L be non empty RelStr ;
coherence
for b1 being SubRelStr of L st b1 is infs-inheriting holds
b1 is filtered-infs-inheriting
proof end;
coherence
for b1 being SubRelStr of L st b1 is sups-inheriting holds
b1 is directed-sups-inheriting
proof end;
end;

registration
let L be non empty RelStr ;
existence
ex b1 being SubRelStr of L st
( b1 is infs-inheriting & b1 is sups-inheriting & not b1 is empty & b1 is full & b1 is strict )
proof end;
end;

theorem :: WAYBEL_0:6
for L being non empty transitive RelStr
for S being non empty full filtered-infs-inheriting SubRelStr of L
for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds
( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) )
proof end;

theorem :: WAYBEL_0:7
for L being non empty transitive RelStr
for S being non empty full directed-sups-inheriting SubRelStr of L
for X being directed Subset of S st X <> {} & ex_sup_of X,L holds
( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) )
proof end;

begin

definition
let L1, L2 be RelStr ;
let f be Function of L1,L2;
attr f is antitone means :: WAYBEL_0:def 5
for x, y being Element of L1 st x <= y holds
for a, b being Element of L2 st a = f . x & b = f . y holds
a >= b;
end;

:: deftheorem defines antitone WAYBEL_0:def 5 :
for L1, L2 being RelStr
for f being Function of L1,L2 holds
( f is antitone iff for x, y being Element of L1 st x <= y holds
for a, b being Element of L2 st a = f . x & b = f . y holds
a >= b );

:: Definition 1.2
definition
let L be 1-sorted ;
attr c2 is strict ;
struct NetStr over L -> RelStr ;
aggr NetStr(# carrier, InternalRel, mapping #) -> NetStr over L;
sel mapping c2 -> Function of the carrier of c2, the carrier of L;
end;

registration
let L be 1-sorted ;
let X be non empty set ;
let O be Relation of X;
let F be Function of X, the carrier of L;
cluster NetStr(# X,O,F #) -> non empty ;
coherence
not NetStr(# X,O,F #) is empty
;
end;

definition
let N be RelStr ;
attr N is directed means :Def6: :: WAYBEL_0:def 6
[#] N is directed ;
end;

:: deftheorem Def6 defines directed WAYBEL_0:def 6 :
for N being RelStr holds
( N is directed iff [#] N is directed );

registration
let L be 1-sorted ;
existence
ex b1 being strict NetStr over L st
( not b1 is empty & b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is directed )
proof end;
end;

definition
let L be 1-sorted ;
mode prenet of L is non empty directed NetStr over L;
end;

definition
let L be 1-sorted ;
mode net of L is transitive prenet of L;
end;

definition
let L be non empty 1-sorted ;
let N be non empty NetStr over L;
func netmap (N,L) -> Function of N,L equals :: WAYBEL_0:def 7
the mapping of N;
coherence
the mapping of N is Function of N,L
;
let i be Element of N;
func N . i -> Element of L equals :: WAYBEL_0:def 8
the mapping of N . i;
correctness
coherence
the mapping of N . i is Element of L
;
;
end;

:: deftheorem defines netmap WAYBEL_0:def 7 :
for L being non empty 1-sorted
for N being non empty NetStr over L holds netmap (N,L) = the mapping of N;

:: deftheorem defines . WAYBEL_0:def 8 :
for L being non empty 1-sorted
for N being non empty NetStr over L
for i being Element of N holds N . i = the mapping of N . i;

definition
let L be non empty RelStr ;
let N be non empty NetStr over L;
attr N is monotone means :: WAYBEL_0:def 9
netmap (N,L) is monotone ;
attr N is antitone means :: WAYBEL_0:def 10
netmap (N,L) is antitone ;
end;

:: deftheorem defines monotone WAYBEL_0:def 9 :
for L being non empty RelStr
for N being non empty NetStr over L holds
( N is monotone iff netmap (N,L) is monotone );

:: deftheorem defines antitone WAYBEL_0:def 10 :
for L being non empty RelStr
for N being non empty NetStr over L holds
( N is antitone iff netmap (N,L) is antitone );

definition
let L be non empty 1-sorted ;
let N be non empty NetStr over L;
let X be set ;
pred N is_eventually_in X means :Def11: :: WAYBEL_0:def 11
ex i being Element of N st
for j being Element of N st i <= j holds
N . j in X;
pred N is_often_in X means :: WAYBEL_0:def 12
for i being Element of N ex j being Element of N st
( i <= j & N . j in X );
end;

:: deftheorem Def11 defines is_eventually_in WAYBEL_0:def 11 :
for L being non empty 1-sorted
for N being non empty NetStr over L
for X being set holds
( N is_eventually_in X iff ex i being Element of N st
for j being Element of N st i <= j holds
N . j in X );

:: deftheorem defines is_often_in WAYBEL_0:def 12 :
for L being non empty 1-sorted
for N being non empty NetStr over L
for X being set holds
( N is_often_in X iff for i being Element of N ex j being Element of N st
( i <= j & N . j in X ) );

theorem :: WAYBEL_0:8
for L being non empty 1-sorted
for N being non empty NetStr over L
for X, Y being set st X c= Y holds
( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) )
proof end;

theorem :: WAYBEL_0:9
for L being non empty 1-sorted
for N being non empty NetStr over L
for X being set holds
( N is_eventually_in X iff not N is_often_in the carrier of L \ X )
proof end;

theorem :: WAYBEL_0:10
for L being non empty 1-sorted
for N being non empty NetStr over L
for X being set holds
( N is_often_in X iff not N is_eventually_in the carrier of L \ X )
proof end;

scheme :: WAYBEL_0:sch 1
HoldsEventually{ F1() -> non empty RelStr , F2() -> non empty NetStr over F1(), P1[ set ] } :
( F2() is_eventually_in { (F2() . k) where k is Element of F2() : P1[F2() . k] } iff ex i being Element of F2() st
for j being Element of F2() st i <= j holds
P1[F2() . j] )
proof end;

definition
let L be non empty RelStr ;
let N be non empty NetStr over L;
attr N is eventually-directed means :Def13: :: WAYBEL_0:def 13
for i being Element of N holds N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j } ;
attr N is eventually-filtered means :Def14: :: WAYBEL_0:def 14
for i being Element of N holds N is_eventually_in { (N . j) where j is Element of N : N . i >= N . j } ;
end;

:: deftheorem Def13 defines eventually-directed WAYBEL_0:def 13 :
for L being non empty RelStr
for N being non empty NetStr over L holds
( N is eventually-directed iff for i being Element of N holds N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j } );

:: deftheorem Def14 defines eventually-filtered WAYBEL_0:def 14 :
for L being non empty RelStr
for N being non empty NetStr over L holds
( N is eventually-filtered iff for i being Element of N holds N is_eventually_in { (N . j) where j is Element of N : N . i >= N . j } );

theorem Th11: :: WAYBEL_0:11
for L being non empty RelStr
for N being non empty NetStr over L holds
( N is eventually-directed iff for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds
N . i <= N . k )
proof end;

theorem Th12: :: WAYBEL_0:12
for L being non empty RelStr
for N being non empty NetStr over L holds
( N is eventually-filtered iff for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds
N . i >= N . k )
proof end;

registration
let L be non empty RelStr ;
cluster non empty directed monotone -> eventually-directed for NetStr over L;
coherence
for b1 being prenet of L st b1 is monotone holds
b1 is eventually-directed
proof end;
cluster non empty directed antitone -> eventually-filtered for NetStr over L;
coherence
for b1 being prenet of L st b1 is antitone holds
b1 is eventually-filtered
proof end;
end;

registration
let L be non empty reflexive RelStr ;
cluster non empty strict directed monotone antitone for NetStr over L;
existence
ex b1 being prenet of L st
( b1 is monotone & b1 is antitone & b1 is strict )
proof end;
end;

begin

:: Definition 1.3
definition
let L be RelStr ;
let X be Subset of L;
func downarrow X -> Subset of L means :Def15: :: WAYBEL_0:def 15
for x being Element of L holds
( x in it iff ex y being Element of L st
( y >= x & y in X ) );
existence
ex b1 being Subset of L st
for x being Element of L holds
( x in b1 iff ex y being Element of L st
( y >= x & y in X ) )
proof end;
uniqueness
for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff ex y being Element of L st
( y >= x & y in X ) ) ) & ( for x being Element of L holds
( x in b2 iff ex y being Element of L st
( y >= x & y in X ) ) ) holds
b1 = b2
proof end;
func uparrow X -> Subset of L means :Def16: :: WAYBEL_0:def 16
for x being Element of L holds
( x in it iff ex y being Element of L st
( y <= x & y in X ) );
existence
ex b1 being Subset of L st
for x being Element of L holds
( x in b1 iff ex y being Element of L st
( y <= x & y in X ) )
proof end;
correctness
uniqueness
for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff ex y being Element of L st
( y <= x & y in X ) ) ) & ( for x being Element of L holds
( x in b2 iff ex y being Element of L st
( y <= x & y in X ) ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def15 defines downarrow WAYBEL_0:def 15 :
for L being RelStr
for X, b3 being Subset of L holds
( b3 = downarrow X iff for x being Element of L holds
( x in b3 iff ex y being Element of L st
( y >= x & y in X ) ) );

:: deftheorem Def16 defines uparrow WAYBEL_0:def 16 :
for L being RelStr
for X, b3 being Subset of L holds
( b3 = uparrow X iff for x being Element of L holds
( x in b3 iff ex y being Element of L st
( y <= x & y in X ) ) );

theorem Th13: :: WAYBEL_0:13
for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for X being Subset of L1
for Y being Subset of L2 st X = Y holds
( downarrow X = downarrow Y & uparrow X = uparrow Y )
proof end;

theorem Th14: :: WAYBEL_0:14
for L being non empty RelStr
for X being Subset of L holds downarrow X = { x where x is Element of L : ex y being Element of L st
( x <= y & y in X )
}
proof end;

theorem Th15: :: WAYBEL_0:15
for L being non empty RelStr
for X being Subset of L holds uparrow X = { x where x is Element of L : ex y being Element of L st
( x >= y & y in X )
}
proof end;

registration
let L be non empty reflexive RelStr ;
let X be non empty Subset of L;
cluster downarrow X -> non empty ;
coherence
not downarrow X is empty
proof end;
cluster uparrow X -> non empty ;
coherence
not uparrow X is empty
proof end;
end;

theorem Th16: :: WAYBEL_0:16
for L being reflexive RelStr
for X being Subset of L holds
( X c= downarrow X & X c= uparrow X )
proof end;

definition
let L be non empty RelStr ;
let x be Element of L;
func downarrow x -> Subset of L equals :: WAYBEL_0:def 17
downarrow {x};
correctness
coherence
downarrow {x} is Subset of L
;
;
func uparrow x -> Subset of L equals :: WAYBEL_0:def 18
uparrow {x};
correctness
coherence
uparrow {x} is Subset of L
;
;
end;

:: deftheorem defines downarrow WAYBEL_0:def 17 :
for L being non empty RelStr
for x being Element of L holds downarrow x = downarrow {x};

:: deftheorem defines uparrow WAYBEL_0:def 18 :
for L being non empty RelStr
for x being Element of L holds uparrow x = uparrow {x};

theorem Th17: :: WAYBEL_0:17
for L being non empty RelStr
for x, y being Element of L holds
( y in downarrow x iff y <= x )
proof end;

theorem Th18: :: WAYBEL_0:18
for L being non empty RelStr
for x, y being Element of L holds
( y in uparrow x iff x <= y )
proof end;

theorem :: WAYBEL_0:19
for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st downarrow x = downarrow y holds
x = y
proof end;

theorem :: WAYBEL_0:20
for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st uparrow x = uparrow y holds
x = y
proof end;

theorem Th21: :: WAYBEL_0:21
for L being non empty transitive RelStr
for x, y being Element of L st x <= y holds
downarrow x c= downarrow y
proof end;

theorem Th22: :: WAYBEL_0:22
for L being non empty transitive RelStr
for x, y being Element of L st x <= y holds
uparrow y c= uparrow x
proof end;

registration
let L be non empty reflexive RelStr ;
let x be Element of L;
coherence
( not downarrow x is empty & downarrow x is directed )
proof end;
cluster uparrow x -> non empty filtered ;
coherence
( not uparrow x is empty & uparrow x is filtered )
proof end;
end;

definition
let L be RelStr ;
let X be Subset of L;
attr X is lower means :Def19: :: WAYBEL_0:def 19
for x, y being Element of L st x in X & y <= x holds
y in X;
attr X is upper means :Def20: :: WAYBEL_0:def 20
for x, y being Element of L st x in X & x <= y holds
y in X;
end;

:: deftheorem Def19 defines lower WAYBEL_0:def 19 :
for L being RelStr
for X being Subset of L holds
( X is lower iff for x, y being Element of L st x in X & y <= x holds
y in X );

:: deftheorem Def20 defines upper WAYBEL_0:def 20 :
for L being RelStr
for X being Subset of L holds
( X is upper iff for x, y being Element of L st x in X & x <= y holds
y in X );

registration
let L be RelStr ;
cluster lower upper for Element of K10( the carrier of L);
existence
ex b1 being Subset of L st
( b1 is lower & b1 is upper )
proof end;
end;

theorem Th23: :: WAYBEL_0:23
for L being RelStr
for X being Subset of L holds
( X is lower iff downarrow X c= X )
proof end;

theorem Th24: :: WAYBEL_0:24
for L being RelStr
for X being Subset of L holds
( X is upper iff uparrow X c= X )
proof end;

theorem :: WAYBEL_0:25
for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 holds
( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) )
proof end;

theorem :: WAYBEL_0:26
for L being RelStr
for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is lower ) holds
union A is lower Subset of L
proof end;

theorem Th27: :: WAYBEL_0:27
for L being RelStr
for X, Y being Subset of L st X is lower & Y is lower holds
( X /\ Y is lower & X \/ Y is lower )
proof end;

theorem :: WAYBEL_0:28
for L being RelStr
for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is upper ) holds
union A is upper Subset of L
proof end;

theorem Th29: :: WAYBEL_0:29
for L being RelStr
for X, Y being Subset of L st X is upper & Y is upper holds
( X /\ Y is upper & X \/ Y is upper )
proof end;

registration
let L be non empty transitive RelStr ;
let X be Subset of L;
coherence
proof end;
coherence
uparrow X is upper
proof end;
end;

registration
let L be non empty transitive RelStr ;
let x be Element of L;
coherence ;
coherence
uparrow x is upper
;
end;

registration
let L be non empty RelStr ;
coherence
( [#] L is lower & [#] L is upper )
proof end;
end;

registration
let L be non empty RelStr ;
cluster non empty lower upper for Element of K10( the carrier of L);
existence
ex b1 being Subset of L st
( not b1 is empty & b1 is lower & b1 is upper )
proof end;
end;

registration
let L be non empty reflexive transitive RelStr ;
cluster non empty directed lower for Element of K10( the carrier of L);
existence
ex b1 being Subset of L st
( not b1 is empty & b1 is lower & b1 is directed )
proof end;
cluster non empty filtered upper for Element of K10( the carrier of L);
existence
ex b1 being Subset of L st
( not b1 is empty & b1 is upper & b1 is filtered )
proof end;
end;

registration
let L be with_suprema with_infima Poset;
cluster non empty directed filtered lower upper for Element of K10( the carrier of L);
existence
ex b1 being Subset of L st
( not b1 is empty & b1 is directed & b1 is filtered & b1 is lower & b1 is upper )
proof end;
end;

theorem Th30: :: WAYBEL_0:30
for L being non empty reflexive transitive RelStr
for X being Subset of L holds
( X is directed iff downarrow X is directed )
proof end;

registration
let L be non empty reflexive transitive RelStr ;
let X be directed Subset of L;
coherence by Th30;
end;

theorem Th31: :: WAYBEL_0:31
for L being non empty reflexive transitive RelStr
for X being Subset of L
for x being Element of L holds
( x is_>=_than X iff x is_>=_than downarrow X )
proof end;

theorem Th32: :: WAYBEL_0:32
for L being non empty reflexive transitive RelStr
for X being Subset of L holds
( ex_sup_of X,L iff ex_sup_of downarrow X,L )
proof end;

theorem Th33: :: WAYBEL_0:33
for L being non empty reflexive transitive RelStr
for X being Subset of L st ex_sup_of X,L holds
sup X = sup ()
proof end;

theorem :: WAYBEL_0:34
for L being non empty Poset
for x being Element of L holds
( ex_sup_of downarrow x,L & sup () = x )
proof end;

theorem Th35: :: WAYBEL_0:35
for L being non empty reflexive transitive RelStr
for X being Subset of L holds
( X is filtered iff uparrow X is filtered )
proof end;

registration
let L be non empty reflexive transitive RelStr ;
let X be filtered Subset of L;
coherence by Th35;
end;

theorem Th36: :: WAYBEL_0:36
for L being non empty reflexive transitive RelStr
for X being Subset of L
for x being Element of L holds
( x is_<=_than X iff x is_<=_than uparrow X )
proof end;

theorem Th37: :: WAYBEL_0:37
for L being non empty reflexive transitive RelStr
for X being Subset of L holds
( ex_inf_of X,L iff ex_inf_of uparrow X,L )
proof end;

theorem Th38: :: WAYBEL_0:38
for L being non empty reflexive transitive RelStr
for X being Subset of L st ex_inf_of X,L holds
inf X = inf ()
proof end;

theorem :: WAYBEL_0:39
for L being non empty Poset
for x being Element of L holds
( ex_inf_of uparrow x,L & inf () = x )
proof end;

begin

definition end;

theorem Th40: :: WAYBEL_0:40
for L being antisymmetric with_suprema RelStr
for X being lower Subset of L holds
( X is directed iff for x, y being Element of L st x in X & y in X holds
x "\/" y in X )
proof end;

theorem Th41: :: WAYBEL_0:41
for L being antisymmetric with_infima RelStr
for X being upper Subset of L holds
( X is filtered iff for x, y being Element of L st x in X & y in X holds
x "/\" y in X )
proof end;

theorem Th42: :: WAYBEL_0:42
for L being with_suprema Poset
for X being non empty lower Subset of L holds
( X is directed iff for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in X )
proof end;

theorem Th43: :: WAYBEL_0:43
for L being with_infima Poset
for X being non empty upper Subset of L holds
( X is filtered iff for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in X )
proof end;

theorem :: WAYBEL_0:44
for L being non empty antisymmetric RelStr st ( L is with_suprema or L is with_infima ) holds
for X, Y being Subset of L st X is lower & X is directed & Y is lower & Y is directed holds
X /\ Y is directed
proof end;

theorem :: WAYBEL_0:45
for L being non empty antisymmetric RelStr st ( L is with_suprema or L is with_infima ) holds
for X, Y being Subset of L st X is upper & X is filtered & Y is upper & Y is filtered holds
X /\ Y is filtered
proof end;

theorem :: WAYBEL_0:46
for L being RelStr
for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is directed ) & ( for X, Y being Subset of L st X in A & Y in A holds
ex Z being Subset of L st
( Z in A & X \/ Y c= Z ) ) holds
for X being Subset of L st X = union A holds
X is directed
proof end;

theorem :: WAYBEL_0:47
for L being RelStr
for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is filtered ) & ( for X, Y being Subset of L st X in A & Y in A holds
ex Z being Subset of L st
( Z in A & X \/ Y c= Z ) ) holds
for X being Subset of L st X = union A holds
X is filtered
proof end;

definition
let L be non empty reflexive transitive RelStr ;
let I be Ideal of L;
attr I is principal means :: WAYBEL_0:def 21
ex x being Element of L st
( x in I & x is_>=_than I );
end;

:: deftheorem defines principal WAYBEL_0:def 21 :
for L being non empty reflexive transitive RelStr
for I being Ideal of L holds
( I is principal iff ex x being Element of L st
( x in I & x is_>=_than I ) );

definition
let L be non empty reflexive transitive RelStr ;
let F be Filter of L;
attr F is principal means :: WAYBEL_0:def 22
ex x being Element of L st
( x in F & x is_<=_than F );
end;

:: deftheorem defines principal WAYBEL_0:def 22 :
for L being non empty reflexive transitive RelStr
for F being Filter of L holds
( F is principal iff ex x being Element of L st
( x in F & x is_<=_than F ) );

theorem :: WAYBEL_0:48
for L being non empty reflexive transitive RelStr
for I being Ideal of L holds
( I is principal iff ex x being Element of L st I = downarrow x )
proof end;

theorem :: WAYBEL_0:49
for L being non empty reflexive transitive RelStr
for F being Filter of L holds
( F is principal iff ex x being Element of L st F = uparrow x )
proof end;

definition
let L be non empty reflexive transitive RelStr ;
func Ids L -> set equals :: WAYBEL_0:def 23
{ X where X is Ideal of L : verum } ;
correctness
coherence
{ X where X is Ideal of L : verum } is set
;
;
func Filt L -> set equals :: WAYBEL_0:def 24
{ X where X is Filter of L : verum } ;
correctness
coherence
{ X where X is Filter of L : verum } is set
;
;
end;

:: deftheorem defines Ids WAYBEL_0:def 23 :
for L being non empty reflexive transitive RelStr holds Ids L = { X where X is Ideal of L : verum } ;

:: deftheorem defines Filt WAYBEL_0:def 24 :
for L being non empty reflexive transitive RelStr holds Filt L = { X where X is Filter of L : verum } ;

definition
let L be non empty reflexive transitive RelStr ;
func Ids_0 L -> set equals :: WAYBEL_0:def 25
(Ids L) \/ ;
correctness
coherence
(Ids L) \/ is set
;
;
func Filt_0 L -> set equals :: WAYBEL_0:def 26
(Filt L) \/ ;
correctness
coherence
(Filt L) \/ is set
;
;
end;

:: deftheorem defines Ids_0 WAYBEL_0:def 25 :
for L being non empty reflexive transitive RelStr holds Ids_0 L = (Ids L) \/ ;

:: deftheorem defines Filt_0 WAYBEL_0:def 26 :
for L being non empty reflexive transitive RelStr holds Filt_0 L = (Filt L) \/ ;

definition
let L be non empty RelStr ;
let X be Subset of L;
set D = { ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } ;
A1: { ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } c= the carrier of L
proof end;
func finsups X -> Subset of L equals :: WAYBEL_0:def 27
{ ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } ;
correctness
coherence
{ ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } is Subset of L
;
by A1;
set D = { ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } ;
A2: { ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } c= the carrier of L
proof end;
func fininfs X -> Subset of L equals :: WAYBEL_0:def 28
{ ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } ;
correctness
coherence
{ ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } is Subset of L
;
by A2;
end;

:: deftheorem defines finsups WAYBEL_0:def 27 :
for L being non empty RelStr
for X being Subset of L holds finsups X = { ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } ;

:: deftheorem defines fininfs WAYBEL_0:def 28 :
for L being non empty RelStr
for X being Subset of L holds fininfs X = { ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } ;

registration
let L be non empty antisymmetric lower-bounded RelStr ;
let X be Subset of L;
cluster finsups X -> non empty ;
coherence
not finsups X is empty
proof end;
end;

registration
let L be non empty antisymmetric upper-bounded RelStr ;
let X be Subset of L;
cluster fininfs X -> non empty ;
coherence
not fininfs X is empty
proof end;
end;

registration
let L be non empty reflexive antisymmetric RelStr ;
let X be non empty Subset of L;
cluster finsups X -> non empty ;
coherence
not finsups X is empty
proof end;
cluster fininfs X -> non empty ;
coherence
not fininfs X is empty
proof end;
end;

theorem Th50: :: WAYBEL_0:50
for L being non empty reflexive antisymmetric RelStr
for X being Subset of L holds
( X c= finsups X & X c= fininfs X )
proof end;

theorem Th51: :: WAYBEL_0:51
for L being non empty transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) holds
F is directed
proof end;

registration
let L be with_suprema Poset;
let X be Subset of L;
coherence
proof end;
end;

theorem Th52: :: WAYBEL_0:52
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) holds
for x being Element of L holds
( x is_>=_than X iff x is_>=_than F )
proof end;

theorem Th53: :: WAYBEL_0:53
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) holds
( ex_sup_of X,L iff ex_sup_of F,L )
proof end;

theorem Th54: :: WAYBEL_0:54
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) & ex_sup_of X,L holds
sup F = sup X
proof end;

theorem :: WAYBEL_0:55
for L being with_suprema Poset
for X being Subset of L st ( ex_sup_of X,L or L is complete ) holds
sup X = sup ()
proof end;

theorem Th56: :: WAYBEL_0:56
for L being non empty transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ) holds
F is filtered
proof end;

registration
let L be with_infima Poset;
let X be Subset of L;
coherence
proof end;
end;

theorem Th57: :: WAYBEL_0:57
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ) holds
for x being Element of L holds
( x is_<=_than X iff x is_<=_than F )
proof end;

theorem Th58: :: WAYBEL_0:58
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ) holds
( ex_inf_of X,L iff ex_inf_of F,L )
proof end;

theorem Th59: :: WAYBEL_0:59
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ) & ex_inf_of X,L holds
inf F = inf X
proof end;

theorem :: WAYBEL_0:60
for L being with_infima Poset
for X being Subset of L st ( ex_inf_of X,L or L is complete ) holds
inf X = inf ()
proof end;

theorem :: WAYBEL_0:61
for L being with_suprema Poset
for X being Subset of L holds
( X c= downarrow () & ( for I being Ideal of L st X c= I holds
downarrow () c= I ) )
proof end;

theorem :: WAYBEL_0:62
for L being with_infima Poset
for X being Subset of L holds
( X c= uparrow () & ( for F being Filter of L st X c= F holds
uparrow () c= F ) )
proof end;

begin

definition
let L be non empty RelStr ;
attr L is connected means :Def29: :: WAYBEL_0:def 29
for x, y being Element of L holds
( x <= y or y <= x );
end;

:: deftheorem Def29 defines connected WAYBEL_0:def 29 :
for L being non empty RelStr holds
( L is connected iff for x, y being Element of L holds
( x <= y or y <= x ) );

registration
coherence
for b1 being non empty reflexive RelStr st b1 is trivial holds
b1 is connected
proof end;
end;

registration
existence
ex b1 being non empty Poset st b1 is connected
proof end;
end;

definition end;

registration
let L be Chain;
coherence
L ~ is connected
proof end;
end;

begin

definition end;

theorem :: WAYBEL_0:63
for L being Semilattice
for X being non empty upper Subset of L holds
( X is Filter of L iff subrelstr X is meet-inheriting )
proof end;

theorem :: WAYBEL_0:64
for L being sup-Semilattice
for X being non empty lower Subset of L holds
( X is Ideal of L iff subrelstr X is join-inheriting )
proof end;

begin

definition
let S, T be non empty RelStr ;
let f be Function of S,T;
let X be Subset of S;
pred f preserves_inf_of X means :Def30: :: WAYBEL_0:def 30
( ex_inf_of X,S implies ( ex_inf_of f .: X,T & inf (f .: X) = f . (inf X) ) );
pred f preserves_sup_of X means :Def31: :: WAYBEL_0:def 31
( ex_sup_of X,S implies ( ex_sup_of f .: X,T & sup (f .: X) = f . (sup X) ) );
end;

:: deftheorem Def30 defines preserves_inf_of WAYBEL_0:def 30 :
for S, T being non empty RelStr
for f being Function of S,T
for X being Subset of S holds
( f preserves_inf_of X iff ( ex_inf_of X,S implies ( ex_inf_of f .: X,T & inf (f .: X) = f . (inf X) ) ) );

:: deftheorem Def31 defines preserves_sup_of WAYBEL_0:def 31 :
for S, T being non empty RelStr
for f being Function of S,T
for X being Subset of S holds
( f preserves_sup_of X iff ( ex_sup_of X,S implies ( ex_sup_of f .: X,T & sup (f .: X) = f . (sup X) ) ) );

theorem :: WAYBEL_0:65
for S1, S2, T1, T2 being non empty RelStr st RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of T1, the InternalRel of T1 #) & RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) holds
for f being Function of S1,S2
for g being Function of T1,T2 st f = g holds
for X being Subset of S1
for Y being Subset of T1 st X = Y holds
( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) )
proof end;

definition
let L1, L2 be non empty RelStr ;
let f be Function of L1,L2;
attr f is infs-preserving means :: WAYBEL_0:def 32
for X being Subset of L1 holds f preserves_inf_of X;
attr f is sups-preserving means :: WAYBEL_0:def 33
for X being Subset of L1 holds f preserves_sup_of X;
attr f is meet-preserving means :: WAYBEL_0:def 34
for x, y being Element of L1 holds f preserves_inf_of {x,y};
attr f is join-preserving means :: WAYBEL_0:def 35
for x, y being Element of L1 holds f preserves_sup_of {x,y};
attr f is filtered-infs-preserving means :: WAYBEL_0:def 36
for X being Subset of L1 st not X is empty & X is filtered holds
f preserves_inf_of X;
attr f is directed-sups-preserving means :: WAYBEL_0:def 37
for X being Subset of L1 st not X is empty & X is directed holds
f preserves_sup_of X;
end;

:: deftheorem defines infs-preserving WAYBEL_0:def 32 :
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is infs-preserving iff for X being Subset of L1 holds f preserves_inf_of X );

:: deftheorem defines sups-preserving WAYBEL_0:def 33 :
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is sups-preserving iff for X being Subset of L1 holds f preserves_sup_of X );

:: deftheorem defines meet-preserving WAYBEL_0:def 34 :
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is meet-preserving iff for x, y being Element of L1 holds f preserves_inf_of {x,y} );

:: deftheorem defines join-preserving WAYBEL_0:def 35 :
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is join-preserving iff for x, y being Element of L1 holds f preserves_sup_of {x,y} );

:: deftheorem defines filtered-infs-preserving WAYBEL_0:def 36 :
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is filtered-infs-preserving iff for X being Subset of L1 st not X is empty & X is filtered holds
f preserves_inf_of X );

:: deftheorem defines directed-sups-preserving WAYBEL_0:def 37 :
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is directed-sups-preserving iff for X being Subset of L1 st not X is empty & X is directed holds
f preserves_sup_of X );

registration
let L1, L2 be non empty RelStr ;
cluster Function-like V21( the carrier of L1, the carrier of L2) infs-preserving -> meet-preserving filtered-infs-preserving for Element of K10(K11( the carrier of L1, the carrier of L2));
coherence
for b1 being Function of L1,L2 st b1 is infs-preserving holds
( b1 is filtered-infs-preserving & b1 is meet-preserving )
proof end;
cluster Function-like V21( the carrier of L1, the carrier of L2) sups-preserving -> join-preserving directed-sups-preserving for Element of K10(K11( the carrier of L1, the carrier of L2));
coherence
for b1 being Function of L1,L2 st b1 is sups-preserving holds
( b1 is directed-sups-preserving & b1 is join-preserving )
proof end;
end;

definition
let S, T be RelStr ;
let f be Function of S,T;
attr f is isomorphic means :Def38: :: WAYBEL_0:def 38
( f is one-to-one & f is monotone & ex g being Function of T,S st
( g = f " & g is monotone ) ) if ( not S is empty & not T is empty )
otherwise ( S is empty & T is empty );
correctness
consistency
verum
;
;
end;

:: deftheorem Def38 defines isomorphic WAYBEL_0:def 38 :
for S, T being RelStr
for f being Function of S,T holds
( ( not S is empty & not T is empty implies ( f is isomorphic iff ( f is one-to-one & f is monotone & ex g being Function of T,S st
( g = f " & g is monotone ) ) ) ) & ( ( S is empty or T is empty ) implies ( f is isomorphic iff ( S is empty & T is empty ) ) ) );

theorem Th66: :: WAYBEL_0:66
for S, T being non empty RelStr
for f being Function of S,T holds
( f is isomorphic iff ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds
( x <= y iff f . x <= f . y ) ) ) )
proof end;

registration
let S, T be non empty RelStr ;
cluster Function-like V21( the carrier of S, the carrier of T) isomorphic -> one-to-one monotone for Element of K10(K11( the carrier of S, the carrier of T));
coherence
for b1 being Function of S,T st b1 is isomorphic holds
( b1 is one-to-one & b1 is monotone )
by Def38;
end;

theorem :: WAYBEL_0:67
for S, T being non empty RelStr
for f being Function of S,T st f is isomorphic holds
( f " is Function of T,S & rng (f ") = the carrier of S )
proof end;

theorem :: WAYBEL_0:68
for S, T being non empty RelStr
for f being Function of S,T st f is isomorphic holds
for g being Function of T,S st g = f " holds
g is isomorphic
proof end;

theorem Th69: :: WAYBEL_0:69
for S, T being non empty Poset
for f being Function of S,T st ( for X being Filter of S holds f preserves_inf_of X ) holds
f is monotone
proof end;

theorem :: WAYBEL_0:70
for S, T being non empty Poset
for f being Function of S,T st ( for X being Filter of S holds f preserves_inf_of X ) holds
f is filtered-infs-preserving
proof end;

theorem :: WAYBEL_0:71
for S being Semilattice
for T being non empty Poset
for f being Function of S,T st ( for X being finite Subset of S holds f preserves_inf_of X ) & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) holds
f is infs-preserving
proof end;

theorem Th72: :: WAYBEL_0:72
for S, T being non empty Poset
for f being Function of S,T st ( for X being Ideal of S holds f preserves_sup_of X ) holds
f is monotone
proof end;

theorem :: WAYBEL_0:73
for S, T being non empty Poset
for f being Function of S,T st ( for X being Ideal of S holds f preserves_sup_of X ) holds
f is directed-sups-preserving
proof end;

theorem :: WAYBEL_0:74
for S being sup-Semilattice
for T being non empty Poset
for f being Function of S,T st ( for X being finite Subset of S holds f preserves_sup_of X ) & ( for X being non empty directed Subset of S holds f preserves_sup_of X ) holds
f is sups-preserving
proof end;

begin

definition
let L be non empty reflexive RelStr ;
attr L is up-complete means :Def39: :: WAYBEL_0:def 39
for X being non empty directed Subset of L ex x being Element of L st
( x is_>=_than X & ( for y being Element of L st y is_>=_than X holds
x <= y ) );
end;

:: deftheorem Def39 defines up-complete WAYBEL_0:def 39 :
for L being non empty reflexive RelStr holds
( L is up-complete iff for X being non empty directed Subset of L ex x being Element of L st
( x is_>=_than X & ( for y being Element of L st y is_>=_than X holds
x <= y ) ) );

registration
coherence
for b1 being reflexive with_suprema RelStr st b1 is up-complete holds
b1 is upper-bounded
proof end;
end;

theorem :: WAYBEL_0:75
for L being non empty reflexive antisymmetric RelStr holds
( L is up-complete iff for X being non empty directed Subset of L holds ex_sup_of X,L )
proof end;

definition
let L be non empty reflexive RelStr ;
attr L is /\-complete means :Def40: :: WAYBEL_0:def 40
for X being non empty Subset of L ex x being Element of L st
( x is_<=_than X & ( for y being Element of L st y is_<=_than X holds
x >= y ) );
end;

:: deftheorem Def40 defines /\-complete WAYBEL_0:def 40 :
for L being non empty reflexive RelStr holds
( L is /\-complete iff for X being non empty Subset of L ex x being Element of L st
( x is_<=_than X & ( for y being Element of L st y is_<=_than X holds
x >= y ) ) );

theorem Th76: :: WAYBEL_0:76
for L being non empty reflexive antisymmetric RelStr holds
( L is /\-complete iff for X being non empty Subset of L holds ex_inf_of X,L )
proof end;

registration
coherence
for b1 being non empty reflexive RelStr st b1 is complete holds
( b1 is up-complete & b1 is /\-complete )
proof end;
coherence
for b1 being non empty reflexive RelStr st b1 is /\-complete holds
b1 is lower-bounded
proof end;
coherence
for b1 being non empty Poset st b1 is up-complete & b1 is with_suprema & b1 is lower-bounded holds
b1 is complete
proof end;
end;

registration
coherence
for b1 being non empty reflexive antisymmetric RelStr st b1 is /\-complete holds
b1 is with_infima
proof end;
end;

registration
coherence
for b1 being non empty reflexive antisymmetric upper-bounded RelStr st b1 is /\-complete holds
b1 is with_suprema
proof end;
end;

registration
existence
ex b1 being LATTICE st
( b1 is complete & b1 is strict )
proof end;
end;