:: Properties of Relational Structures, Posets, Lattices and Maps
:: by Mariusz \.Zynel and Czes{\l}aw Byli\'nski
::
:: Received September 20, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users

theorem :: YELLOW_2:1

for L being non empty RelStr
for x being Element of L
for X being Subset of L holds
( X c= downarrow x iff X is_<=_than x ) by WAYBEL_0:17;

theorem :: YELLOW_2:2

for L being non empty RelStr
for x being Element of L
for X being Subset of L holds
( X c= uparrow x iff x is_<=_than X ) by WAYBEL_0:18;

theorem :: YELLOW_2:3

for L being transitive antisymmetric with_suprema RelStr
for X, Y being set st ex_sup_of X,L & ex_sup_of Y,L holds
( ex_sup_of X \/ Y,L & "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) )

proof end;

theorem :: YELLOW_2:4

for L being transitive antisymmetric with_infima RelStr
for X, Y being set st ex_inf_of X,L & ex_inf_of Y,L holds
( ex_inf_of X \/ Y,L & "/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L)) )

proof end;

theorem Th5: :: YELLOW_2:5

for R being Relation
for X, Y being set st X c= Y holds
R |_2 X c= R |_2 Y

proof end;

theorem :: YELLOW_2:6

for L being RelStr
for S, T being full SubRelStr of L st the carrier of S c= the carrier of T holds
the InternalRel of S c= the InternalRel of T

proof end;

theorem Th7: :: YELLOW_2:7

for X being set
for L being non empty RelStr
for S being non empty SubRelStr of L holds
( ( X is directed Subset of S implies X is directed Subset of L ) & ( X is filtered Subset of S implies X is filtered Subset of L ) )

proof end;

theorem :: YELLOW_2:8

for L being non empty RelStr
for S, T being non empty full SubRelStr of L st the carrier of S c= the carrier of T holds
for X being Subset of S holds
( X is Subset of T & ( for Y being Subset of T st X = Y holds
( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) ) ) )

proof end;

definition

let J be set ;
let L be RelStr ;
let f, g be Function of J, the carrier of L;

pred f <= g means :: YELLOW_2:def 1
for j being set st j in J holds
ex a, b being Element of L st
( a = f . j & b = g . j & a <= b );

end;

:: deftheorem defines <= YELLOW_2:def 1 :
for J being set
for L being RelStr
for f, g being Function of J, the carrier of L holds
( f <= g iff for j being set st j in J holds
ex a, b being Element of L st
( a = f . j & b = g . j & a <= b ) );

notation

let J be set ;
let L be RelStr ;
let f, g be Function of J, the carrier of L;
synonym g >= f for f <= g;

end;

theorem :: YELLOW_2:9

for L, M being non empty RelStr
for f, g being Function of L,M holds
( f <= g iff for x being Element of L holds f . x <= g . x )

proof end;

definition

let L, M be non empty RelStr ;
let f be Function of L,M;

func Image f -> strict full SubRelStr of M equals :: YELLOW_2:def 2
subrelstr (rng f);

correctness
coherence
subrelstr (rng f) is strict full SubRelStr of M;
;

end;

:: deftheorem defines Image YELLOW_2:def 2 :
for L, M being non empty RelStr
for f being Function of L,M holds Image f = subrelstr (rng f);

theorem :: YELLOW_2:10

for L, M being non empty RelStr
for f being Function of L,M
for y being Element of (Image f) ex x being Element of L st f . x = y

proof end;

registration

let L be non empty RelStr ;
let X be non empty Subset of L;

cluster subrelstr X -> non empty ;

coherence
not subrelstr X is empty by YELLOW_0:def 15;

end;

registration

let L, M be non empty RelStr ;
let f be Function of L,M;

cluster Image f -> non empty strict full ;

coherence
not Image f is empty

proof end;

end;

theorem :: YELLOW_2:11

for L being non empty RelStr holds id L is monotone

proof end;

theorem :: YELLOW_2:12

for L, M, N being non empty RelStr
for f being Function of L,M
for g being Function of M,N st f is monotone & g is monotone holds
g * f is monotone

proof end;

theorem :: YELLOW_2:13

for L, M being non empty RelStr
for f being Function of L,M
for X being Subset of L
for x being Element of L st f is monotone & x is_<=_than X holds
f . x is_<=_than f .: X

proof end;

theorem :: YELLOW_2:14

for L, M being non empty RelStr
for f being Function of L,M
for X being Subset of L
for x being Element of L st f is monotone & X is_<=_than x holds
f .: X is_<=_than f . x

proof end;

theorem :: YELLOW_2:15

for S, T being non empty RelStr
for f being Function of S,T
for X being directed Subset of S st f is monotone holds
f .: X is directed

proof end;

theorem Th16: :: YELLOW_2:16

for L being with_suprema Poset
for f being Function of L,L st f is directed-sups-preserving holds
f is monotone

proof end;

theorem :: YELLOW_2:17

for L being with_infima Poset
for f being Function of L,L st f is filtered-infs-preserving holds
f is monotone

proof end;

theorem :: YELLOW_2:18

for S being non empty 1-sorted
for f being Function of S,S st f is idempotent holds
for x being Element of S holds f . (f . x) = f . x

proof end;

theorem Th19: :: YELLOW_2:19

for S being non empty 1-sorted
for f being Function of S,S st f is idempotent holds
rng f = { x where x is Element of S : x = f . x }

proof end;

theorem Th20: :: YELLOW_2:20

for X being set
for S being non empty 1-sorted
for f being Function of S,S st f is idempotent & X c= rng f holds
f .: X = X

proof end;

theorem :: YELLOW_2:21

for L being non empty RelStr holds id L is idempotent

proof end;

theorem Th22: :: YELLOW_2:22

for X being set
for L being complete LATTICE
for a being Element of L st a in X holds
( a <= "\/" (X,L) & "/\" (X,L) <= a )

proof end;

theorem Th23: :: YELLOW_2:23

for L being non empty RelStr holds
( ( for X being set holds ex_sup_of X,L ) iff for Y being set holds ex_inf_of Y,L )

proof end;

theorem Th24: :: YELLOW_2:24

for L being non empty RelStr st ( for X being set holds ex_sup_of X,L ) holds
L is complete

proof end;

theorem Th25: :: YELLOW_2:25

for L being non empty RelStr st ( for X being set holds ex_inf_of X,L ) holds
L is complete

proof end;

theorem Th26: :: YELLOW_2:26

for L being non empty RelStr st ( for A being Subset of L holds ex_inf_of A,L ) holds
for X being set holds
( ex_inf_of X,L & "/\" (X,L) = "/\" ((X /\ the carrier of L),L) )

proof end;

theorem :: YELLOW_2:27

for L being non empty RelStr st ( for A being Subset of L holds ex_sup_of A,L ) holds
for X being set holds
( ex_sup_of X,L & "\/" (X,L) = "\/" ((X /\ the carrier of L),L) )

proof end;

theorem Th28: :: YELLOW_2:28

for L being non empty RelStr st ( for A being Subset of L holds ex_inf_of A,L ) holds
L is complete

proof end;

registration

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

correctness
coherence
for b₁ being non empty Poset st b₁ is up-complete & b₁ is /\-complete & b₁ is upper-bounded holds
b₁ is complete ;
;

end;

theorem Th29: :: YELLOW_2:29

for L being complete LATTICE
for f being Function of L,L st f is monotone holds
for M being Subset of L st M = { x where x is Element of L : x = f . x } holds
subrelstr M is complete LATTICE

proof end;

theorem Th30: :: YELLOW_2:30

for L being complete LATTICE
for S being non empty full infs-inheriting SubRelStr of L holds S is complete LATTICE

proof end;

theorem Th31: :: YELLOW_2:31

for L being complete LATTICE
for S being non empty full sups-inheriting SubRelStr of L holds S is complete LATTICE

proof end;

theorem Th32: :: YELLOW_2:32

for L being complete LATTICE
for M being non empty RelStr
for f being Function of L,M st f is sups-preserving holds
Image f is sups-inheriting

proof end;

theorem Th33: :: YELLOW_2:33

for L being complete LATTICE
for M being non empty RelStr
for f being Function of L,M st f is infs-preserving holds
Image f is infs-inheriting

proof end;

theorem :: YELLOW_2:34

for L, M being complete LATTICE
for f being Function of L,M st ( f is sups-preserving or f is infs-preserving ) holds
Image f is complete LATTICE

proof end;

theorem :: YELLOW_2:35

for L being complete LATTICE
for f being Function of L,L st f is idempotent & f is directed-sups-preserving holds
( Image f is directed-sups-inheriting & Image f is complete LATTICE )

proof end;

theorem Th36: :: YELLOW_2:36

for L being RelStr
for F being Subset-Family of L st ( for X being Subset of L st X in F holds
X is lower ) holds
meet F is lower Subset of L

proof end;

theorem :: YELLOW_2:37

for L being RelStr
for F being Subset-Family of L st ( for X being Subset of L st X in F holds
X is upper ) holds
meet F is upper Subset of L

proof end;

theorem Th38: :: YELLOW_2:38

for L being antisymmetric with_suprema RelStr
for F being Subset-Family of L st ( for X being Subset of L st X in F holds
( X is lower & X is directed ) ) holds
meet F is directed Subset of L

proof end;

theorem :: YELLOW_2:39

for L being antisymmetric with_infima RelStr
for F being Subset-Family of L st ( for X being Subset of L st X in F holds
( X is upper & X is filtered ) ) holds
meet F is filtered Subset of L

proof end;

theorem Th40: :: YELLOW_2:40

for L being with_infima Poset
for I, J being Ideal of L holds I /\ J is Ideal of L

proof end;

registration

let L be non empty reflexive transitive RelStr ;

cluster Ids L -> non empty ;

correctness
coherence
not Ids L is empty ;

proof end;

end;

theorem Th41: :: YELLOW_2:41

for x being set
for L being non empty reflexive transitive RelStr holds
( x is Element of (InclPoset (Ids L)) iff x is Ideal of L )

proof end;

theorem Th42: :: YELLOW_2:42

for x being set
for L being non empty reflexive transitive RelStr
for I being Element of (InclPoset (Ids L)) st x in I holds
x is Element of L

proof end;

theorem :: YELLOW_2:43

for L being with_infima Poset
for x, y being Element of (InclPoset (Ids L)) holds x "/\" y = x /\ y

proof end;

registration

let L be with_infima Poset;

cluster InclPoset (Ids L) -> with_infima ;

correctness
coherence
InclPoset (Ids L) is with_infima ;

proof end;

end;

theorem Th44: :: YELLOW_2:44

for L being with_suprema Poset
for x, y being Element of (InclPoset (Ids L)) ex Z being Subset of L st
( Z = { z where z is Element of L : ( z in x or z in y or ex a, b being Element of L st
( a in x & b in y & z = a "\/" b ) ) } & ex_sup_of {x,y}, InclPoset (Ids L) & x "\/" y = downarrow Z )

proof end;

registration

let L be with_suprema Poset;

cluster InclPoset (Ids L) -> with_suprema ;

correctness
coherence
InclPoset (Ids L) is with_suprema ;

proof end;

end;

theorem Th45: :: YELLOW_2:45

for L being lower-bounded sup-Semilattice
for X being non empty Subset of (Ids L) holds meet X is Ideal of L

proof end;

theorem Th46: :: YELLOW_2:46

for L being lower-bounded sup-Semilattice
for A being non empty Subset of (InclPoset (Ids L)) holds
( ex_inf_of A, InclPoset (Ids L) & inf A = meet A )

proof end;

theorem Th47: :: YELLOW_2:47

for L being with_suprema Poset holds
( ex_inf_of {} , InclPoset (Ids L) & "/\" ({},(InclPoset (Ids L))) = [#] L )

proof end;

theorem Th48: :: YELLOW_2:48

for L being lower-bounded sup-Semilattice holds InclPoset (Ids L) is complete

proof end;

registration

let L be lower-bounded sup-Semilattice;

cluster InclPoset (Ids L) -> complete ;

correctness
coherence
InclPoset (Ids L) is complete ;
by Th48;

end;

definition

let L be non empty Poset;

func SupMap L -> Function of (InclPoset (Ids L)),L means :Def3: :: YELLOW_2:def 3
for I being Ideal of L holds it . I = sup I;

existence
ex b₁ being Function of (InclPoset (Ids L)),L st
for I being Ideal of L holds b₁ . I = sup I

proof end;

uniqueness
for b₁, b₂ being Function of (InclPoset (Ids L)),L st ( for I being Ideal of L holds b₁ . I = sup I ) & ( for I being Ideal of L holds b₂ . I = sup I ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines SupMap YELLOW_2:def 3 :
for L being non empty Poset
for b₂ being Function of (InclPoset (Ids L)),L holds
( b₂ = SupMap L iff for I being Ideal of L holds b₂ . I = sup I );

theorem Th49: :: YELLOW_2:49

for L being non empty Poset holds
( dom (SupMap L) = Ids L & rng (SupMap L) is Subset of L )

proof end;

theorem :: YELLOW_2:50

for x being set
for L being non empty Poset holds
( x in dom (SupMap L) iff x is Ideal of L )

proof end;

theorem Th51: :: YELLOW_2:51

for L being non empty up-complete Poset holds SupMap L is monotone

proof end;

registration

let L be non empty up-complete Poset;

cluster SupMap L -> monotone ;

correctness
coherence
SupMap L is monotone ;
by Th51;

end;

definition

let L be non empty Poset;

func IdsMap L -> Function of L,(InclPoset (Ids L)) means :Def4: :: YELLOW_2:def 4
for x being Element of L holds it . x = downarrow x;

existence
ex b₁ being Function of L,(InclPoset (Ids L)) st
for x being Element of L holds b₁ . x = downarrow x

proof end;

uniqueness
for b₁, b₂ being Function of L,(InclPoset (Ids L)) st ( for x being Element of L holds b₁ . x = downarrow x ) & ( for x being Element of L holds b₂ . x = downarrow x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines IdsMap YELLOW_2:def 4 :
for L being non empty Poset
for b₂ being Function of L,(InclPoset (Ids L)) holds
( b₂ = IdsMap L iff for x being Element of L holds b₂ . x = downarrow x );

theorem Th52: :: YELLOW_2:52

for L being non empty Poset holds IdsMap L is monotone

proof end;

registration

let L be non empty Poset;

cluster IdsMap L -> monotone ;

correctness
coherence
IdsMap L is monotone ;
by Th52;

end;

definition

let L be non empty RelStr ;
let F be Relation;

func \\/ (F,L) -> Element of L equals :: YELLOW_2:def 5
"\/" ((rng F),L);

coherence
"\/" ((rng F),L) is Element of L ;

func //\ (F,L) -> Element of L equals :: YELLOW_2:def 6
"/\" ((rng F),L);

coherence
"/\" ((rng F),L) is Element of L ;

end;

:: deftheorem defines \\/ YELLOW_2:def 5 :
for L being non empty RelStr
for F being Relation holds \\/ (F,L) = "\/" ((rng F),L);

:: deftheorem defines //\ YELLOW_2:def 6 :
for L being non empty RelStr
for F being Relation holds //\ (F,L) = "/\" ((rng F),L);

notation

let J be set ;
let L be non empty RelStr ;
let F be Function of J, the carrier of L;
synonym Sup F for \\/ (L,J);
synonym Inf F for //\ (L,J);

end;

theorem :: YELLOW_2:53

for L being complete LATTICE
for J being non empty set
for j being Element of J
for F being Function of J, the carrier of L holds
( F . j <= Sup & Inf <= F . j )

proof end;

theorem :: YELLOW_2:54

for L being complete LATTICE
for a being Element of L
for J being non empty set
for F being Function of J, the carrier of L st ( for j being Element of J holds F . j <= a ) holds
Sup <= a

proof end;

theorem :: YELLOW_2:55

for L being complete LATTICE
for a being Element of L
for J being non empty set
for F being Function of J, the carrier of L st ( for j being Element of J holds a <= F . j ) holds
a <= Inf

proof end;