:: Meet-continuous Lattices
:: by Artur Korni{\l}owicz
::
:: Copyright (c) 1996-2019 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
coherence
for b1 being non empty RelStr st b1 is reflexive & b1 is connected holds
( b1 is with_infima & b1 is with_suprema )
proof end;
end;

registration
let C be Chain;
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} "/\" ())) 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} "/\" () & 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} "/\" () & x in proj1 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} "/\" () & 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} "/\" () & 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} "/\" () & 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} "/\" () & 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} "/\" () & 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} "/\" () & 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 ()),(sup ())]
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 .: () 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 .: () c= uparrow (f .: D)
proof end;

registration
coherence
for b1 being 1 -element reflexive RelStr holds
( b1 is distributive & b1 is complemented )
proof end;
end;

registration
existence
ex b1 being LATTICE st
( b1 is strict & b1 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{ F1() -> non empty RelStr , F2() -> prenet of F1(), F3( set ) -> Element of F1() } :
ex M being prenet of F1() st
( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of F2(), the InternalRel of F2() #) & ( for i being Element of M holds the mapping of M . i = F3(( the mapping of F2() . 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 b1 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) & b1 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) )
proof end;
uniqueness
for b1, b2 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) & b1 = 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) & b2 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) holds
b1 = b2
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 b4 being prenet of L holds
( b4 = 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) & b4 = 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 () 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
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 b1 being strict NetStr over L st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b1 ex y being Element of L st
( y = the mapping of N . i & the mapping of b1 . i = x "/\" y ) ) )
proof end;
uniqueness
for b1, b2 being strict NetStr over L st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b1 ex y being Element of L st
( y = the mapping of N . i & the mapping of b1 . i = x "/\" y ) ) & RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b2 ex y being Element of L st
( y = the mapping of N . i & the mapping of b2 . i = x "/\" y ) ) holds
b1 = b2
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 b4 being strict NetStr over L holds
( b4 = x "/\" N iff ( RelStr(# the carrier of b4, the InternalRel of b4 #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b4 ex y being Element of L st
( y = the mapping of N . i & the mapping of b4 . 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;
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 ((),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 ((),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 ((),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) holds
Sup = sup ()
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} "/\" ())
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} "/\" ()) ) 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 b1 being Function of [:L,L:],L st
for x, y being Element of L holds b1 . (x,y) = x "/\" y
proof end;
uniqueness
for b1, b2 being Function of [:L,L:],L st ( for x, y being Element of L holds b1 . (x,y) = x "/\" y ) & ( for x, y being Element of L holds b2 . (x,y) = x "/\" y ) holds
b1 = b2
proof end;
end;

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

theorem Th31: :: WAYBEL_2:31
for L being non empty RelStr
for x being Element of [:L,L:] holds () . x = (x 1) "/\" (x 2)
proof end;

registration
let L be transitive antisymmetric with_infima RelStr ;
coherence
proof end;
end;

theorem Th32: :: WAYBEL_2:32
for S being non empty RelStr
for D1, D2 being Subset of S holds () .: [: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 (() .: D) = sup (() "/\" ())
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 b1 being Function of [:L,L:],L st
for x, y being Element of L holds b1 . (x,y) = x "\/" y
proof end;
uniqueness
for b1, b2 being Function of [:L,L:],L st ( for x, y being Element of L holds b1 . (x,y) = x "\/" y ) & ( for x, y being Element of L holds b2 . (x,y) = x "\/" y ) holds
b1 = b2
proof end;
end;

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

theorem Th34: :: WAYBEL_2:34
for L being non empty RelStr
for x being Element of [:L,L:] holds () . x = (x 1) "\/" (x 2)
proof end;

registration
let L be transitive antisymmetric with_suprema RelStr ;
coherence
proof end;
end;

theorem Th35: :: WAYBEL_2:35
for S being non empty RelStr
for D1, D2 being Subset of S holds () .: [: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 (() .: D) = inf (() "\/" ())
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
coherence
for b1 being 1 -element reflexive RelStr holds b1 is satisfying_MC
by STRUCT_0:def 10;
end;

registration
coherence
for b1 being non empty reflexive RelStr st b1 is meet-continuous holds
( b1 is up-complete & b1 is satisfying_MC )
;
coherence
for b1 being non empty reflexive RelStr st b1 is up-complete & b1 is satisfying_MC holds
b1 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;
coherence
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 (x "/\" ())
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 (x "/\" ()) ) 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;
coherence 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;
coherence 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 ;

:: 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 (x "/\" ()) )
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 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
coherence
for b1 being non empty Poset st b1 is complete & b1 is Heyting holds
( b1 is meet-continuous & b1 is distributive )
by Th56;
coherence
for b1 being non empty Poset st b1 is complete & b1 is meet-continuous & b1 is distributive holds
b1 is Heyting
by Th56;
end;