WAYBEL_0: Directed Sets, Nets, Ideals, Filters, and Maps

:: Directed Sets, Nets, Ideals, Filters, and Maps
:: by Grzegorz Bancerek
::
:: Received September 12, 1996
:: Copyright (c) 1996-2011 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 :

:: deftheorem Def2 defines filtered WAYBEL_0:def 2 :

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;

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 Element of K10( the carrier of L);
coherence

proof end;

end;

registration

let L be RelStr ;
cluster directed filtered Element of K10( the carrier of L);
existence

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

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 Element of K10( the carrier of L);
existence

proof end;

end;

registration

let L be with_suprema RelStr ;
cluster [#] L -> directed ;
coherence

proof end;

end;

registration

let L be non empty upper-bounded RelStr ;
cluster [#] L -> directed ;
coherence

proof end;

end;

registration

let L be with_infima RelStr ;
cluster [#] L -> filtered ;
coherence

proof end;

end;

registration

let L be non empty lower-bounded RelStr ;
cluster [#] L -> filtered ;
coherence

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 :

:: deftheorem Def4 defines directed-sups-inheriting WAYBEL_0:def 4 :

registration

let L be non empty RelStr ;
cluster infs-inheriting -> filtered-infs-inheriting SubRelStr of L;
coherence

proof end;

cluster sups-inheriting -> directed-sups-inheriting SubRelStr of L;
coherence

proof end;

end;

registration

let L be non empty RelStr ;
cluster non empty strict full infs-inheriting sups-inheriting SubRelStr of L;
existence

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 :

definition

let L be 1-sorted ;
attr c₂ is strict ;
struct NetStr of L -> RelStr ;
aggr NetStr(# carrier, InternalRel, mapping #) -> NetStr of L;
sel mapping c₂ -> Function of the carrier of c₂, 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 ;

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 :

registration

let L be 1-sorted ;
cluster non empty reflexive transitive antisymmetric strict directed NetStr of L;
existence

proof end;

end;

definition

let L be 1-sorted ;
mode prenet of L is non empty directed NetStr of 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 of L;
func netmap (N,L) -> Function of N,L equals :: WAYBEL_0:def 7
the mapping of N;
coherence ;
let i be Element of N;
func N . i -> Element of L equals :: WAYBEL_0:def 8
the mapping of N . i;
correctness ;

end;

:: deftheorem defines netmap WAYBEL_0:def 7 :

:: deftheorem defines . WAYBEL_0:def 8 :

definition

let L be non empty RelStr ;
let N be non empty NetStr of 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 :

:: deftheorem defines antitone WAYBEL_0:def 10 :

definition

let L be non empty 1-sorted ;
let N be non empty NetStr of 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 :

:: deftheorem defines is_often_in WAYBEL_0:def 12 :

theorem :: WAYBEL_0:8

for L being non empty 1-sorted
for N being non empty NetStr of 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 of 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 of 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₁() -> non empty RelStr , F₂() -> non empty NetStr of F₁(), P₁[ set ] } :

( F₂() is_eventually_in { (F₂() . k) where k is Element of F₂() : P₁[F₂() . k] } iff ex i being Element of F₂() st
for j being Element of F₂() st i <= j holds
P₁[F₂() . j] )

proof end;

definition

let L be non empty RelStr ;
let N be non empty NetStr of 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 :

:: deftheorem Def14 defines eventually-filtered WAYBEL_0:def 14 :

theorem Th11: :: WAYBEL_0:11

for L being non empty RelStr
for N being non empty NetStr of 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 of 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 NetStr of L;
coherence

proof end;

cluster non empty directed antitone -> eventually-filtered NetStr of L;
coherence

proof end;

end;

registration

let L be non empty reflexive RelStr ;
cluster non empty strict directed monotone antitone NetStr of L;
existence

proof end;

end;

begin

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

proof end;

uniqueness

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

proof end;

correctness

proof end;

end;

:: deftheorem Def15 defines downarrow WAYBEL_0:def 15 :

:: deftheorem Def16 defines uparrow WAYBEL_0:def 16 :

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

proof end;

cluster uparrow X -> non empty ;
coherence

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 ;
func uparrow x -> Subset of L equals :: WAYBEL_0:def 18
uparrow {x};
correctness ;

end;

:: deftheorem defines downarrow WAYBEL_0:def 17 :

:: deftheorem defines uparrow WAYBEL_0:def 18 :

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;
cluster downarrow x -> non empty directed ;
coherence

proof end;

cluster uparrow x -> non empty filtered ;
coherence

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 :

:: deftheorem Def20 defines upper WAYBEL_0:def 20 :

registration

let L be RelStr ;
cluster lower upper Element of K10( the carrier of L);
existence

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

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;
cluster downarrow X -> lower ;
coherence

proof end;

cluster uparrow X -> upper ;
coherence

proof end;

end;

registration

let L be non empty transitive RelStr ;
let x be Element of L;
cluster downarrow x -> lower ;
coherence ;
cluster uparrow x -> upper ;
coherence ;

end;

registration

let L be non empty RelStr ;
cluster [#] L -> lower upper ;
coherence

proof end;

end;

registration

let L be non empty RelStr ;
cluster non empty lower upper Element of K10( the carrier of L);
existence

proof end;

end;

registration

let L be non empty reflexive transitive RelStr ;
cluster non empty directed lower Element of K10( the carrier of L);
existence

proof end;

cluster non empty filtered upper Element of K10( the carrier of L);
existence

proof end;

end;

registration

let L be with_suprema with_infima Poset;
cluster non empty directed filtered lower upper Element of K10( the carrier of L);
existence

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

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

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;

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 :

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 :

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 ;
func Filt L -> set equals :: WAYBEL_0:def 24
{ X where X is Filter of L : verum } ;
correctness ;

end;

:: deftheorem defines Ids WAYBEL_0:def 23 :

:: deftheorem defines Filt WAYBEL_0:def 24 :

definition

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

end;

:: deftheorem defines Ids_0 WAYBEL_0:def 25 :

:: deftheorem defines Filt_0 WAYBEL_0:def 26 :

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 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 by A2;

end;

:: deftheorem defines finsups WAYBEL_0:def 27 :

:: deftheorem defines fininfs WAYBEL_0:def 28 :

registration

let L be non empty antisymmetric lower-bounded RelStr ;
let X be Subset of L;
cluster finsups X -> non empty ;
coherence

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

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

proof end;

cluster fininfs X -> non empty ;
coherence

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;
cluster finsups X -> directed ;
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

proof end;

theorem Th54: :: WAYBEL_0:54

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)

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;
cluster fininfs X -> filtered ;
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

proof end;

theorem Th59: :: WAYBEL_0:59

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)

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

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

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 :

registration

cluster non empty trivial reflexive -> non empty reflexive connected RelStr ;
coherence

proof end;

end;

registration

cluster non empty V51() reflexive transitive antisymmetric connected RelStr ;
existence

proof end;

end;

definition

mode Chain is non empty connected Poset;

end;

registration

let L be Chain;
cluster L ~ -> connected ;
coherence

proof end;

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;

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 :

:: deftheorem Def31 defines preserves_sup_of WAYBEL_0:def 31 :

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 :

:: deftheorem defines sups-preserving WAYBEL_0:def 33 :

:: deftheorem defines meet-preserving WAYBEL_0:def 34 :

:: deftheorem defines join-preserving WAYBEL_0:def 35 :

:: deftheorem defines filtered-infs-preserving WAYBEL_0:def 36 :

:: deftheorem defines directed-sups-preserving WAYBEL_0:def 37 :

registration

let L1, L2 be non empty RelStr ;
cluster Function-like V18( the carrier of L1, the carrier of L2) infs-preserving -> meet-preserving filtered-infs-preserving Element of K10(K11( the carrier of L1, the carrier of L2));
coherence

proof end;

cluster Function-like V18( the carrier of L1, the carrier of L2) sups-preserving -> join-preserving directed-sups-preserving Element of K10(K11( the carrier of L1, the carrier of L2));
coherence

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 ;

end;

:: deftheorem Def38 defines isomorphic WAYBEL_0:def 38 :

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 V18( the carrier of S, the carrier of T) isomorphic -> one-to-one monotone Element of K10(K11( the carrier of S, the carrier of T));
coherence 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 :

registration

cluster reflexive with_suprema up-complete -> reflexive with_suprema upper-bounded RelStr ;
coherence

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;