:: Meet-continuous Lattices
:: by Artur Korni{\l}owicz
::
:: Received October 10, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users

registration

let X, Y be non empty set ;
let f be Function of X,Y;
let Z be non empty Subset of X;

cluster f .: Z -> non empty ;

coherence
not f .: Z is empty

proof end;

end;

registration

cluster non empty reflexive connected -> non empty with_suprema with_infima for RelStr ;

coherence
for b₁ being non empty RelStr st b₁ is reflexive & b₁ is connected holds
( b₁ is with_infima & b₁ is with_suprema )

proof end;

end;

registration

let C be Chain;

cluster [#] C -> directed ;

coherence
[#] C is directed ;

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

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

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)

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)

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

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)

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

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

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)

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)

proof end;

registration

let S, T be non empty reflexive up-complete RelStr ;

cluster [:S,T:] -> up-complete ;

coherence
[:S,T:] is up-complete

proof end;

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 )

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

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)

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)

proof end;

registration

cluster 1 -element reflexive -> 1 -element reflexive distributive complemented for RelStr ;

coherence
for b₁ being 1 -element reflexive RelStr holds
( b₁ is distributive & b₁ is complemented )

proof end;

end;

registration

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

existence
ex b₁ being LATTICE st
( b₁ is strict & b₁ is 1 -element )

proof end;

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)

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)

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

proof end;

scheme :: WAYBEL_2:sch 1
ExNet{ F₁() -> non empty RelStr , F₂() -> prenet of F₁(), F₃( set ) -> Element of F₁() } :

ex M being prenet of F₁() st
( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of F₂(), the InternalRel of F₂() #) & ( for i being Element of M holds the mapping of M . i = F₃(( the mapping of F₂() . i)) ) )

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

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

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

proof end;

definition

let L be non empty RelStr ;
let N be NetStr over L;

func sup N -> Element of L equals :: WAYBEL_2:def 1
Sup ;

coherence
Sup is Element of L ;

end;

:: deftheorem defines sup WAYBEL_2:def 1 :
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;

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 b₁ 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₁ = NetStr(# (Fin J),(RelIncl (Fin J)),g #) )

proof end;

uniqueness
for b₁, b₂ 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₁ = 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₂ = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) holds
b₁ = b₂

proof end;

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₄ being prenet of L holds
( b₄ = 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₄ = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) );

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 )

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;

cluster FinSups f -> monotone ;

coherence
FinSups f is monotone

proof end;

end;

definition

let L be non empty RelStr ;
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
ex b₁ being strict NetStr over L st
( RelStr(# the carrier of b₁, the InternalRel of b₁ #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b₁ ex y being Element of L st
( y = the mapping of N . i & the mapping of b₁ . i = x "/\" y ) ) )

proof end;

uniqueness
for b₁, b₂ being strict NetStr over L st RelStr(# the carrier of b₁, the InternalRel of b₁ #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b₁ ex y being Element of L st
( y = the mapping of N . i & the mapping of b₁ . i = x "/\" y ) ) & RelStr(# the carrier of b₂, the InternalRel of b₂ #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b₂ ex y being Element of L st
( y = the mapping of N . i & the mapping of b₂ . i = x "/\" y ) ) holds
b₁ = b₂

proof end;

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₄ being strict NetStr over L holds
( b₄ = x "/\" N iff ( RelStr(# the carrier of b₄, the InternalRel of b₄ #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b₄ ex y being Element of L st
( y = the mapping of N . i & the mapping of b₄ . i = x "/\" y ) ) ) );

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

proof end;

registration

let L be non empty RelStr ;
let x be Element of L;
let N be non empty NetStr over L;

cluster x "/\" N -> non empty strict ;

coherence
not x "/\" N is empty

proof end;

end;

registration

let L be non empty RelStr ;
let x be Element of L;
let N be prenet of L;

cluster x "/\" N -> strict directed ;

coherence
x "/\" N is directed

proof end;

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)

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)

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

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)

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

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)

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

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)

proof end;

definition

let L be non empty RelStr ;

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
ex b₁ being Function of [:L,L:],L st
for x, y being Element of L holds b₁ . (x,y) = x "/\" y

proof end;

uniqueness
for b₁, b₂ being Function of [:L,L:],L st ( for x, y being Element of L holds b₁ . (x,y) = x "/\" y ) & ( for x, y being Element of L holds b₂ . (x,y) = x "/\" y ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines inf_op WAYBEL_2:def 4 :
for L being non empty RelStr
for b₂ being Function of [:L,L:],L holds
( b₂ = inf_op L iff for x, y being Element of L holds b₂ . (x,y) = x "/\" y );

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)

proof end;

registration

let L be transitive antisymmetric with_infima RelStr ;

cluster inf_op L -> monotone ;

coherence
inf_op L is monotone

proof end;

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

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

proof end;

definition

let L be non empty RelStr ;

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
ex b₁ being Function of [:L,L:],L st
for x, y being Element of L holds b₁ . (x,y) = x "\/" y

proof end;

uniqueness
for b₁, b₂ being Function of [:L,L:],L st ( for x, y being Element of L holds b₁ . (x,y) = x "\/" y ) & ( for x, y being Element of L holds b₂ . (x,y) = x "\/" y ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines sup_op WAYBEL_2:def 5 :
for L being non empty RelStr
for b₂ being Function of [:L,L:],L holds
( b₂ = sup_op L iff for x, y being Element of L holds b₂ . (x,y) = x "\/" y );

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)

proof end;

registration

let L be transitive antisymmetric with_suprema RelStr ;

cluster sup_op L -> monotone ;

coherence
sup_op L is monotone

proof end;

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

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

proof end;

:: Def 4.1, s.30

definition

let R be non empty reflexive RelStr ;

attr R is satisfying_MC means :Def6: :: WAYBEL_2:def 6
for x being Element of R
for D being non empty directed Subset of R holds x "/\" (sup D) = sup ({x} "/\" D);

end;

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

definition

let R be non empty reflexive RelStr ;

attr R is meet-continuous means :: WAYBEL_2:def 7
( R is up-complete & R is satisfying_MC );

end;

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

registration

cluster 1 -element reflexive -> 1 -element reflexive satisfying_MC for RelStr ;

coherence
for b₁ being 1 -element reflexive RelStr holds b₁ is satisfying_MC by STRUCT_0:def 10;

end;

registration

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

coherence
for b₁ being non empty reflexive RelStr st b₁ is meet-continuous holds
( b₁ is up-complete & b₁ is satisfying_MC ) ;

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

coherence
for b₁ being non empty reflexive RelStr st b₁ is up-complete & b₁ is satisfying_MC holds
b₁ is meet-continuous ;

end;

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

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)

proof end;

registration

let L be up-complete sup-Semilattice;

cluster SupMap L -> join-preserving ;

coherence
SupMap L is join-preserving

proof end;

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

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)

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

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

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)

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

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)

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

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

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

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

proof end;

registration

let L be meet-continuous LATTICE;

cluster SupMap L -> meet-preserving join-preserving ;

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

end;

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

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

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

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 )

proof end;

registration

let L be meet-continuous Semilattice;

cluster inf_op L -> directed-sups-preserving ;

coherence
inf_op L is directed-sups-preserving by Th53;

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)))) ) by Th41, Th42;

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

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;

cluster x "/\" -> directed-sups-preserving ;

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

end;

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

proof end;

registration

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

coherence
for b₁ being non empty Poset st b₁ is complete & b₁ is Heyting holds
( b₁ is meet-continuous & b₁ is distributive ) by Th56;

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

coherence
for b₁ being non empty Poset st b₁ is complete & b₁ is meet-continuous & b₁ is distributive holds
b₁ is Heyting by Th56;

end;