:: Auxiliary and Approximating Relations
:: by Adam Grabowski
::
:: Received October 21, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users

definition

let L be non empty reflexive RelStr ;

func L -waybelow -> Relation of L means :Def1: :: WAYBEL_4:def 1
for x, y being Element of L holds
( [x,y] in it iff x << y );

existence
ex b₁ being Relation of L st
for x, y being Element of L holds
( [x,y] in b₁ iff x << y )

proof end;

uniqueness
for b₁, b₂ being Relation of L st ( for x, y being Element of L holds
( [x,y] in b₁ iff x << y ) ) & ( for x, y being Element of L holds
( [x,y] in b₂ iff x << y ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines -waybelow WAYBEL_4:def 1 :
for L being non empty reflexive RelStr
for b₂ being Relation of L holds
( b₂ = L -waybelow iff for x, y being Element of L holds
( [x,y] in b₂ iff x << y ) );

definition

let L be RelStr ;

func IntRel L -> Relation of L equals :: WAYBEL_4:def 2
the InternalRel of L;

coherence
the InternalRel of L is Relation of L ;
correctness
;

end;

:: deftheorem defines IntRel WAYBEL_4:def 2 :
for L being RelStr holds IntRel L = the InternalRel of L;

definition

let L be RelStr ;
let R be Relation of L;

attr R is auxiliary(i) means :Def3: :: WAYBEL_4:def 3
for x, y being Element of L st [x,y] in R holds
x <= y;

attr R is auxiliary(ii) means :Def4: :: WAYBEL_4:def 4
for x, y, z, u being Element of L st u <= x & [x,y] in R & y <= z holds
[u,z] in R;

end;

:: deftheorem Def3 defines auxiliary(i) WAYBEL_4:def 3 :
for L being RelStr
for R being Relation of L holds
( R is auxiliary(i) iff for x, y being Element of L st [x,y] in R holds
x <= y );

:: deftheorem Def4 defines auxiliary(ii) WAYBEL_4:def 4 :
for L being RelStr
for R being Relation of L holds
( R is auxiliary(ii) iff for x, y, z, u being Element of L st u <= x & [x,y] in R & y <= z holds
[u,z] in R );

definition

let L be non empty RelStr ;
let R be Relation of L;

attr R is auxiliary(iii) means :Def5: :: WAYBEL_4:def 5
for x, y, z being Element of L st [x,z] in R & [y,z] in R holds
[(x "\/" y),z] in R;

attr R is auxiliary(iv) means :Def6: :: WAYBEL_4:def 6
for x being Element of L holds [(Bottom L),x] in R;

end;

:: deftheorem Def5 defines auxiliary(iii) WAYBEL_4:def 5 :
for L being non empty RelStr
for R being Relation of L holds
( R is auxiliary(iii) iff for x, y, z being Element of L st [x,z] in R & [y,z] in R holds
[(x "\/" y),z] in R );

:: deftheorem Def6 defines auxiliary(iv) WAYBEL_4:def 6 :
for L being non empty RelStr
for R being Relation of L holds
( R is auxiliary(iv) iff for x being Element of L holds [(Bottom L),x] in R );

:: Definition 1.9 p.43

definition

let L be non empty RelStr ;
let R be Relation of L;

attr R is auxiliary means :: WAYBEL_4:def 7
( R is auxiliary(i) & R is auxiliary(ii) & R is auxiliary(iii) & R is auxiliary(iv) );

end;

:: deftheorem defines auxiliary WAYBEL_4:def 7 :
for L being non empty RelStr
for R being Relation of L holds
( R is auxiliary iff ( R is auxiliary(i) & R is auxiliary(ii) & R is auxiliary(iii) & R is auxiliary(iv) ) );

registration

let L be non empty RelStr ;

cluster auxiliary -> auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) for Element of bool [: the carrier of L, the carrier of L:];

coherence
for b₁ being Relation of L st b₁ is auxiliary holds
( b₁ is auxiliary(i) & b₁ is auxiliary(ii) & b₁ is auxiliary(iii) & b₁ is auxiliary(iv) ) ;

cluster auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) -> auxiliary for Element of bool [: the carrier of L, the carrier of L:];

coherence
for b₁ being Relation of L st b₁ is auxiliary(i) & b₁ is auxiliary(ii) & b₁ is auxiliary(iii) & b₁ is auxiliary(iv) holds
b₁ is auxiliary ;

end;

registration

let L be transitive antisymmetric lower-bounded with_suprema RelStr ;

cluster Relation-like auxiliary for Element of bool [: the carrier of L, the carrier of L:];

existence
ex b₁ being Relation of L st b₁ is auxiliary

proof end;

end;

theorem Th1: :: WAYBEL_4:1

for L being lower-bounded sup-Semilattice
for AR being auxiliary(ii) auxiliary(iii) Relation of L
for x, y, z, u being Element of L st [x,z] in AR & [y,u] in AR holds
[(x "\/" y),(z "\/" u)] in AR

proof end;

Lm1: for L being lower-bounded sup-Semilattice
for AR being auxiliary(i) auxiliary(ii) Relation of L holds AR is transitive

proof end;

registration

let L be lower-bounded sup-Semilattice;

cluster auxiliary(i) auxiliary(ii) -> transitive for Element of bool [: the carrier of L, the carrier of L:];

coherence
for b₁ being Relation of L st b₁ is auxiliary(i) & b₁ is auxiliary(ii) holds
b₁ is transitive by Lm1;

end;

registration

let L be RelStr ;

cluster IntRel L -> auxiliary(i) ;

coherence
IntRel L is auxiliary(i) by ORDERS_2:def 5;

end;

registration

let L be transitive RelStr ;

cluster IntRel L -> auxiliary(ii) ;

coherence
IntRel L is auxiliary(ii)

proof end;

end;

registration

let L be antisymmetric with_suprema RelStr ;

cluster IntRel L -> auxiliary(iii) ;

coherence
IntRel L is auxiliary(iii)

proof end;

end;

registration

let L be non empty antisymmetric lower-bounded RelStr ;

cluster IntRel L -> auxiliary(iv) ;

coherence
IntRel L is auxiliary(iv) by YELLOW_0:44, ORDERS_2:def 5;

end;

definition

let L be lower-bounded sup-Semilattice;

func Aux L -> set means :Def8: :: WAYBEL_4:def 8
for a being set holds
( a in it iff a is auxiliary Relation of L );

existence
ex b₁ being set st
for a being set holds
( a in b₁ iff a is auxiliary Relation of L )

proof end;

uniqueness
for b₁, b₂ being set st ( for a being set holds
( a in b₁ iff a is auxiliary Relation of L ) ) & ( for a being set holds
( a in b₂ iff a is auxiliary Relation of L ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines Aux WAYBEL_4:def 8 :
for L being lower-bounded sup-Semilattice
for b₂ being set holds
( b₂ = Aux L iff for a being set holds
( a in b₂ iff a is auxiliary Relation of L ) );

registration

let L be lower-bounded sup-Semilattice;

cluster Aux L -> non empty ;

coherence
not Aux L is empty

proof end;

end;

Lm2: for L being lower-bounded sup-Semilattice
for AR being auxiliary(i) Relation of L
for a, b being object st [a,b] in AR holds
[a,b] in IntRel L

proof end;

theorem Th2: :: WAYBEL_4:2

for L being lower-bounded sup-Semilattice
for AR being auxiliary(i) Relation of L holds AR c= IntRel L by Lm2;

theorem :: WAYBEL_4:3

for L being lower-bounded sup-Semilattice holds Top (InclPoset (Aux L)) = IntRel L

proof end;

registration

let L be lower-bounded sup-Semilattice;

cluster InclPoset (Aux L) -> upper-bounded ;

coherence
InclPoset (Aux L) is upper-bounded

proof end;

end;

definition

let L be non empty RelStr ;

func AuxBottom L -> Relation of L means :Def9: :: WAYBEL_4:def 9
for x, y being Element of L holds
( [x,y] in it iff x = Bottom L );

existence
ex b₁ being Relation of L st
for x, y being Element of L holds
( [x,y] in b₁ iff x = Bottom L )

proof end;

uniqueness
for b₁, b₂ being Relation of L st ( for x, y being Element of L holds
( [x,y] in b₁ iff x = Bottom L ) ) & ( for x, y being Element of L holds
( [x,y] in b₂ iff x = Bottom L ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines AuxBottom WAYBEL_4:def 9 :
for L being non empty RelStr
for b₂ being Relation of L holds
( b₂ = AuxBottom L iff for x, y being Element of L holds
( [x,y] in b₂ iff x = Bottom L ) );

registration

let L be lower-bounded sup-Semilattice;

cluster AuxBottom L -> auxiliary ;

coherence
AuxBottom L is auxiliary

proof end;

end;

theorem Th4: :: WAYBEL_4:4

for L being lower-bounded sup-Semilattice
for AR being auxiliary(iv) Relation of L holds AuxBottom L c= AR

proof end;

theorem :: WAYBEL_4:5

for L being lower-bounded sup-Semilattice holds Bottom (InclPoset (Aux L)) = AuxBottom L

proof end;

registration

let L be lower-bounded sup-Semilattice;

cluster InclPoset (Aux L) -> lower-bounded ;

coherence
InclPoset (Aux L) is lower-bounded

proof end;

end;

theorem Th6: :: WAYBEL_4:6

for L being lower-bounded sup-Semilattice
for a, b being auxiliary(i) Relation of L holds a /\ b is auxiliary(i) Relation of L

proof end;

theorem Th7: :: WAYBEL_4:7

for L being lower-bounded sup-Semilattice
for a, b being auxiliary(ii) Relation of L holds a /\ b is auxiliary(ii) Relation of L

proof end;

theorem Th8: :: WAYBEL_4:8

for L being lower-bounded sup-Semilattice
for a, b being auxiliary(iii) Relation of L holds a /\ b is auxiliary(iii) Relation of L

proof end;

theorem Th9: :: WAYBEL_4:9

for L being lower-bounded sup-Semilattice
for a, b being auxiliary(iv) Relation of L holds a /\ b is auxiliary(iv) Relation of L

proof end;

theorem Th10: :: WAYBEL_4:10

for L being lower-bounded sup-Semilattice
for a, b being auxiliary Relation of L holds a /\ b is auxiliary Relation of L

proof end;

theorem Th11: :: WAYBEL_4:11

for L being lower-bounded sup-Semilattice
for X being non empty Subset of (InclPoset (Aux L)) holds meet X is auxiliary Relation of L

proof end;

registration

let L be lower-bounded sup-Semilattice;

cluster InclPoset (Aux L) -> with_infima ;

coherence
InclPoset (Aux L) is with_infima

proof end;

end;

registration

let L be lower-bounded sup-Semilattice;

cluster InclPoset (Aux L) -> complete ;

coherence
InclPoset (Aux L) is complete

proof end;

end;

definition

let L be non empty RelStr ;
let x be Element of L;
let AR be Relation of the carrier of L;
A1: { y where y is Element of L : [y,x] in AR } c= the carrier of L

proof end;

func AR -below x -> Subset of L equals :: WAYBEL_4:def 10
{ y where y is Element of L : [y,x] in AR } ;

correctness
coherence
{ y where y is Element of L : [y,x] in AR } is Subset of L;
by A1;
A2: { y where y is Element of L : [x,y] in AR } c= the carrier of L

proof end;

func AR -above x -> Subset of L equals :: WAYBEL_4:def 11
{ y where y is Element of L : [x,y] in AR } ;

correctness
coherence
{ y where y is Element of L : [x,y] in AR } is Subset of L;
by A2;

end;

:: deftheorem defines -below WAYBEL_4:def 10 :
for L being non empty RelStr
for x being Element of L
for AR being Relation of the carrier of L holds AR -below x = { y where y is Element of L : [y,x] in AR } ;

:: deftheorem defines -above WAYBEL_4:def 11 :
for L being non empty RelStr
for x being Element of L
for AR being Relation of the carrier of L holds AR -above x = { y where y is Element of L : [x,y] in AR } ;

theorem Th12: :: WAYBEL_4:12

for L being lower-bounded sup-Semilattice
for x being Element of L
for AR being auxiliary(i) Relation of L holds AR -below x c= downarrow x

proof end;

registration

let L be lower-bounded sup-Semilattice;
let x be Element of L;
let AR be auxiliary(iv) Relation of L;

cluster AR -below x -> non empty ;

coherence
not AR -below x is empty

proof end;

end;

registration

let L be lower-bounded sup-Semilattice;
let x be Element of L;
let AR be auxiliary(ii) Relation of L;

cluster AR -below x -> lower ;

coherence
AR -below x is lower

proof end;

end;

registration

let L be lower-bounded sup-Semilattice;
let x be Element of L;
let AR be auxiliary(iii) Relation of L;

cluster AR -below x -> directed ;

coherence
AR -below x is directed

proof end;

end;

definition

let L be lower-bounded sup-Semilattice;
let AR be auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L;

func AR -below -> Function of L,(InclPoset (Ids L)) means :Def12: :: WAYBEL_4:def 12
for x being Element of L holds it . x = AR -below x;

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

proof end;

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

proof end;

end;

:: deftheorem Def12 defines -below WAYBEL_4:def 12 :
for L being lower-bounded sup-Semilattice
for AR being auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L
for b₃ being Function of L,(InclPoset (Ids L)) holds
( b₃ = AR -below iff for x being Element of L holds b₃ . x = AR -below x );

theorem Th13: :: WAYBEL_4:13

for L being non empty RelStr
for AR being Relation of L
for a being object
for y being Element of L holds
( a in AR -below y iff [a,y] in AR )

proof end;

theorem :: WAYBEL_4:14

for a being set
for L being sup-Semilattice
for AR being Relation of L
for y being Element of L holds
( a in AR -above y iff [y,a] in AR )

proof end;

Lm3: for L being lower-bounded with_suprema Poset
for AR being Relation of L
for a being set
for y being Element of L holds
( a in downarrow y iff [a,y] in the InternalRel of L )

proof end;

theorem :: WAYBEL_4:15

for L being lower-bounded sup-Semilattice
for AR being auxiliary(i) Relation of L
for x being Element of L st AR = the InternalRel of L holds
AR -below x = downarrow x

proof end;

definition

let L be non empty Poset;

func MonSet L -> strict RelStr means :Def13: :: WAYBEL_4:def 13
for a being set holds
( ( a in the carrier of it implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of it ) & ( for c, d being object holds
( [c,d] in the InternalRel of it iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of it & d in the carrier of it & f <= g ) ) ) );

existence
ex b₁ being strict RelStr st
for a being set holds
( ( a in the carrier of b₁ implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of b₁ ) & ( for c, d being object holds
( [c,d] in the InternalRel of b₁ iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of b₁ & d in the carrier of b₁ & f <= g ) ) ) )

proof end;

uniqueness
for b₁, b₂ being strict RelStr st ( for a being set holds
( ( a in the carrier of b₁ implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of b₁ ) & ( for c, d being object holds
( [c,d] in the InternalRel of b₁ iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of b₁ & d in the carrier of b₁ & f <= g ) ) ) ) ) & ( for a being set holds
( ( a in the carrier of b₂ implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of b₂ ) & ( for c, d being object holds
( [c,d] in the InternalRel of b₂ iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of b₂ & d in the carrier of b₂ & f <= g ) ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines MonSet WAYBEL_4:def 13 :
for L being non empty Poset
for b₂ being strict RelStr holds
( b₂ = MonSet L iff for a being set holds
( ( a in the carrier of b₂ implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of b₂ ) & ( for c, d being object holds
( [c,d] in the InternalRel of b₂ iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of b₂ & d in the carrier of b₂ & f <= g ) ) ) ) );

theorem :: WAYBEL_4:16

for L being lower-bounded sup-Semilattice holds MonSet L is full SubRelStr of (InclPoset (Ids L)) |^ the carrier of L

proof end;

theorem Th17: :: WAYBEL_4:17

for L being lower-bounded sup-Semilattice
for AR being auxiliary(ii) Relation of L
for x, y being Element of L st x <= y holds
AR -below x c= AR -below y

proof end;

registration

let L be lower-bounded sup-Semilattice;
let AR be auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L;

cluster AR -below -> monotone ;

coherence
AR -below is monotone

proof end;

end;

theorem Th18: :: WAYBEL_4:18

for L being lower-bounded sup-Semilattice
for AR being auxiliary Relation of L holds AR -below in the carrier of (MonSet L)

proof end;

registration

let L be lower-bounded sup-Semilattice;

cluster MonSet L -> non empty strict ;

coherence
not MonSet L is empty by Th18;

end;

theorem Th19: :: WAYBEL_4:19

for L being lower-bounded sup-Semilattice holds IdsMap L in the carrier of (MonSet L)

proof end;

theorem :: WAYBEL_4:20

for L being lower-bounded sup-Semilattice
for AR being auxiliary Relation of L holds AR -below <= IdsMap L

proof end;

theorem Th21: :: WAYBEL_4:21

for L being non empty lower-bounded Poset
for I being Ideal of L holds Bottom L in I

proof end;

theorem :: WAYBEL_4:22

for L being non empty upper-bounded Poset
for F being Filter of L holds Top L in F

proof end;

theorem Th23: :: WAYBEL_4:23

for L being non empty lower-bounded Poset holds downarrow (Bottom L) = {(Bottom L)}

proof end;

theorem :: WAYBEL_4:24

for L being non empty upper-bounded Poset holds uparrow (Top L) = {(Top L)}

proof end;

Lm4: for L being lower-bounded sup-Semilattice
for I being Ideal of L holds {(Bottom L)} c= I

proof end;

theorem Th25: :: WAYBEL_4:25

for L being lower-bounded sup-Semilattice holds the carrier of L --> {(Bottom L)} is Function of L,(InclPoset (Ids L))

proof end;

Lm5: for L being lower-bounded sup-Semilattice
for f being Function of L,(InclPoset (Ids L)) st f = the carrier of L --> {(Bottom L)} holds
f is monotone
by YELLOW_1:3;

theorem Th26: :: WAYBEL_4:26

for L being lower-bounded sup-Semilattice holds the carrier of L --> {(Bottom L)} in the carrier of (MonSet L)

proof end;

theorem :: WAYBEL_4:27

for L being lower-bounded sup-Semilattice
for AR being auxiliary Relation of L holds [( the carrier of L --> {(Bottom L)}),(AR -below)] in the InternalRel of (MonSet L)

proof end;

Lm6: for L being lower-bounded sup-Semilattice ex x being Element of (MonSet L) st x is_>=_than the carrier of (MonSet L)

proof end;

registration

let L be lower-bounded sup-Semilattice;

cluster MonSet L -> strict upper-bounded ;

coherence
MonSet L is upper-bounded by Lm6;

end;

definition

let L be lower-bounded sup-Semilattice;

func Rel2Map L -> Function of (InclPoset (Aux L)),(MonSet L) means :Def14: :: WAYBEL_4:def 14
for AR being auxiliary Relation of L holds it . AR = AR -below ;

existence
ex b₁ being Function of (InclPoset (Aux L)),(MonSet L) st
for AR being auxiliary Relation of L holds b₁ . AR = AR -below

proof end;

uniqueness
for b₁, b₂ being Function of (InclPoset (Aux L)),(MonSet L) st ( for AR being auxiliary Relation of L holds b₁ . AR = AR -below ) & ( for AR being auxiliary Relation of L holds b₂ . AR = AR -below ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines Rel2Map WAYBEL_4:def 14 :
for L being lower-bounded sup-Semilattice
for b₂ being Function of (InclPoset (Aux L)),(MonSet L) holds
( b₂ = Rel2Map L iff for AR being auxiliary Relation of L holds b₂ . AR = AR -below );

theorem :: WAYBEL_4:28

for L being lower-bounded sup-Semilattice
for R1, R2 being auxiliary Relation of L st R1 c= R2 holds
R1 -below <= R2 -below

proof end;

theorem Th29: :: WAYBEL_4:29

for L being lower-bounded sup-Semilattice
for x being Element of L
for R1, R2 being Relation of L st R1 c= R2 holds
R1 -below x c= R2 -below x

proof end;

Lm7: for L being lower-bounded sup-Semilattice holds Rel2Map L is monotone

proof end;

registration

let L be lower-bounded sup-Semilattice;

cluster Rel2Map L -> monotone ;

coherence
Rel2Map L is monotone by Lm7;

end;

definition

let L be lower-bounded sup-Semilattice;

func Map2Rel L -> Function of (MonSet L),(InclPoset (Aux L)) means :Def15: :: WAYBEL_4:def 15
for s being object st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = it . s & ( for x, y being object holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) );

existence
ex b₁ being Function of (MonSet L),(InclPoset (Aux L)) st
for s being object st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = b₁ . s & ( for x, y being object holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Function of (MonSet L),(InclPoset (Aux L)) st ( for s being object st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = b₁ . s & ( for x, y being object holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) ) & ( for s being object st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = b₂ . s & ( for x, y being object holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines Map2Rel WAYBEL_4:def 15 :
for L being lower-bounded sup-Semilattice
for b₂ being Function of (MonSet L),(InclPoset (Aux L)) holds
( b₂ = Map2Rel L iff for s being object st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = b₂ . s & ( for x, y being object holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) );

Lm8: for L being lower-bounded sup-Semilattice holds Map2Rel L is monotone

proof end;

registration

let L be lower-bounded sup-Semilattice;

cluster Map2Rel L -> monotone ;

coherence
Map2Rel L is monotone by Lm8;

end;

theorem Th30: :: WAYBEL_4:30

for L being lower-bounded sup-Semilattice holds (Map2Rel L) * (Rel2Map L) = id (dom (Rel2Map L))

proof end;

theorem Th31: :: WAYBEL_4:31

for L being lower-bounded sup-Semilattice holds (Rel2Map L) * (Map2Rel L) = id the carrier of (MonSet L)

proof end;

registration

let L be lower-bounded sup-Semilattice;

cluster Rel2Map L -> V16() ;

coherence
Rel2Map L is one-to-one

proof end;

end;

:: Proposition 1.10 (i) p.43

theorem Th32: :: WAYBEL_4:32

for L being lower-bounded sup-Semilattice holds (Rel2Map L) " = Map2Rel L

proof end;

:: Proposition 1.10 (ii) p.43

theorem :: WAYBEL_4:33

for L being lower-bounded sup-Semilattice holds Rel2Map L is isomorphic

proof end;

theorem Th34: :: WAYBEL_4:34

for L being complete LATTICE
for x being Element of L holds meet { I where I is Ideal of L : x <= sup I } = waybelow x

proof end;

definition

let L be Semilattice;
let I be Ideal of L;

func DownMap I -> Function of L,(InclPoset (Ids L)) means :Def16: :: WAYBEL_4:def 16
for x being Element of L holds
( ( x <= sup I implies it . x = (downarrow x) /\ I ) & ( not x <= sup I implies it . x = downarrow x ) );

existence
ex b₁ being Function of L,(InclPoset (Ids L)) st
for x being Element of L holds
( ( x <= sup I implies b₁ . x = (downarrow x) /\ I ) & ( not x <= sup I implies 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
( ( x <= sup I implies b₁ . x = (downarrow x) /\ I ) & ( not x <= sup I implies b₁ . x = downarrow x ) ) ) & ( for x being Element of L holds
( ( x <= sup I implies b₂ . x = (downarrow x) /\ I ) & ( not x <= sup I implies b₂ . x = downarrow x ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def16 defines DownMap WAYBEL_4:def 16 :
for L being Semilattice
for I being Ideal of L
for b₃ being Function of L,(InclPoset (Ids L)) holds
( b₃ = DownMap I iff for x being Element of L holds
( ( x <= sup I implies b₃ . x = (downarrow x) /\ I ) & ( not x <= sup I implies b₃ . x = downarrow x ) ) );

Lm9: for L being Semilattice
for I being Ideal of L holds DownMap I is monotone

proof end;

Lm10: for L being Semilattice
for x being Element of L
for I being Ideal of L holds (DownMap I) . x c= downarrow x

proof end;

theorem Th35: :: WAYBEL_4:35

for L being Semilattice
for I being Ideal of L holds DownMap I in the carrier of (MonSet L)

proof end;

theorem Th36: :: WAYBEL_4:36

for L being reflexive antisymmetric with_infima RelStr
for x being Element of L
for D being non empty lower Subset of L holds {x} "/\" D = (downarrow x) /\ D

proof end;

:: Definition 1.11 p.44

definition

let L be non empty RelStr ;
let AR be Relation of L;

attr AR is approximating means :Def17: :: WAYBEL_4:def 17
for x being Element of L holds x = sup (AR -below x);

end;

:: deftheorem Def17 defines approximating WAYBEL_4:def 17 :
for L being non empty RelStr
for AR being Relation of L holds
( AR is approximating iff for x being Element of L holds x = sup (AR -below x) );

definition

let L be non empty Poset;
let mp be Function of L,(InclPoset (Ids L));

attr mp is approximating means :: WAYBEL_4:def 18
for x being Element of L ex ii being Subset of L st
( ii = mp . x & x = sup ii );

end;

:: deftheorem defines approximating WAYBEL_4:def 18 :
for L being non empty Poset
for mp being Function of L,(InclPoset (Ids L)) holds
( mp is approximating iff for x being Element of L ex ii being Subset of L st
( ii = mp . x & x = sup ii ) );

:: Lemma 1.12 (i) p.44

theorem Th37: :: WAYBEL_4:37

for L being lower-bounded meet-continuous Semilattice
for I being Ideal of L holds DownMap I is approximating

proof end;

Lm11: for L being complete LATTICE
for x being Element of L
for D being directed Subset of L holds sup ({x} "/\" D) <= x

proof end;

:: Lemma 1.12 (ii) p.44

theorem Th38: :: WAYBEL_4:38

for L being lower-bounded continuous LATTICE holds L is meet-continuous

proof end;

registration

cluster reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous -> lower-bounded meet-continuous for RelStr ;

coherence
for b₁ being lower-bounded LATTICE st b₁ is continuous holds
b₁ is meet-continuous by Th38;

end;

:: Lemma 1.12 (iii) p.44

theorem :: WAYBEL_4:39

for L being lower-bounded continuous LATTICE
for I being Ideal of L holds DownMap I is approximating by Th37;

registration

let L be non empty reflexive antisymmetric RelStr ;

cluster L -waybelow -> auxiliary(i) ;

coherence
L -waybelow is auxiliary(i)

proof end;

end;

registration

let L be non empty reflexive transitive RelStr ;

cluster L -waybelow -> auxiliary(ii) ;

coherence
L -waybelow is auxiliary(ii)

proof end;

end;

registration

let L be with_suprema Poset;

cluster L -waybelow -> auxiliary(iii) ;

coherence
L -waybelow is auxiliary(iii)

proof end;

end;

registration

let L be non empty /\-complete Poset;

cluster L -waybelow -> auxiliary(iii) ;

coherence
L -waybelow is auxiliary(iii)

proof end;

end;

registration

let L be non empty reflexive antisymmetric lower-bounded RelStr ;

cluster L -waybelow -> auxiliary(iv) ;

coherence
L -waybelow is auxiliary(iv)

proof end;

end;

theorem Th40: :: WAYBEL_4:40

for L being complete LATTICE
for x being Element of L holds (L -waybelow) -below x = waybelow x

proof end;

theorem Th41: :: WAYBEL_4:41

for L being LATTICE holds IntRel L is approximating

proof end;

Lm12: for L being lower-bounded continuous LATTICE holds L -waybelow is approximating

proof end;

registration

let L be lower-bounded continuous LATTICE;

cluster L -waybelow -> approximating ;

coherence
L -waybelow is approximating by Lm12;

end;

registration

let L be complete LATTICE;

cluster Relation-like auxiliary approximating for Element of bool [: the carrier of L, the carrier of L:];

existence
ex b₁ being Relation of L st
( b₁ is approximating & b₁ is auxiliary )

proof end;

end;

definition

let L be complete LATTICE;
defpred S₁[ object ] means $1 is auxiliary approximating Relation of L;

func App L -> set means :Def19: :: WAYBEL_4:def 19
for a being set holds
( a in it iff a is auxiliary approximating Relation of L );

existence
ex b₁ being set st
for a being set holds
( a in b₁ iff a is auxiliary approximating Relation of L )

proof end;

uniqueness
for b₁, b₂ being set st ( for a being set holds
( a in b₁ iff a is auxiliary approximating Relation of L ) ) & ( for a being set holds
( a in b₂ iff a is auxiliary approximating Relation of L ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def19 defines App WAYBEL_4:def 19 :
for L being complete LATTICE
for b₂ being set holds
( b₂ = App L iff for a being set holds
( a in b₂ iff a is auxiliary approximating Relation of L ) );

registration

let L be complete LATTICE;

cluster App L -> non empty ;

coherence
not App L is empty

proof end;

end;

theorem Th42: :: WAYBEL_4:42

for L being complete LATTICE
for mp being Function of L,(InclPoset (Ids L)) st mp is approximating & mp in the carrier of (MonSet L) holds
ex AR being auxiliary approximating Relation of L st AR = (Map2Rel L) . mp

proof end;

theorem Th43: :: WAYBEL_4:43

for L being complete LATTICE
for x being Element of L holds meet { ((DownMap I) . x) where I is Ideal of L : verum } = waybelow x

proof end;

:: Proposition 1.13 p.45

theorem Th44: :: WAYBEL_4:44

for L being lower-bounded meet-continuous LATTICE
for x being Element of L holds meet { (AR -below x) where AR is auxiliary Relation of L : AR in App L } = waybelow x

proof end;

:: Proposition 1.14 p.45 ( 1 <=> 2 )

theorem Th45: :: WAYBEL_4:45

for L being complete LATTICE holds
( L is continuous iff for R being auxiliary approximating Relation of L holds
( L -waybelow c= R & L -waybelow is approximating ) )

proof end;

:: Proposition 1.14 p.45 ( 1 <=> 3 )

theorem :: WAYBEL_4:46

for L being complete LATTICE holds
( L is continuous iff ( L is meet-continuous & ex R being auxiliary approximating Relation of L st
for R9 being auxiliary approximating Relation of L holds R c= R9 ) )

proof end;

:: Definition 1.15 (SI) p.46

definition

let L be RelStr ;
let AR be Relation of L;

attr AR is satisfying_SI means :: WAYBEL_4:def 20
for x, z being Element of L st [x,z] in AR & x <> z holds
ex y being Element of L st
( [x,y] in AR & [y,z] in AR & x <> y );

end;

:: deftheorem defines satisfying_SI WAYBEL_4:def 20 :
for L being RelStr
for AR being Relation of L holds
( AR is satisfying_SI iff for x, z being Element of L st [x,z] in AR & x <> z holds
ex y being Element of L st
( [x,y] in AR & [y,z] in AR & x <> y ) );

:: Definition 1.15 (INT) p.46

definition

let L be RelStr ;
let AR be Relation of L;

attr AR is satisfying_INT means :Def21: :: WAYBEL_4:def 21
for x, z being Element of L st [x,z] in AR holds
ex y being Element of L st
( [x,y] in AR & [y,z] in AR );

end;

:: deftheorem Def21 defines satisfying_INT WAYBEL_4:def 21 :
for L being RelStr
for AR being Relation of L holds
( AR is satisfying_INT iff for x, z being Element of L st [x,z] in AR holds
ex y being Element of L st
( [x,y] in AR & [y,z] in AR ) );

theorem Th47: :: WAYBEL_4:47

for L being RelStr
for AR being Relation of L st AR is satisfying_SI holds
AR is satisfying_INT

proof end;

registration

let L be non empty RelStr ;

cluster satisfying_SI -> satisfying_INT for Element of bool [: the carrier of L, the carrier of L:];

coherence
for b₁ being Relation of L st b₁ is satisfying_SI holds
b₁ is satisfying_INT by Th47;

end;

theorem Th48: :: WAYBEL_4:48

for L being complete LATTICE
for x, y being Element of L
for AR being approximating Relation of L st not x <= y holds
ex u being Element of L st
( [u,x] in AR & not u <= y )

proof end;

:: Lemma 1.16 p.46

theorem Th49: :: WAYBEL_4:49

for L being complete LATTICE
for x, z being Element of L
for R being auxiliary(i) auxiliary(iii) approximating Relation of L st [x,z] in R & x <> z holds
ex y being Element of L st
( x <= y & [y,z] in R & x <> y )

proof end;

:: Lemma 1.17 p.46

theorem Th50: :: WAYBEL_4:50

for L being complete LATTICE
for x, z being Element of L
for R being auxiliary approximating Relation of L st x << z & x <> z holds
ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y )

proof end;

:: Theorem 1.18 p.47

theorem Th51: :: WAYBEL_4:51

for L being lower-bounded continuous LATTICE holds L -waybelow is satisfying_SI

proof end;

registration

let L be lower-bounded continuous LATTICE;

cluster L -waybelow -> satisfying_SI ;

coherence
L -waybelow is satisfying_SI by Th51;

end;

theorem Th52: :: WAYBEL_4:52

for L being lower-bounded continuous LATTICE
for x, y being Element of L st x << y holds
ex x9 being Element of L st
( x << x9 & x9 << y )

proof end;

:: Corollary 1.19 p.47

theorem :: WAYBEL_4:53

for L being lower-bounded continuous LATTICE
for x, y being Element of L holds
( x << y iff for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x << d ) )

proof end;

definition

let L be RelStr ;
let X be Subset of L;
let R be Relation of the carrier of L;

pred X is_directed_wrt R means :: WAYBEL_4:def 22
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] in R & [y,z] in R );

end;

:: deftheorem defines is_directed_wrt WAYBEL_4:def 22 :
for L being RelStr
for X being Subset of L
for R being Relation of the carrier of L holds
( X is_directed_wrt R 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] in R & [y,z] in R ) );

theorem :: WAYBEL_4:54

for L being RelStr
for X being Subset of L st X is_directed_wrt the InternalRel of L holds
X is directed

proof end;

definition

let X be set ;
let x be object ;
let R be Relation;

pred x is_maximal_wrt X,R means :: WAYBEL_4:def 23
( x in X & ( for y being set holds
( not y in X or not y <> x or not [x,y] in R ) ) );

end;

:: deftheorem defines is_maximal_wrt WAYBEL_4:def 23 :
for X being set
for x being object
for R being Relation holds
( x is_maximal_wrt X,R iff ( x in X & ( for y being set holds
( not y in X or not y <> x or not [x,y] in R ) ) ) );

definition

let L be RelStr ;
let X be set ;
let x be Element of L;

pred x is_maximal_in X means :: WAYBEL_4:def 24
x is_maximal_wrt X, the InternalRel of L;

end;

:: deftheorem defines is_maximal_in WAYBEL_4:def 24 :
for L being RelStr
for X being set
for x being Element of L holds
( x is_maximal_in X iff x is_maximal_wrt X, the InternalRel of L );

theorem :: WAYBEL_4:55

for L being RelStr
for X being set
for x being Element of L holds
( x is_maximal_in X iff ( x in X & ( for y being Element of L holds
( not y in X or not x < y ) ) ) )

proof end;

definition

let X be set ;
let x be object ;
let R be Relation;

pred x is_minimal_wrt X,R means :: WAYBEL_4:def 25
( x in X & ( for y being set holds
( not y in X or not y <> x or not [y,x] in R ) ) );

end;

:: deftheorem defines is_minimal_wrt WAYBEL_4:def 25 :
for X being set
for x being object
for R being Relation holds
( x is_minimal_wrt X,R iff ( x in X & ( for y being set holds
( not y in X or not y <> x or not [y,x] in R ) ) ) );

definition

let L be RelStr ;
let X be set ;
let x be Element of L;

pred x is_minimal_in X means :: WAYBEL_4:def 26
x is_minimal_wrt X, the InternalRel of L;

end;

:: deftheorem defines is_minimal_in WAYBEL_4:def 26 :
for L being RelStr
for X being set
for x being Element of L holds
( x is_minimal_in X iff x is_minimal_wrt X, the InternalRel of L );

theorem :: WAYBEL_4:56

for L being RelStr
for X being set
for x being Element of L holds
( x is_minimal_in X iff ( x in X & ( for y being Element of L holds
( not y in X or not x > y ) ) ) )

proof end;

:: Exercise 1.23 (i) ( 1 => 2 )

theorem :: WAYBEL_4:57

for L being complete LATTICE
for AR being Relation of L st AR is satisfying_SI holds
for x being Element of L st ex y being Element of L st y is_maximal_wrt AR -below x,AR holds
[x,x] in AR

proof end;

:: Exercise 1.23 (i) ( 2 => 1 )

theorem :: WAYBEL_4:58

for L being complete LATTICE
for AR being Relation of L st ( for x being Element of L st ex y being Element of L st y is_maximal_wrt AR -below x,AR holds
[x,x] in AR ) holds
AR is satisfying_SI

proof end;

:: Exercise 1.23 (ii) ( 3 => 4 )

theorem :: WAYBEL_4:59

for L being complete LATTICE
for AR being auxiliary(ii) auxiliary(iii) Relation of L st AR is satisfying_INT holds
for x being Element of L holds AR -below x is_directed_wrt AR

proof end;

:: Exercise 1.23 (ii) ( 4 => 3 )

theorem :: WAYBEL_4:60

for L being complete LATTICE
for AR being Relation of L st ( for x being Element of L holds AR -below x is_directed_wrt AR ) holds
AR is satisfying_INT

proof end;

:: Exercise 1.23 (iii) p.51

theorem Th61: :: WAYBEL_4:61

for L being complete LATTICE
for R being auxiliary(i) auxiliary(ii) auxiliary(iii) approximating Relation of L st R is satisfying_INT holds
R is satisfying_SI

proof end;

registration

let L be complete LATTICE;

cluster auxiliary approximating satisfying_INT -> auxiliary approximating satisfying_SI for Element of bool [: the carrier of L, the carrier of L:];

coherence
for b₁ being auxiliary approximating Relation of L st b₁ is satisfying_INT holds
b₁ is satisfying_SI by Th61;

end;