:: by Grzegorz Bancerek

::

:: Received September 12, 1996

:: Copyright (c) 1996-2012 Association of Mizar Users

begin

definition

let L be RelStr ;

let X be Subset of L;

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

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

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

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

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

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.

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

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 ;

coherence

for b_{1} being Subset of L st b_{1} is empty holds

( b_{1} is directed & b_{1} is filtered )

end;
coherence

for b

( b

proof end;

registration

let L be RelStr ;

existence

ex b_{1} being Subset of L st

( b_{1} is directed & b_{1} is filtered )

end;
existence

ex b

( b

proof 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

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

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 )

for x being Element of L holds

( {x} is directed & {x} is filtered )

proof end;

registration

let L be non empty reflexive RelStr ;

existence

ex b_{1} being Subset of L st

( b_{1} is directed & b_{1} is filtered & not b_{1} is empty & b_{1} is finite )

end;
existence

ex b

( b

proof end;

registration
end;

registration
end;

definition

let L be non empty RelStr ;

let S be SubRelStr of L;

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

for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds

"/\" (X,L) in the carrier of S;

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

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

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 b_{1} being SubRelStr of L st b_{1} is infs-inheriting holds

b_{1} is filtered-infs-inheriting

for b_{1} being SubRelStr of L st b_{1} is sups-inheriting holds

b_{1} is directed-sups-inheriting

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

registration

let L be non empty RelStr ;

existence

ex b_{1} being SubRelStr of L st

( b_{1} is infs-inheriting & b_{1} is sups-inheriting & not b_{1} is empty & b_{1} is full & b_{1} is strict )

end;
existence

ex b

( b

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

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

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

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

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 c_{2} is strict ;

struct NetStr over L -> RelStr ;

aggr NetStr(# carrier, InternalRel, mapping #) -> NetStr over L;

sel mapping c_{2} -> Function of the carrier of c_{2}, the carrier of L;

end;
attr c

struct NetStr over L -> RelStr ;

aggr NetStr(# carrier, InternalRel, mapping #) -> NetStr over L;

sel mapping c

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;

coherence

not NetStr(# X,O,F #) is empty ;

end;
let X be non empty set ;

let O be Relation of X;

let F be Function of X, the carrier of L;

coherence

not NetStr(# X,O,F #) is empty ;

definition
end;

:: deftheorem Def6 defines directed WAYBEL_0:def 6 :

for N being RelStr holds

( N is directed iff [#] N is directed );

for N being RelStr holds

( N is directed iff [#] N is directed );

registration

let L be 1-sorted ;

existence

ex b_{1} being strict NetStr over L st

( not b_{1} is empty & b_{1} is reflexive & b_{1} is transitive & b_{1} is antisymmetric & b_{1} is directed )

end;
existence

ex b

( not b

proof end;

definition

let L be non empty 1-sorted ;

let N be non empty NetStr over L;

coherence

the mapping of N is Function of N,L ;

let i be Element of N;

correctness

coherence

the mapping of N . i is Element of L;

;

end;
let N be non empty NetStr over L;

coherence

the mapping of N is Function of N,L ;

let i be Element of N;

correctness

coherence

the mapping of N . i is Element of L;

;

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

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;

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;

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

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

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 ;

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

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

for i being Element of N ex j being Element of N st

( i <= j & N . j in X );

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

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

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

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 )

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 )

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{ F_{1}() -> non empty RelStr , F_{2}() -> non empty NetStr over F_{1}(), P_{1}[ set ] } :

HoldsEventually{ F

( F_{2}() is_eventually_in { (F_{2}() . k) where k is Element of F_{2}() : P_{1}[F_{2}() . k] } iff ex i being Element of F_{2}() st

for j being Element of F_{2}() st i <= j holds

P_{1}[F_{2}() . j] )

for j being Element of F

P

proof end;

definition

let L be non empty RelStr ;

let N be non empty NetStr over L;

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

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 } ;

for i being Element of N holds N is_eventually_in { (N . j) where j is Element of N : N . i >= N . j } ;

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

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

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 )

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 )

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 ;

coherence

for b_{1} being prenet of L st b_{1} is monotone holds

b_{1} is eventually-directed

for b_{1} being prenet of L st b_{1} is antitone holds

b_{1} is eventually-filtered

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

registration

let L be non empty reflexive RelStr ;

existence

ex b_{1} being prenet of L st

( b_{1} is monotone & b_{1} is antitone & b_{1} is strict )

end;
existence

ex b

( b

proof end;

begin

:: Definition 1.3

definition

let L be RelStr ;

let X be Subset of L;

ex b_{1} being Subset of L st

for x being Element of L holds

( x in b_{1} iff ex y being Element of L st

( y >= x & y in X ) )

for b_{1}, b_{2} being Subset of L st ( for x being Element of L holds

( x in b_{1} iff ex y being Element of L st

( y >= x & y in X ) ) ) & ( for x being Element of L holds

( x in b_{2} iff ex y being Element of L st

( y >= x & y in X ) ) ) holds

b_{1} = b_{2}

ex b_{1} being Subset of L st

for x being Element of L holds

( x in b_{1} iff ex y being Element of L st

( y <= x & y in X ) )

uniqueness

for b_{1}, b_{2} being Subset of L st ( for x being Element of L holds

( x in b_{1} iff ex y being Element of L st

( y <= x & y in X ) ) ) & ( for x being Element of L holds

( x in b_{2} iff ex y being Element of L st

( y <= x & y in X ) ) ) holds

b_{1} = b_{2};

end;
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 for x being Element of L holds

( x in it iff ex y being Element of L st

( y >= x & y in X ) );

ex b

for x being Element of L holds

( x in b

( y >= x & y in X ) )

proof end;

uniqueness for b

( x in b

( y >= x & y in X ) ) ) & ( for x being Element of L holds

( x in b

( y >= x & y in X ) ) ) holds

b

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 for x being Element of L holds

( x in it iff ex y being Element of L st

( y <= x & y in X ) );

ex b

for x being Element of L holds

( x in b

( y <= x & y in X ) )

proof end;

correctness uniqueness

for b

( x in b

( y <= x & y in X ) ) ) & ( for x being Element of L holds

( x in b

( y <= x & y in X ) ) ) holds

b

proof end;

:: deftheorem Def15 defines downarrow WAYBEL_0:def 15 :

for L being RelStr

for X, b_{3} being Subset of L holds

( b_{3} = downarrow X iff for x being Element of L holds

( x in b_{3} iff ex y being Element of L st

( y >= x & y in X ) ) );

for L being RelStr

for X, b

( b

( x in b

( y >= x & y in X ) ) );

:: deftheorem Def16 defines uparrow WAYBEL_0:def 16 :

for L being RelStr

for X, b_{3} being Subset of L holds

( b_{3} = uparrow X iff for x being Element of L holds

( x in b_{3} iff ex y being Element of L st

( y <= x & y in X ) ) );

for L being RelStr

for X, b

( b

( x in b

( 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 )

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 ) }

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 ) }

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;

coherence

not downarrow X is empty

not uparrow X is empty

end;
let X be non empty Subset of L;

coherence

not downarrow X is empty

proof end;

coherence not uparrow X is empty

proof end;

definition

let L be non empty RelStr ;

let x be Element of L;

correctness

coherence

downarrow {x} is Subset of L;

;

correctness

coherence

uparrow {x} is Subset of L;

;

end;
let x be Element of L;

correctness

coherence

downarrow {x} is Subset of L;

;

correctness

coherence

uparrow {x} is Subset of L;

;

:: deftheorem defines downarrow WAYBEL_0:def 17 :

for L being non empty RelStr

for x being Element of L holds downarrow x = downarrow {x};

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};

for L being non empty RelStr

for x being Element of L holds uparrow x = uparrow {x};

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

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

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

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

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 )

( not uparrow x is empty & uparrow x is filtered )

end;
let x be Element of L;

coherence

( not downarrow x is empty & downarrow x is directed )

proof end;

coherence ( not uparrow x is empty & uparrow x is filtered )

proof end;

definition

let L be RelStr ;

let X be Subset of L;

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

for x, y being Element of L st x in X & y <= x holds

y in X;

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

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

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 ;

existence

ex b_{1} being Subset of L st

( b_{1} is lower & b_{1} is upper )

end;
existence

ex b

( b

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

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

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 )

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

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 )

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

downarrow X is lower

uparrow X is upper

end;
let X be Subset of L;

coherence

downarrow X is lower

proof end;

coherence uparrow X is upper

proof end;

registration

let L be non empty transitive RelStr ;

let x be Element of L;

coherence

downarrow x is lower ;

coherence

uparrow x is upper ;

end;
let x be Element of L;

coherence

downarrow x is lower ;

coherence

uparrow x is upper ;

registration
end;

registration

let L be non empty RelStr ;

existence

ex b_{1} being Subset of L st

( not b_{1} is empty & b_{1} is lower & b_{1} is upper )

end;
existence

ex b

( not b

proof end;

registration

let L be non empty reflexive transitive RelStr ;

existence

ex b_{1} being Subset of L st

( not b_{1} is empty & b_{1} is lower & b_{1} is directed )

ex b_{1} being Subset of L st

( not b_{1} is empty & b_{1} is upper & b_{1} is filtered )

end;
existence

ex b

( not b

proof end;

existence ex b

( not b

proof end;

registration

let L be with_suprema with_infima Poset;

existence

ex b_{1} being Subset of L st

( not b_{1} is empty & b_{1} is directed & b_{1} is filtered & b_{1} is lower & b_{1} is upper )

end;
existence

ex b

( not b

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

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

downarrow X is directed by Th30;

end;
let X be directed Subset of L;

coherence

downarrow X is directed by Th30;

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 )

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 )

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 (downarrow X)

for X being Subset of L st ex_sup_of X,L holds

sup X = sup (downarrow X)

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 (downarrow x) = x )

for x being Element of L holds

( ex_sup_of downarrow x,L & sup (downarrow x) = 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 )

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

uparrow X is filtered by Th35;

end;
let X be filtered Subset of L;

coherence

uparrow X is filtered by Th35;

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 )

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 )

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 (uparrow X)

for X being Subset of L st ex_inf_of X,L holds

inf X = inf (uparrow X)

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 (uparrow x) = x )

for x being Element of L holds

( ex_inf_of uparrow x,L & inf (uparrow x) = x )

proof end;

begin

definition

let L be non empty reflexive transitive RelStr ;

mode Ideal of L is non empty directed lower Subset of L;

mode Filter of L is non empty filtered upper Subset of L;

end;
mode Ideal of L is non empty directed lower Subset of L;

mode Filter of L is non empty filtered upper Subset of L;

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 )

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 )

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 )

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 )

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

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

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

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

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;

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

ex x being Element of L st

( x in I & x is_>=_than I );

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

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;

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

ex x being Element of L st

( x in F & x is_<=_than F );

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

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 )

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 )

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 ;

correctness

coherence

{ X where X is Ideal of L : verum } is set ;

;

correctness

coherence

{ X where X is Filter of L : verum } is set ;

;

end;
correctness

coherence

{ X where X is Ideal of L : verum } is set ;

;

correctness

coherence

{ X where X is Filter of L : verum } is set ;

;

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

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 } ;

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 ;

correctness

coherence

(Ids L) \/ {{}} is set ;

;

correctness

coherence

(Filt L) \/ {{}} is set ;

;

end;
correctness

coherence

(Ids L) \/ {{}} is set ;

;

correctness

coherence

(Filt L) \/ {{}} is set ;

;

:: deftheorem defines Ids_0 WAYBEL_0:def 25 :

for L being non empty reflexive transitive RelStr holds Ids_0 L = (Ids L) \/ {{}};

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) \/ {{}};

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

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

coherence

{ ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } is Subset of L;

by A2;

end;
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 { ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } ;

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 { ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } ;

coherence

{ ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } is Subset of L;

by A2;

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

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 } ;

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;

coherence

not finsups X is empty

end;
let X be Subset of L;

coherence

not finsups X is empty

proof end;

registration

let L be non empty antisymmetric upper-bounded RelStr ;

let X be Subset of L;

coherence

not fininfs X is empty

end;
let X be Subset of L;

coherence

not fininfs X is empty

proof end;

registration

let L be non empty reflexive antisymmetric RelStr ;

let X be non empty Subset of L;

coherence

not finsups X is empty

not fininfs X is empty

end;
let X be non empty Subset of L;

coherence

not finsups X is empty

proof end;

coherence not fininfs X is empty

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

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

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

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 )

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

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 (finsups X)

for X being Subset of L st ( ex_sup_of X,L or L is complete ) holds

sup X = sup (finsups X)

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

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

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 )

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

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 (fininfs X)

for X being Subset of L st ( ex_inf_of X,L or L is complete ) holds

inf X = inf (fininfs X)

proof end;

theorem :: WAYBEL_0:61

for L being with_suprema Poset

for X being Subset of L holds

( X c= downarrow (finsups X) & ( for I being Ideal of L st X c= I holds

downarrow (finsups X) c= I ) )

for X being Subset of L holds

( X c= downarrow (finsups X) & ( for I being Ideal of L st X c= I holds

downarrow (finsups X) c= I ) )

proof end;

theorem :: WAYBEL_0:62

for L being with_infima Poset

for X being Subset of L holds

( X c= uparrow (fininfs X) & ( for F being Filter of L st X c= F holds

uparrow (fininfs X) c= F ) )

for X being Subset of L holds

( X c= uparrow (fininfs X) & ( for F being Filter of L st X c= F holds

uparrow (fininfs X) c= F ) )

proof end;

begin

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

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 b_{1} being non empty reflexive RelStr st b_{1} is trivial holds

b_{1} is connected

end;
for b

b

proof end;

begin

definition

mode Semilattice is with_infima Poset;

mode sup-Semilattice is with_suprema Poset;

mode LATTICE is with_suprema with_infima Poset;

end;
mode sup-Semilattice is with_suprema Poset;

mode LATTICE is with_suprema with_infima Poset;

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 )

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 )

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;

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

( ex_inf_of X,S implies ( ex_inf_of f .: X,T & inf (f .: X) = f . (inf X) ) );

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

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

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

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;

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

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;

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};

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};

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;

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;

for X being Subset of L1 st not X is empty & X is directed holds

f preserves_sup_of X;

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

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

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

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

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

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

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 ;

for b_{1} being Function of L1,L2 st b_{1} is infs-preserving holds

( b_{1} is filtered-infs-preserving & b_{1} is meet-preserving )

for b_{1} being Function of L1,L2 st b_{1} is sups-preserving holds

( b_{1} is directed-sups-preserving & b_{1} is join-preserving )

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

( b

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 b

( b

proof end;

definition

let S, T be RelStr ;

let f be Function of S,T;

consistency

verum;

;

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

consistency

verum;

;

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

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

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 ;

for b_{1} being Function of S,T st b_{1} is isomorphic holds

( b_{1} is one-to-one & b_{1} is monotone )
by Def38;

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

( b

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 )

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

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

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

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

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

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

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

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 ;

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

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

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

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 b_{1} being reflexive with_suprema RelStr st b_{1} is up-complete holds

b_{1} is upper-bounded

end;
for b

b

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

( 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 ;

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

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

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

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 )

( L is /\-complete iff for X being non empty Subset of L holds ex_inf_of X,L )

proof end;

registration

coherence

for b_{1} being non empty reflexive RelStr st b_{1} is complete holds

( b_{1} is up-complete & b_{1} is /\-complete )

for b_{1} being non empty reflexive RelStr st b_{1} is /\-complete holds

b_{1} is lower-bounded

for b_{1} being non empty Poset st b_{1} is up-complete & b_{1} is with_suprema & b_{1} is lower-bounded holds

b_{1} is complete

end;
for b

( b

proof end;

coherence for b

b

proof end;

cluster non empty reflexive transitive antisymmetric with_suprema lower-bounded up-complete -> non empty complete for RelStr ;

coherence for b

b

proof end;

registration

for b_{1} being non empty reflexive antisymmetric RelStr st b_{1} is /\-complete holds

b_{1} is with_infima
end;

cluster non empty reflexive antisymmetric /\-complete -> non empty reflexive antisymmetric with_infima for RelStr ;

coherence for b

b

proof end;

registration

for b_{1} being non empty reflexive antisymmetric upper-bounded RelStr st b_{1} is /\-complete holds

b_{1} is with_suprema
end;

cluster non empty reflexive antisymmetric upper-bounded /\-complete -> non empty reflexive antisymmetric with_suprema upper-bounded for RelStr ;

coherence for b

b

proof end;

registration

ex b_{1} being LATTICE st

( b_{1} is complete & b_{1} is strict )
end;

cluster non empty strict V58() reflexive transitive antisymmetric with_suprema with_infima complete for RelStr ;

existence ex b

( b

proof end;

:: in our terminology. It is shown bellow.