:: by Artur Korni{\l}owicz

::

:: Received October 10, 1996

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

begin

registration

let X, Y be non empty set ;

let f be Function of X,Y;

let Z be non empty Subset of X;

coherence

not f .: Z is empty

end;
let f be Function of X,Y;

let Z be non empty Subset of X;

coherence

not f .: Z is empty

proof end;

registration

coherence

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

( b_{1} is with_infima & b_{1} is with_suprema )

end;
for b

( b

proof end;

theorem Th1: :: WAYBEL_2:1

for L being up-complete Semilattice

for D being non empty directed Subset of L

for x being Element of L holds ex_sup_of {x} "/\" D,L

for D being non empty directed Subset of L

for x being Element of L holds ex_sup_of {x} "/\" D,L

proof end;

theorem :: WAYBEL_2:2

for L being up-complete sup-Semilattice

for D being non empty directed Subset of L

for x being Element of L holds ex_sup_of {x} "\/" D,L

for D being non empty directed Subset of L

for x being Element of L holds ex_sup_of {x} "\/" D,L

proof end;

theorem Th3: :: WAYBEL_2:3

for L being up-complete sup-Semilattice

for A, B being non empty directed Subset of L holds A is_<=_than sup (A "\/" B)

for A, B being non empty directed Subset of L holds A is_<=_than sup (A "\/" B)

proof end;

theorem Th4: :: WAYBEL_2:4

for L being up-complete sup-Semilattice

for A, B being non empty directed Subset of L holds sup (A "\/" B) = (sup A) "\/" (sup B)

for A, B being non empty directed Subset of L holds sup (A "\/" B) = (sup A) "\/" (sup B)

proof end;

theorem Th5: :: WAYBEL_2:5

for L being up-complete Semilattice

for D being non empty directed Subset of [:L,L:] holds { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } = { (sup X) where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) }

for D being non empty directed Subset of [:L,L:] holds { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } = { (sup X) where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) }

proof end;

theorem Th6: :: WAYBEL_2:6

for L being Semilattice

for D being non empty directed Subset of [:L,L:] holds union { X where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } = (proj1 D) "/\" (proj2 D)

for D being non empty directed Subset of [:L,L:] holds union { X where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } = (proj1 D) "/\" (proj2 D)

proof end;

theorem Th7: :: WAYBEL_2:7

for L being up-complete Semilattice

for D being non empty directed Subset of [:L,L:] holds ex_sup_of union { X where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L

for D being non empty directed Subset of [:L,L:] holds ex_sup_of union { X where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L

proof end;

theorem Th8: :: WAYBEL_2:8

for L being up-complete Semilattice

for D being non empty directed Subset of [:L,L:] holds ex_sup_of { (sup X) where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L

for D being non empty directed Subset of [:L,L:] holds ex_sup_of { (sup X) where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L

proof end;

theorem Th9: :: WAYBEL_2:9

for L being up-complete Semilattice

for D being non empty directed Subset of [:L,L:] holds "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) <= "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } ),L)

for D being non empty directed Subset of [:L,L:] holds "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) <= "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } ),L)

proof end;

theorem Th10: :: WAYBEL_2:10

for L being up-complete Semilattice

for D being non empty directed Subset of [:L,L:] holds "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) = "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } ),L)

for D being non empty directed Subset of [:L,L:] holds "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) = "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } ),L)

proof end;

registration
end;

theorem :: WAYBEL_2:11

for S, T being non empty reflexive antisymmetric RelStr st [:S,T:] is up-complete holds

( S is up-complete & T is up-complete )

( S is up-complete & T is up-complete )

proof end;

theorem Th12: :: WAYBEL_2:12

for L being non empty reflexive antisymmetric up-complete RelStr

for D being non empty directed Subset of [:L,L:] holds sup D = [(sup (proj1 D)),(sup (proj2 D))]

for D being non empty directed Subset of [:L,L:] holds sup D = [(sup (proj1 D)),(sup (proj2 D))]

proof end;

theorem Th13: :: WAYBEL_2:13

for S1, S2 being RelStr

for D being Subset of S1

for f being Function of S1,S2 st f is monotone holds

f .: (downarrow D) c= downarrow (f .: D)

for D being Subset of S1

for f being Function of S1,S2 st f is monotone holds

f .: (downarrow D) c= downarrow (f .: D)

proof end;

theorem Th14: :: WAYBEL_2:14

for S1, S2 being RelStr

for D being Subset of S1

for f being Function of S1,S2 st f is monotone holds

f .: (uparrow D) c= uparrow (f .: D)

for D being Subset of S1

for f being Function of S1,S2 st f is monotone holds

f .: (uparrow D) c= uparrow (f .: D)

proof end;

registration

coherence

for b_{1} being 1 -element reflexive RelStr holds

( b_{1} is distributive & b_{1} is complemented )

end;
for b

( b

proof end;

registration

ex b_{1} being LATTICE st

( b_{1} is strict & b_{1} is 1 -element )
end;

cluster non empty 1 -element strict V70() reflexive transitive antisymmetric non void with_suprema with_infima for RelStr ;

existence ex b

( b

proof end;

theorem Th15: :: WAYBEL_2:15

for H being distributive complete LATTICE

for a being Element of H

for X being finite Subset of H holds sup ({a} "/\" X) = a "/\" (sup X)

for a being Element of H

for X being finite Subset of H holds sup ({a} "/\" X) = a "/\" (sup X)

proof end;

theorem :: WAYBEL_2:16

for H being distributive complete LATTICE

for a being Element of H

for X being finite Subset of H holds inf ({a} "\/" X) = a "\/" (inf X)

for a being Element of H

for X being finite Subset of H holds inf ({a} "\/" X) = a "\/" (inf X)

proof end;

theorem Th17: :: WAYBEL_2:17

for H being distributive complete LATTICE

for a being Element of H

for X being finite Subset of H holds a "/\" preserves_sup_of X

for a being Element of H

for X being finite Subset of H holds a "/\" preserves_sup_of X

proof end;

begin

scheme :: WAYBEL_2:sch 1

ExNet{ F_{1}() -> non empty RelStr , F_{2}() -> prenet of F_{1}(), F_{3}( set ) -> Element of F_{1}() } :

ExNet{ F

ex M being prenet of F_{1}() st

( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of F_{2}(), the InternalRel of F_{2}() #) & ( for i being Element of M holds the mapping of M . i = F_{3}(( the mapping of F_{2}() . i)) ) )

( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of F

proof end;

theorem Th18: :: WAYBEL_2:18

for L being non empty RelStr

for N being prenet of L st N is eventually-directed holds

rng (netmap (N,L)) is directed

for N being prenet of L st N is eventually-directed holds

rng (netmap (N,L)) is directed

proof end;

theorem Th19: :: WAYBEL_2:19

for L being non empty reflexive RelStr

for D being non empty directed Subset of L

for n being Function of D, the carrier of L holds NetStr(# D,( the InternalRel of L |_2 D),n #) is prenet of L

for D being non empty directed Subset of L

for n being Function of D, the carrier of L holds NetStr(# D,( the InternalRel of L |_2 D),n #) is prenet of L

proof end;

theorem Th20: :: WAYBEL_2:20

for L being non empty reflexive RelStr

for D being non empty directed Subset of L

for n being Function of D, the carrier of L

for N being prenet of L st n = id D & N = NetStr(# D,( the InternalRel of L |_2 D),n #) holds

N is eventually-directed

for D being non empty directed Subset of L

for n being Function of D, the carrier of L

for N being prenet of L st n = id D & N = NetStr(# D,( the InternalRel of L |_2 D),n #) holds

N is eventually-directed

proof end;

:: deftheorem defines sup WAYBEL_2:def 1 :

for L being non empty RelStr

for N being NetStr over L holds sup N = Sup ;

for L being non empty RelStr

for N being NetStr over L holds sup N = Sup ;

definition

let L be non empty RelStr ;

let J be set ;

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

ex b_{1} being prenet of L ex g being Function of (Fin J), the carrier of L st

for x being Element of Fin J holds

( g . x = sup (f .: x) & b_{1} = NetStr(# (Fin J),(RelIncl (Fin J)),g #) )

for b_{1}, b_{2} being prenet of L st ex g being Function of (Fin J), the carrier of L st

for x being Element of Fin J holds

( g . x = sup (f .: x) & b_{1} = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) & ex g being Function of (Fin J), the carrier of L st

for x being Element of Fin J holds

( g . x = sup (f .: x) & b_{2} = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) holds

b_{1} = b_{2}

end;
let J be set ;

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

func FinSups f -> prenet of L means :Def2: :: WAYBEL_2:def 2

ex g being Function of (Fin J), the carrier of L st

for x being Element of Fin J holds

( g . x = sup (f .: x) & it = NetStr(# (Fin J),(RelIncl (Fin J)),g #) );

existence ex g being Function of (Fin J), the carrier of L st

for x being Element of Fin J holds

( g . x = sup (f .: x) & it = NetStr(# (Fin J),(RelIncl (Fin J)),g #) );

ex b

for x being Element of Fin J holds

( g . x = sup (f .: x) & b

proof end;

uniqueness for b

for x being Element of Fin J holds

( g . x = sup (f .: x) & b

for x being Element of Fin J holds

( g . x = sup (f .: x) & b

b

proof end;

:: deftheorem Def2 defines FinSups WAYBEL_2:def 2 :

for L being non empty RelStr

for J being set

for f being Function of J, the carrier of L

for b_{4} being prenet of L holds

( b_{4} = FinSups f iff ex g being Function of (Fin J), the carrier of L st

for x being Element of Fin J holds

( g . x = sup (f .: x) & b_{4} = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) );

for L being non empty RelStr

for J being set

for f being Function of J, the carrier of L

for b

( b

for x being Element of Fin J holds

( g . x = sup (f .: x) & b

theorem :: WAYBEL_2:21

for L being non empty RelStr

for J, x being set

for f being Function of J, the carrier of L holds

( x is Element of (FinSups f) iff x is Element of Fin J )

for J, x being set

for f being Function of J, the carrier of L holds

( x is Element of (FinSups f) iff x is Element of Fin J )

proof end;

registration

let L be non empty reflexive antisymmetric complete RelStr ;

let J be set ;

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

coherence

FinSups f is monotone

end;
let J be set ;

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

coherence

FinSups f is monotone

proof end;

definition

let L be non empty RelStr ;

let x be Element of L;

let N be non empty NetStr over L;

ex b_{1} being strict NetStr over L st

( RelStr(# the carrier of b_{1}, the InternalRel of b_{1} #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b_{1} ex y being Element of L st

( y = the mapping of N . i & the mapping of b_{1} . i = x "/\" y ) ) )

for b_{1}, b_{2} being strict NetStr over L st RelStr(# the carrier of b_{1}, the InternalRel of b_{1} #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b_{1} ex y being Element of L st

( y = the mapping of N . i & the mapping of b_{1} . i = x "/\" y ) ) & RelStr(# the carrier of b_{2}, the InternalRel of b_{2} #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b_{2} ex y being Element of L st

( y = the mapping of N . i & the mapping of b_{2} . i = x "/\" y ) ) holds

b_{1} = b_{2}

end;
let x be Element of L;

let N be non empty NetStr over L;

func x "/\" N -> strict NetStr over L means :Def3: :: WAYBEL_2:def 3

( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of it ex y being Element of L st

( y = the mapping of N . i & the mapping of it . i = x "/\" y ) ) );

existence ( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of it ex y being Element of L st

( y = the mapping of N . i & the mapping of it . i = x "/\" y ) ) );

ex b

( RelStr(# the carrier of b

( y = the mapping of N . i & the mapping of b

proof end;

uniqueness for b

( y = the mapping of N . i & the mapping of b

( y = the mapping of N . i & the mapping of b

b

proof end;

:: deftheorem Def3 defines "/\" WAYBEL_2:def 3 :

for L being non empty RelStr

for x being Element of L

for N being non empty NetStr over L

for b_{4} being strict NetStr over L holds

( b_{4} = x "/\" N iff ( RelStr(# the carrier of b_{4}, the InternalRel of b_{4} #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b_{4} ex y being Element of L st

( y = the mapping of N . i & the mapping of b_{4} . i = x "/\" y ) ) ) );

for L being non empty RelStr

for x being Element of L

for N being non empty NetStr over L

for b

( b

( y = the mapping of N . i & the mapping of b

theorem Th22: :: WAYBEL_2:22

for L being non empty RelStr

for N being non empty NetStr over L

for x being Element of L

for y being set holds

( y is Element of N iff y is Element of (x "/\" N) )

for N being non empty NetStr over L

for x being Element of L

for y being set holds

( y is Element of N iff y is Element of (x "/\" N) )

proof end;

registration

let L be non empty RelStr ;

let x be Element of L;

let N be non empty NetStr over L;

coherence

not x "/\" N is empty

end;
let x be Element of L;

let N be non empty NetStr over L;

coherence

not x "/\" N is empty

proof end;

registration

let L be non empty RelStr ;

let x be Element of L;

let N be prenet of L;

coherence

x "/\" N is directed

end;
let x be Element of L;

let N be prenet of L;

coherence

x "/\" N is directed

proof end;

theorem Th23: :: WAYBEL_2:23

for L being non empty RelStr

for x being Element of L

for F being non empty NetStr over L holds rng the mapping of (x "/\" F) = {x} "/\" (rng the mapping of F)

for x being Element of L

for F being non empty NetStr over L holds rng the mapping of (x "/\" F) = {x} "/\" (rng the mapping of F)

proof end;

theorem Th24: :: WAYBEL_2:24

for L being non empty RelStr

for J being set

for f being Function of J, the carrier of L st ( for x being set holds ex_sup_of f .: x,L ) holds

rng (netmap ((FinSups f),L)) c= finsups (rng f)

for J being set

for f being Function of J, the carrier of L st ( for x being set holds ex_sup_of f .: x,L ) holds

rng (netmap ((FinSups f),L)) c= finsups (rng f)

proof end;

theorem Th25: :: WAYBEL_2:25

for L being non empty reflexive antisymmetric RelStr

for J being set

for f being Function of J, the carrier of L holds rng f c= rng (netmap ((FinSups f),L))

for J being set

for f being Function of J, the carrier of L holds rng f c= rng (netmap ((FinSups f),L))

proof end;

theorem Th26: :: WAYBEL_2:26

for L being non empty reflexive antisymmetric RelStr

for J being set

for f being Function of J, the carrier of L st ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) holds

Sup = sup (FinSups f)

for J being set

for f being Function of J, the carrier of L st ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) holds

Sup = sup (FinSups f)

proof end;

theorem Th27: :: WAYBEL_2:27

for L being transitive antisymmetric with_infima RelStr

for N being prenet of L

for x being Element of L st N is eventually-directed holds

x "/\" N is eventually-directed

for N being prenet of L

for x being Element of L st N is eventually-directed holds

x "/\" N is eventually-directed

proof end;

theorem Th28: :: WAYBEL_2:28

for L being up-complete Semilattice st ( for x being Element of L

for E being non empty directed Subset of L st x <= sup E holds

x <= sup ({x} "/\" E) ) holds

for D being non empty directed Subset of L

for x being Element of L holds x "/\" (sup D) = sup ({x} "/\" D)

for E being non empty directed Subset of L st x <= sup E holds

x <= sup ({x} "/\" E) ) holds

for D being non empty directed Subset of L

for x being Element of L holds x "/\" (sup D) = sup ({x} "/\" D)

proof end;

theorem :: WAYBEL_2:29

for L being with_suprema Poset st ( for X being directed Subset of L

for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X) ) holds

for X being Subset of L

for x being Element of L st ex_sup_of X,L holds

x "/\" (sup X) = sup ({x} "/\" (finsups X))

for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X) ) holds

for X being Subset of L

for x being Element of L st ex_sup_of X,L holds

x "/\" (sup X) = sup ({x} "/\" (finsups X))

proof end;

theorem :: WAYBEL_2:30

for L being up-complete LATTICE st ( for X being Subset of L

for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" (finsups X)) ) holds

for X being non empty directed Subset of L

for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X)

for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" (finsups X)) ) holds

for X being non empty directed Subset of L

for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X)

proof end;

begin

definition

let L be non empty RelStr ;

ex b_{1} being Function of [:L,L:],L st

for x, y being Element of L holds b_{1} . (x,y) = x "/\" y

for b_{1}, b_{2} being Function of [:L,L:],L st ( for x, y being Element of L holds b_{1} . (x,y) = x "/\" y ) & ( for x, y being Element of L holds b_{2} . (x,y) = x "/\" y ) holds

b_{1} = b_{2}

end;
func inf_op L -> Function of [:L,L:],L means :Def4: :: WAYBEL_2:def 4

for x, y being Element of L holds it . (x,y) = x "/\" y;

existence for x, y being Element of L holds it . (x,y) = x "/\" y;

ex b

for x, y being Element of L holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines inf_op WAYBEL_2:def 4 :

for L being non empty RelStr

for b_{2} being Function of [:L,L:],L holds

( b_{2} = inf_op L iff for x, y being Element of L holds b_{2} . (x,y) = x "/\" y );

for L being non empty RelStr

for b

( b

theorem Th31: :: WAYBEL_2:31

for L being non empty RelStr

for x being Element of [:L,L:] holds (inf_op L) . x = (x `1) "/\" (x `2)

for x being Element of [:L,L:] holds (inf_op L) . x = (x `1) "/\" (x `2)

proof end;

registration
end;

theorem Th32: :: WAYBEL_2:32

for S being non empty RelStr

for D1, D2 being Subset of S holds (inf_op S) .: [:D1,D2:] = D1 "/\" D2

for D1, D2 being Subset of S holds (inf_op S) .: [:D1,D2:] = D1 "/\" D2

proof end;

theorem Th33: :: WAYBEL_2:33

for L being up-complete Semilattice

for D being non empty directed Subset of [:L,L:] holds sup ((inf_op L) .: D) = sup ((proj1 D) "/\" (proj2 D))

for D being non empty directed Subset of [:L,L:] holds sup ((inf_op L) .: D) = sup ((proj1 D) "/\" (proj2 D))

proof end;

definition

let L be non empty RelStr ;

ex b_{1} being Function of [:L,L:],L st

for x, y being Element of L holds b_{1} . (x,y) = x "\/" y

for b_{1}, b_{2} being Function of [:L,L:],L st ( for x, y being Element of L holds b_{1} . (x,y) = x "\/" y ) & ( for x, y being Element of L holds b_{2} . (x,y) = x "\/" y ) holds

b_{1} = b_{2}

end;
func sup_op L -> Function of [:L,L:],L means :Def5: :: WAYBEL_2:def 5

for x, y being Element of L holds it . (x,y) = x "\/" y;

existence for x, y being Element of L holds it . (x,y) = x "\/" y;

ex b

for x, y being Element of L holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines sup_op WAYBEL_2:def 5 :

for L being non empty RelStr

for b_{2} being Function of [:L,L:],L holds

( b_{2} = sup_op L iff for x, y being Element of L holds b_{2} . (x,y) = x "\/" y );

for L being non empty RelStr

for b

( b

theorem Th34: :: WAYBEL_2:34

for L being non empty RelStr

for x being Element of [:L,L:] holds (sup_op L) . x = (x `1) "\/" (x `2)

for x being Element of [:L,L:] holds (sup_op L) . x = (x `1) "\/" (x `2)

proof end;

registration
end;

theorem Th35: :: WAYBEL_2:35

for S being non empty RelStr

for D1, D2 being Subset of S holds (sup_op S) .: [:D1,D2:] = D1 "\/" D2

for D1, D2 being Subset of S holds (sup_op S) .: [:D1,D2:] = D1 "\/" D2

proof end;

theorem :: WAYBEL_2:36

for L being non empty complete Poset

for D being non empty filtered Subset of [:L,L:] holds inf ((sup_op L) .: D) = inf ((proj1 D) "\/" (proj2 D))

for D being non empty filtered Subset of [:L,L:] holds inf ((sup_op L) .: D) = inf ((proj1 D) "\/" (proj2 D))

proof end;

begin

:: Def 4.1, s.30

:: deftheorem Def6 defines satisfying_MC WAYBEL_2:def 6 :

for R being non empty reflexive RelStr holds

( R is satisfying_MC iff for x being Element of R

for D being non empty directed Subset of R holds x "/\" (sup D) = sup ({x} "/\" D) );

for R being non empty reflexive RelStr holds

( R is satisfying_MC iff for x being Element of R

for D being non empty directed Subset of R holds x "/\" (sup D) = sup ({x} "/\" D) );

:: deftheorem Def7 defines meet-continuous WAYBEL_2:def 7 :

for R being non empty reflexive RelStr holds

( R is meet-continuous iff ( R is up-complete & R is satisfying_MC ) );

for R being non empty reflexive RelStr holds

( R is meet-continuous iff ( R is up-complete & R is satisfying_MC ) );

registration
end;

registration

for b_{1} being non empty reflexive RelStr st b_{1} is meet-continuous holds

( b_{1} is up-complete & b_{1} is satisfying_MC )
by Def7;

for b_{1} being non empty reflexive RelStr st b_{1} is up-complete & b_{1} is satisfying_MC holds

b_{1} is meet-continuous
by Def7;

end;

cluster non empty reflexive meet-continuous -> non empty reflexive up-complete satisfying_MC for RelStr ;

coherence for b

( b

cluster non empty reflexive up-complete satisfying_MC -> non empty reflexive meet-continuous for RelStr ;

coherence for b

b

theorem Th37: :: WAYBEL_2:37

for S being non empty reflexive RelStr st ( for X being Subset of S

for x being Element of S holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ) holds

S is satisfying_MC

for x being Element of S holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ) holds

S is satisfying_MC

proof end;

:: Th 4.2, s.30, 1 => 2

theorem Th38: :: WAYBEL_2:38

for L being up-complete Semilattice st SupMap L is meet-preserving holds

for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2)

for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2)

proof end;

registration
end;

:: Th 4.2, s.30, 2 => 1

theorem Th39: :: WAYBEL_2:39

for L being up-complete Semilattice st ( for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ) holds

SupMap L is meet-preserving

SupMap L is meet-preserving

proof end;

:: Th 4.2, s.30, 2 => 3

theorem Th40: :: WAYBEL_2:40

for L being up-complete Semilattice st ( for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ) holds

for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)

for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)

proof end;

:: Th 4.2, s.30, 4 => 7

theorem Th41: :: WAYBEL_2:41

for L being non empty reflexive RelStr st L is satisfying_MC holds

for x being Element of L

for N being prenet of L st N is eventually-directed holds

x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))

for x being Element of L

for N being prenet of L st N is eventually-directed holds

x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))

proof end;

:: Th 4.2, s.30, 7 => 4

theorem Th42: :: WAYBEL_2:42

for L being non empty reflexive RelStr st ( for x being Element of L

for N being prenet of L st N is eventually-directed holds

x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) holds

L is satisfying_MC

for N being prenet of L st N is eventually-directed holds

x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) holds

L is satisfying_MC

proof end;

:: Th 4.2, s.30, 6 => 3

theorem Th43: :: WAYBEL_2:43

for L being non empty reflexive antisymmetric up-complete RelStr st inf_op L is directed-sups-preserving holds

for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)

for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)

proof end;

:: Th 4.2, s.30, 3 => 4

theorem Th44: :: WAYBEL_2:44

for L being non empty reflexive antisymmetric RelStr st ( for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) ) holds

L is satisfying_MC

L is satisfying_MC

proof end;

:: Th 4.2, s.30, MC => 5

theorem Th45: :: WAYBEL_2:45

for L being non empty reflexive antisymmetric with_infima satisfying_MC RelStr

for x being Element of L

for D being non empty directed Subset of L st x <= sup D holds

x = sup ({x} "/\" D)

for x being Element of L

for D being non empty directed Subset of L st x <= sup D holds

x = sup ({x} "/\" D)

proof end;

:: Th 4.2, s.30, 5 => 6

theorem Th46: :: WAYBEL_2:46

for L being up-complete Semilattice st ( for x being Element of L

for E being non empty directed Subset of L st x <= sup E holds

x <= sup ({x} "/\" E) ) holds

inf_op L is directed-sups-preserving

for E being non empty directed Subset of L st x <= sup E holds

x <= sup ({x} "/\" E) ) holds

inf_op L is directed-sups-preserving

proof end;

:: Th 4.2, s.30, 7 => 8

theorem Th47: :: WAYBEL_2:47

for L being non empty reflexive antisymmetric complete RelStr st ( for x being Element of L

for N being prenet of L st N is eventually-directed holds

x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) holds

for x being Element of L

for J being set

for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f))

for N being prenet of L st N is eventually-directed holds

x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) holds

for x being Element of L

for J being set

for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f))

proof end;

:: Th 4.2, s.30, 8 => 7

theorem Th48: :: WAYBEL_2:48

for L being complete Semilattice st ( for x being Element of L

for J being set

for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ) holds

for x being Element of L

for N being prenet of L st N is eventually-directed holds

x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))

for J being set

for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ) holds

for x being Element of L

for N being prenet of L st N is eventually-directed holds

x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))

proof end;

:: Th 4.2, s.30, 4 <=> 1

theorem Th49: :: WAYBEL_2:49

for L being up-complete LATTICE holds

( L is meet-continuous iff ( SupMap L is meet-preserving & SupMap L is join-preserving ) )

( L is meet-continuous iff ( SupMap L is meet-preserving & SupMap L is join-preserving ) )

proof end;

registration

let L be meet-continuous LATTICE;

coherence

( SupMap L is meet-preserving & SupMap L is join-preserving ) by Th49;

end;
coherence

( SupMap L is meet-preserving & SupMap L is join-preserving ) by Th49;

:: Th 4.2, s.30, 4 <=> 2

theorem Th50: :: WAYBEL_2:50

for L being up-complete LATTICE holds

( L is meet-continuous iff for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) )

( L is meet-continuous iff for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) )

proof end;

:: Th 4.2, s.30, 4 <=> 3

theorem Th51: :: WAYBEL_2:51

for L being up-complete LATTICE holds

( L is meet-continuous iff for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) )

( L is meet-continuous iff for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) )

proof end;

:: Th 4.2, s.30, 4 <=> 5

theorem :: WAYBEL_2:52

for L being up-complete LATTICE holds

( L is meet-continuous iff for x being Element of L

for D being non empty directed Subset of L st x <= sup D holds

x = sup ({x} "/\" D) )

( L is meet-continuous iff for x being Element of L

for D being non empty directed Subset of L st x <= sup D holds

x = sup ({x} "/\" D) )

proof end;

:: Th 4.2, s.30, 4 <=> 6

theorem Th53: :: WAYBEL_2:53

for L being up-complete Semilattice holds

( L is meet-continuous iff inf_op L is directed-sups-preserving )

( L is meet-continuous iff inf_op L is directed-sups-preserving )

proof end;

registration
end;

:: Th 4.2, s.30, 4 <=> 7

theorem Th54: :: WAYBEL_2:54

for L being up-complete Semilattice holds

( L is meet-continuous iff for x being Element of L

for N being prenet of L st N is eventually-directed holds

x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) )

( L is meet-continuous iff for x being Element of L

for N being prenet of L st N is eventually-directed holds

x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) )

proof end;

:: Th 4.2, s.30, 4 <=> 8

theorem :: WAYBEL_2:55

for L being complete Semilattice holds

( L is meet-continuous iff for x being Element of L

for J being set

for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) )

( L is meet-continuous iff for x being Element of L

for J being set

for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) )

proof end;

Lm1: for L being meet-continuous Semilattice

for x being Element of L holds x "/\" is directed-sups-preserving

proof end;

registration

let L be meet-continuous Semilattice;

let x be Element of L;

coherence

x "/\" is directed-sups-preserving by Lm1;

end;
let x be Element of L;

coherence

x "/\" is directed-sups-preserving by Lm1;

:: Remark 4.3 s.31

theorem Th56: :: WAYBEL_2:56

for H being non empty complete Poset holds

( H is Heyting iff ( H is meet-continuous & H is distributive ) )

( H is Heyting iff ( H is meet-continuous & H is distributive ) )

proof end;

registration

for b_{1} being non empty Poset st b_{1} is complete & b_{1} is Heyting holds

( b_{1} is meet-continuous & b_{1} is distributive )
by Th56;

for b_{1} being non empty Poset st b_{1} is complete & b_{1} is meet-continuous & b_{1} is distributive holds

b_{1} is Heyting
by Th56;

end;

cluster non empty reflexive transitive antisymmetric Heyting complete -> non empty distributive meet-continuous for RelStr ;

coherence for b

( b

cluster non empty reflexive transitive antisymmetric distributive complete meet-continuous -> non empty Heyting for RelStr ;

coherence for b

b