:: by Mariusz \.Zynel and Czes{\l}aw Byli\'nski

::

:: Received September 20, 1996

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

begin

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 )

for x being Element of L

for X being Subset of L holds

( X c= downarrow x iff X is_<=_than x )

proof end;

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 )

for x being Element of L

for X being Subset of L holds

( X c= uparrow x iff x is_<=_than X )

proof end;

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

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

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;

begin

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

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

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

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;

begin

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

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;
let L be RelStr ;

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

synonym g >= f for f <= g;

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 )

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;

begin

definition

let L, M be non empty RelStr ;

let f be Function of L,M;

correctness

coherence

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

;

end;
let f be Function of L,M;

correctness

coherence

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

;

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

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

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;

coherence

not subrelstr X is empty by YELLOW_0:def 15;

end;
let X be non empty Subset of L;

coherence

not subrelstr X is empty by YELLOW_0:def 15;

registration
end;

begin

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

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

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

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

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

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

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

f is monotone

proof end;

begin

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

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 }

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

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;

begin

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 )

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 )

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

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

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

for X being set holds

( ex_sup_of X,L & "\/" (X,L) = "\/" ((X /\ the carrier of L),L) )

proof end;

registration

coherence

for b_{1} being non empty Poset st b_{1} is up-complete & b_{1} is /\-complete & b_{1} is upper-bounded holds

b_{1} is complete ;

;

end;

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

correctness coherence

for b

b

;

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

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

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

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

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

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

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 )

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;

begin

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

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

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

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

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;

registration

let L be non empty reflexive transitive RelStr ;

correctness

coherence

not Ids L is empty ;

end;
correctness

coherence

not Ids L is empty ;

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

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

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;

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

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

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 )

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 )

( ex_inf_of {} , InclPoset (Ids L) & "/\" ({},(InclPoset (Ids L))) = [#] L )

proof end;

registration

let L be lower-bounded sup-Semilattice;

correctness

coherence

InclPoset (Ids L) is complete ;

by Th48;

end;
correctness

coherence

InclPoset (Ids L) is complete ;

by Th48;

begin

definition

let L be non empty Poset;

ex b_{1} being Function of (InclPoset (Ids L)),L st

for I being Ideal of L holds b_{1} . I = sup I

for b_{1}, b_{2} being Function of (InclPoset (Ids L)),L st ( for I being Ideal of L holds b_{1} . I = sup I ) & ( for I being Ideal of L holds b_{2} . I = sup I ) holds

b_{1} = b_{2}

end;
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 for I being Ideal of L holds it . I = sup I;

ex b

for I being Ideal of L holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines SupMap YELLOW_2:def 3 :

for L being non empty Poset

for b_{2} being Function of (InclPoset (Ids L)),L holds

( b_{2} = SupMap L iff for I being Ideal of L holds b_{2} . I = sup I );

for L being non empty Poset

for b

( b

registration
end;

definition

let L be non empty Poset;

ex b_{1} being Function of L,(InclPoset (Ids L)) st

for x being Element of L holds b_{1} . x = downarrow x

for b_{1}, b_{2} being Function of L,(InclPoset (Ids L)) st ( for x being Element of L holds b_{1} . x = downarrow x ) & ( for x being Element of L holds b_{2} . x = downarrow x ) holds

b_{1} = b_{2}

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

ex b

for x being Element of L holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines IdsMap YELLOW_2:def 4 :

for L being non empty Poset

for b_{2} being Function of L,(InclPoset (Ids L)) holds

( b_{2} = IdsMap L iff for x being Element of L holds b_{2} . x = downarrow x );

for L being non empty Poset

for b

( b

begin

definition

let L be non empty RelStr ;

let F be Relation;

coherence

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

coherence

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

end;
let F be Relation;

coherence

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

coherence

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

:: deftheorem defines \\/ YELLOW_2:def 5 :

for L being non empty RelStr

for F being Relation holds \\/ (F,L) = "\/" ((rng F),L);

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

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

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 )

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

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

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;