WAYBEL_2: Meet-continuous Lattices

:: Meet-continuous Lattices
:: by Artur Korni{\l}owicz
::
:: Received October 10, 1996
:: Copyright (c) 1996-2011 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;
cluster f .: Z -> non empty ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

let C be Chain;
cluster [#] C -> directed ;
coherence ;

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

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 non empty trivial reflexive -> non empty reflexive distributive complemented RelStr ;
coherence

proof end;

end;

registration

cluster non empty trivial strict reflexive transitive antisymmetric non void with_suprema with_infima RelStr ;
existence

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;

begin

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 of L;
func sup N -> Element of L equals :: WAYBEL_2:def 1
Sup ;
coherence ;

end;

:: deftheorem defines sup WAYBEL_2:def 1 :

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

proof end;

proof end;

end;

:: deftheorem Def2 defines FinSups WAYBEL_2:def 2 :

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

proof end;

end;

definition

let L be non empty RelStr ;
let x be Element of L;
let N be non empty NetStr of L;
func x "/\" N -> strict NetStr of 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

proof end;

proof end;

end;

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

theorem Th22: :: WAYBEL_2:22

for L being non empty RelStr
for N being non empty NetStr of 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 of L;
cluster x "/\" N -> non empty strict ;
coherence

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

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

begin

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

proof end;

proof end;

end;

:: deftheorem Def4 defines inf_op WAYBEL_2:def 4 :

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

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

proof end;

proof end;

end;

:: deftheorem Def5 defines sup_op WAYBEL_2:def 5 :

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

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;

begin

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 :

definition

let R be non empty reflexive RelStr ;
attr R is meet-continuous means :Def7: :: WAYBEL_2:def 7
( R is up-complete & R is satisfying_MC );

end;

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

registration

cluster non empty trivial reflexive -> non empty reflexive satisfying_MC RelStr ;
coherence

proof end;

end;

registration

cluster non empty reflexive meet-continuous -> non empty reflexive up-complete satisfying_MC RelStr ;
coherence by Def7;
cluster non empty reflexive up-complete satisfying_MC -> non empty reflexive meet-continuous RelStr ;
coherence by Def7;

end;

registration

cluster non empty trivial strict reflexive transitive antisymmetric non void with_suprema with_infima RelStr ;
existence

proof end;

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;

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

proof end;

end;

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;

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;

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 non empty prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))

proof end;

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;

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;

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;

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;

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;

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;

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;

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 by Th49;

end;

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;

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;

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;

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 by Th53;

end;

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 non empty prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) )

proof end;

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 by Lm1;

end;

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 RelStr ;
coherence by Th56;
cluster non empty reflexive transitive antisymmetric distributive complete meet-continuous -> non empty Heyting RelStr ;
coherence by Th56;

end;