:: by Robert Milewski

::

:: Received November 28, 1998

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

begin

theorem Th1: :: WAYBEL23:1

for L being non empty Poset

for x being Element of L holds compactbelow x = (waybelow x) /\ the carrier of (CompactSublatt L)

for x being Element of L holds compactbelow x = (waybelow x) /\ the carrier of (CompactSublatt L)

proof end;

definition

let L be non empty reflexive transitive RelStr ;

let X be Subset of (InclPoset (Ids L));

:: original: union

redefine func union X -> Subset of L;

coherence

union X is Subset of L

end;
let X be Subset of (InclPoset (Ids L));

:: original: union

redefine func union X -> Subset of L;

coherence

union X is Subset of L

proof end;

Lm1: for X being non empty set

for Y being Subset of (InclPoset X) st ex_sup_of Y, InclPoset X holds

union Y c= sup Y

proof end;

theorem Th3: :: WAYBEL23:3

for L being non empty transitive RelStr

for S being non empty full sups-inheriting SubRelStr of L

for X being Subset of L

for Y being Subset of S st X = Y holds

finsups X c= finsups Y

for S being non empty full sups-inheriting SubRelStr of L

for X being Subset of L

for Y being Subset of S st X = Y holds

finsups X c= finsups Y

proof end;

theorem :: WAYBEL23:4

for L being non empty transitive antisymmetric complete RelStr

for S being non empty full sups-inheriting SubRelStr of L

for X being Subset of L

for Y being Subset of S st X = Y holds

finsups X = finsups Y

for S being non empty full sups-inheriting SubRelStr of L

for X being Subset of L

for Y being Subset of S st X = Y holds

finsups X = finsups Y

proof end;

theorem Th5: :: WAYBEL23:5

for L being complete sup-Semilattice

for S being non empty full join-inheriting SubRelStr of L st Bottom L in the carrier of S holds

for X being Subset of L

for Y being Subset of S st X = Y holds

finsups Y c= finsups X

for S being non empty full join-inheriting SubRelStr of L st Bottom L in the carrier of S holds

for X being Subset of L

for Y being Subset of S st X = Y holds

finsups Y c= finsups X

proof end;

theorem Th6: :: WAYBEL23:6

for L being lower-bounded sup-Semilattice

for X being Subset of (InclPoset (Ids L)) holds sup X = downarrow (finsups (union X))

for X being Subset of (InclPoset (Ids L)) holds sup X = downarrow (finsups (union X))

proof end;

theorem Th7: :: WAYBEL23:7

for L being reflexive transitive RelStr

for X being Subset of L holds downarrow (downarrow X) = downarrow X

for X being Subset of L holds downarrow (downarrow X) = downarrow X

proof end;

theorem :: WAYBEL23:8

for L being reflexive transitive RelStr

for X being Subset of L holds uparrow (uparrow X) = uparrow X

for X being Subset of L holds uparrow (uparrow X) = uparrow X

proof end;

theorem :: WAYBEL23:9

for L being non empty reflexive transitive RelStr

for x being Element of L holds downarrow (downarrow x) = downarrow x

for x being Element of L holds downarrow (downarrow x) = downarrow x

proof end;

theorem :: WAYBEL23:10

for L being non empty reflexive transitive RelStr

for x being Element of L holds uparrow (uparrow x) = uparrow x

for x being Element of L holds uparrow (uparrow x) = uparrow x

proof end;

theorem Th11: :: WAYBEL23:11

for L being non empty RelStr

for S being non empty SubRelStr of L

for X being Subset of L

for Y being Subset of S st X = Y holds

downarrow Y c= downarrow X

for S being non empty SubRelStr of L

for X being Subset of L

for Y being Subset of S st X = Y holds

downarrow Y c= downarrow X

proof end;

theorem Th12: :: WAYBEL23:12

for L being non empty RelStr

for S being non empty SubRelStr of L

for X being Subset of L

for Y being Subset of S st X = Y holds

uparrow Y c= uparrow X

for S being non empty SubRelStr of L

for X being Subset of L

for Y being Subset of S st X = Y holds

uparrow Y c= uparrow X

proof end;

theorem :: WAYBEL23:13

for L being non empty RelStr

for S being non empty SubRelStr of L

for x being Element of L

for y being Element of S st x = y holds

downarrow y c= downarrow x

for S being non empty SubRelStr of L

for x being Element of L

for y being Element of S st x = y holds

downarrow y c= downarrow x

proof end;

theorem :: WAYBEL23:14

for L being non empty RelStr

for S being non empty SubRelStr of L

for x being Element of L

for y being Element of S st x = y holds

uparrow y c= uparrow x

for S being non empty SubRelStr of L

for x being Element of L

for y being Element of S st x = y holds

uparrow y c= uparrow x

proof end;

begin

:: deftheorem Def1 defines meet-closed WAYBEL23:def 1 :

for L being non empty RelStr

for S being Subset of L holds

( S is meet-closed iff subrelstr S is meet-inheriting );

for L being non empty RelStr

for S being Subset of L holds

( S is meet-closed iff subrelstr S is meet-inheriting );

:: deftheorem Def2 defines join-closed WAYBEL23:def 2 :

for L being non empty RelStr

for S being Subset of L holds

( S is join-closed iff subrelstr S is join-inheriting );

for L being non empty RelStr

for S being Subset of L holds

( S is join-closed iff subrelstr S is join-inheriting );

:: deftheorem Def3 defines infs-closed WAYBEL23:def 3 :

for L being non empty RelStr

for S being Subset of L holds

( S is infs-closed iff subrelstr S is infs-inheriting );

for L being non empty RelStr

for S being Subset of L holds

( S is infs-closed iff subrelstr S is infs-inheriting );

:: deftheorem Def4 defines sups-closed WAYBEL23:def 4 :

for L being non empty RelStr

for S being Subset of L holds

( S is sups-closed iff subrelstr S is sups-inheriting );

for L being non empty RelStr

for S being Subset of L holds

( S is sups-closed iff subrelstr S is sups-inheriting );

registration

let L be non empty RelStr ;

coherence

for b_{1} being Subset of L st b_{1} is infs-closed holds

b_{1} is meet-closed

for b_{1} being Subset of L st b_{1} is sups-closed holds

b_{1} is join-closed

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

registration

let L be non empty RelStr ;

existence

ex b_{1} being Subset of L st

( b_{1} is infs-closed & b_{1} is sups-closed & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

theorem Th15: :: WAYBEL23:15

for L being non empty RelStr

for S being Subset of L holds

( S is meet-closed iff for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds

inf {x,y} in S )

for S being Subset of L holds

( S is meet-closed iff for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds

inf {x,y} in S )

proof end;

theorem Th16: :: WAYBEL23:16

for L being non empty RelStr

for S being Subset of L holds

( S is join-closed iff for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds

sup {x,y} in S )

for S being Subset of L holds

( S is join-closed iff for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds

sup {x,y} in S )

proof end;

theorem :: WAYBEL23:17

for L being antisymmetric with_infima RelStr

for S being Subset of L holds

( S is meet-closed iff for x, y being Element of L st x in S & y in S holds

inf {x,y} in S )

for S being Subset of L holds

( S is meet-closed iff for x, y being Element of L st x in S & y in S holds

inf {x,y} in S )

proof end;

theorem Th18: :: WAYBEL23:18

for L being antisymmetric with_suprema RelStr

for S being Subset of L holds

( S is join-closed iff for x, y being Element of L st x in S & y in S holds

sup {x,y} in S )

for S being Subset of L holds

( S is join-closed iff for x, y being Element of L st x in S & y in S holds

sup {x,y} in S )

proof end;

theorem :: WAYBEL23:19

for L being non empty RelStr

for S being Subset of L holds

( S is infs-closed iff for X being Subset of S st ex_inf_of X,L holds

"/\" (X,L) in S )

for S being Subset of L holds

( S is infs-closed iff for X being Subset of S st ex_inf_of X,L holds

"/\" (X,L) in S )

proof end;

theorem :: WAYBEL23:20

for L being non empty RelStr

for S being Subset of L holds

( S is sups-closed iff for X being Subset of S st ex_sup_of X,L holds

"\/" (X,L) in S )

for S being Subset of L holds

( S is sups-closed iff for X being Subset of S st ex_sup_of X,L holds

"\/" (X,L) in S )

proof end;

theorem Th21: :: WAYBEL23:21

for L being non empty transitive RelStr

for S being non empty infs-closed Subset of L

for X being Subset of S st ex_inf_of X,L holds

( ex_inf_of X, subrelstr S & "/\" (X,(subrelstr S)) = "/\" (X,L) )

for S being non empty infs-closed Subset of L

for X being Subset of S st ex_inf_of X,L holds

( ex_inf_of X, subrelstr S & "/\" (X,(subrelstr S)) = "/\" (X,L) )

proof end;

theorem Th22: :: WAYBEL23:22

for L being non empty transitive RelStr

for S being non empty sups-closed Subset of L

for X being Subset of S st ex_sup_of X,L holds

( ex_sup_of X, subrelstr S & "\/" (X,(subrelstr S)) = "\/" (X,L) )

for S being non empty sups-closed Subset of L

for X being Subset of S st ex_sup_of X,L holds

( ex_sup_of X, subrelstr S & "\/" (X,(subrelstr S)) = "\/" (X,L) )

proof end;

theorem :: WAYBEL23:23

for L being non empty transitive RelStr

for S being non empty meet-closed Subset of L

for x, y being Element of S st ex_inf_of {x,y},L holds

( ex_inf_of {x,y}, subrelstr S & "/\" ({x,y},(subrelstr S)) = "/\" ({x,y},L) )

for S being non empty meet-closed Subset of L

for x, y being Element of S st ex_inf_of {x,y},L holds

( ex_inf_of {x,y}, subrelstr S & "/\" ({x,y},(subrelstr S)) = "/\" ({x,y},L) )

proof end;

theorem :: WAYBEL23:24

for L being non empty transitive RelStr

for S being non empty join-closed Subset of L

for x, y being Element of S st ex_sup_of {x,y},L holds

( ex_sup_of {x,y}, subrelstr S & "\/" ({x,y},(subrelstr S)) = "\/" ({x,y},L) )

for S being non empty join-closed Subset of L

for x, y being Element of S st ex_sup_of {x,y},L holds

( ex_sup_of {x,y}, subrelstr S & "\/" ({x,y},(subrelstr S)) = "\/" ({x,y},L) )

proof end;

theorem Th25: :: WAYBEL23:25

for L being transitive antisymmetric with_infima RelStr

for S being non empty meet-closed Subset of L holds subrelstr S is with_infima

for S being non empty meet-closed Subset of L holds subrelstr S is with_infima

proof end;

theorem Th26: :: WAYBEL23:26

for L being transitive antisymmetric with_suprema RelStr

for S being non empty join-closed Subset of L holds subrelstr S is with_suprema

for S being non empty join-closed Subset of L holds subrelstr S is with_suprema

proof end;

registration

let L be transitive antisymmetric with_infima RelStr ;

let S be non empty meet-closed Subset of L;

coherence

subrelstr S is with_infima by Th25;

end;
let S be non empty meet-closed Subset of L;

coherence

subrelstr S is with_infima by Th25;

registration

let L be transitive antisymmetric with_suprema RelStr ;

let S be non empty join-closed Subset of L;

coherence

subrelstr S is with_suprema by Th26;

end;
let S be non empty join-closed Subset of L;

coherence

subrelstr S is with_suprema by Th26;

theorem :: WAYBEL23:27

for L being non empty transitive antisymmetric complete RelStr

for S being non empty infs-closed Subset of L

for X being Subset of S holds "/\" (X,(subrelstr S)) = "/\" (X,L)

for S being non empty infs-closed Subset of L

for X being Subset of S holds "/\" (X,(subrelstr S)) = "/\" (X,L)

proof end;

theorem :: WAYBEL23:28

for L being non empty transitive antisymmetric complete RelStr

for S being non empty sups-closed Subset of L

for X being Subset of S holds "\/" (X,(subrelstr S)) = "\/" (X,L)

for S being non empty sups-closed Subset of L

for X being Subset of S holds "\/" (X,(subrelstr S)) = "\/" (X,L)

proof end;

registration

let L be Semilattice;

coherence

for b_{1} being Subset of L st b_{1} is meet-closed holds

b_{1} is filtered
by Th29;

end;
coherence

for b

b

registration

let L be sup-Semilattice;

coherence

for b_{1} being Subset of L st b_{1} is join-closed holds

b_{1} is directed
by Th30;

end;
coherence

for b

b

theorem :: WAYBEL23:31

for L being Semilattice

for S being non empty upper Subset of L holds

( S is Filter of L iff S is meet-closed )

for S being non empty upper Subset of L holds

( S is Filter of L iff S is meet-closed )

proof end;

theorem :: WAYBEL23:32

for L being sup-Semilattice

for S being non empty lower Subset of L holds

( S is Ideal of L iff S is join-closed )

for S being non empty lower Subset of L holds

( S is Ideal of L iff S is join-closed )

proof end;

registration

let L be sup-Semilattice;

let x be Element of L;

coherence

downarrow x is join-closed by Th35;

coherence

uparrow x is join-closed by Th37;

end;
let x be Element of L;

coherence

downarrow x is join-closed by Th35;

coherence

uparrow x is join-closed by Th37;

registration

let L be Semilattice;

let x be Element of L;

coherence

downarrow x is meet-closed by Th36;

coherence

uparrow x is meet-closed by Th38;

end;
let x be Element of L;

coherence

downarrow x is meet-closed by Th36;

coherence

uparrow x is meet-closed by Th38;

registration

let L be sup-Semilattice;

let x be Element of L;

coherence

waybelow x is join-closed by Th39;

coherence

wayabove x is join-closed by Th41;

end;
let x be Element of L;

coherence

waybelow x is join-closed by Th39;

coherence

wayabove x is join-closed by Th41;

registration
end;

begin

definition

let T be TopStruct ;

meet { (card B) where B is Basis of T : verum } is Cardinal

end;
func weight T -> Cardinal equals :: WAYBEL23:def 5

meet { (card B) where B is Basis of T : verum } ;

coherence meet { (card B) where B is Basis of T : verum } ;

meet { (card B) where B is Basis of T : verum } is Cardinal

proof end;

:: deftheorem defines weight WAYBEL23:def 5 :

for T being TopStruct holds weight T = meet { (card B) where B is Basis of T : verum } ;

for T being TopStruct holds weight T = meet { (card B) where B is Basis of T : verum } ;

definition
end;

:: deftheorem defines second-countable WAYBEL23:def 6 :

for T being TopStruct holds

( T is second-countable iff weight T c= omega );

for T being TopStruct holds

( T is second-countable iff weight T c= omega );

definition

let L be continuous sup-Semilattice;

ex b_{1} being Subset of L st

( b_{1} is join-closed & ( for x being Element of L holds x = sup ((waybelow x) /\ b_{1}) ) )

end;
mode CLbasis of L -> Subset of L means :Def7: :: WAYBEL23:def 7

( it is join-closed & ( for x being Element of L holds x = sup ((waybelow x) /\ it) ) );

existence ( it is join-closed & ( for x being Element of L holds x = sup ((waybelow x) /\ it) ) );

ex b

( b

proof end;

:: deftheorem Def7 defines CLbasis WAYBEL23:def 7 :

for L being continuous sup-Semilattice

for b_{2} being Subset of L holds

( b_{2} is CLbasis of L iff ( b_{2} is join-closed & ( for x being Element of L holds x = sup ((waybelow x) /\ b_{2}) ) ) );

for L being continuous sup-Semilattice

for b

( b

:: deftheorem Def8 defines with_bottom WAYBEL23:def 8 :

for L being non empty RelStr

for S being Subset of L holds

( S is with_bottom iff Bottom L in S );

for L being non empty RelStr

for S being Subset of L holds

( S is with_bottom iff Bottom L in S );

:: deftheorem Def9 defines with_top WAYBEL23:def 9 :

for L being non empty RelStr

for S being Subset of L holds

( S is with_top iff Top L in S );

for L being non empty RelStr

for S being Subset of L holds

( S is with_top iff Top L in S );

registration

let L be non empty RelStr ;

coherence

for b_{1} being Subset of L st b_{1} is with_bottom holds

not b_{1} is empty
by Def8;

end;
coherence

for b

not b

registration

let L be non empty RelStr ;

coherence

for b_{1} being Subset of L st b_{1} is with_top holds

not b_{1} is empty
by Def9;

end;
coherence

for b

not b

registration

let L be non empty RelStr ;

existence

ex b_{1} being Subset of L st b_{1} is with_bottom

ex b_{1} being Subset of L st b_{1} is with_top

end;
existence

ex b

proof end;

existence ex b

proof end;

registration

let L be continuous sup-Semilattice;

existence

ex b_{1} being CLbasis of L st b_{1} is with_bottom

ex b_{1} being CLbasis of L st b_{1} is with_top

end;
existence

ex b

proof end;

existence ex b

proof end;

theorem Th42: :: WAYBEL23:42

for L being non empty antisymmetric lower-bounded RelStr

for S being with_bottom Subset of L holds subrelstr S is lower-bounded

for S being with_bottom Subset of L holds subrelstr S is lower-bounded

proof end;

registration

let L be non empty antisymmetric lower-bounded RelStr ;

let S be with_bottom Subset of L;

coherence

subrelstr S is lower-bounded by Th42;

end;
let S be with_bottom Subset of L;

coherence

subrelstr S is lower-bounded by Th42;

registration

let L be continuous sup-Semilattice;

coherence

for b_{1} being CLbasis of L holds b_{1} is join-closed
by Def7;

end;
coherence

for b

registration

ex b_{1} being continuous LATTICE st

( b_{1} is bounded & not b_{1} is trivial )
end;

cluster non empty non trivial reflexive transitive antisymmetric upper-bounded bounded with_suprema with_infima up-complete satisfying_axiom_of_approximation continuous for RelStr ;

existence ex b

( b

proof end;

registration

let L be non trivial lower-bounded continuous sup-Semilattice;

coherence

for b_{1} being CLbasis of L holds not b_{1} is empty

end;
coherence

for b

proof end;

theorem Th44: :: WAYBEL23:44

for L being lower-bounded algebraic LATTICE holds the carrier of (CompactSublatt L) is with_bottom CLbasis of L

proof end;

theorem :: WAYBEL23:45

for L being lower-bounded continuous sup-Semilattice st the carrier of (CompactSublatt L) is CLbasis of L holds

L is algebraic

L is algebraic

proof end;

theorem Th46: :: WAYBEL23:46

for L being lower-bounded continuous LATTICE

for B being join-closed Subset of L holds

( B is CLbasis of L iff for x, y being Element of L st not y <= x holds

ex b being Element of L st

( b in B & not b <= x & b << y ) )

for B being join-closed Subset of L holds

( B is CLbasis of L iff for x, y being Element of L st not y <= x holds

ex b being Element of L st

( b in B & not b <= x & b << y ) )

proof end;

theorem Th47: :: WAYBEL23:47

for L being lower-bounded continuous LATTICE

for B being join-closed Subset of L st Bottom L in B holds

( B is CLbasis of L iff for x, y being Element of L st x << y holds

ex b being Element of L st

( b in B & x <= b & b << y ) )

for B being join-closed Subset of L st Bottom L in B holds

( B is CLbasis of L iff for x, y being Element of L st x << y holds

ex b being Element of L st

( b in B & x <= b & b << y ) )

proof end;

Lm2: for L being lower-bounded continuous LATTICE

for B being join-closed Subset of L st Bottom L in B & ( for x, y being Element of L st x << y holds

ex b being Element of L st

( b in B & x <= b & b << y ) ) holds

( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds

ex b being Element of L st

( b in B & not b <= x & b <= y ) ) )

proof end;

Lm3: for L being lower-bounded continuous LATTICE

for B being Subset of L st ( for x, y being Element of L st not y <= x holds

ex b being Element of L st

( b in B & not b <= x & b <= y ) ) holds

for x, y being Element of L st not y <= x holds

ex b being Element of L st

( b in B & not b <= x & b << y )

proof end;

theorem Th48: :: WAYBEL23:48

for L being lower-bounded continuous LATTICE

for B being join-closed Subset of L st Bottom L in B holds

( B is CLbasis of L iff ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds

ex b being Element of L st

( b in B & not b <= x & b <= y ) ) ) )

for B being join-closed Subset of L st Bottom L in B holds

( B is CLbasis of L iff ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds

ex b being Element of L st

( b in B & not b <= x & b <= y ) ) ) )

proof end;

theorem :: WAYBEL23:49

for L being lower-bounded continuous LATTICE

for B being join-closed Subset of L st Bottom L in B holds

( B is CLbasis of L iff for x, y being Element of L st not y <= x holds

ex b being Element of L st

( b in B & not b <= x & b <= y ) )

for B being join-closed Subset of L st Bottom L in B holds

( B is CLbasis of L iff for x, y being Element of L st not y <= x holds

ex b being Element of L st

( b in B & not b <= x & b <= y ) )

proof end;

theorem Th50: :: WAYBEL23:50

for L being lower-bounded sup-Semilattice

for S being non empty full SubRelStr of L st Bottom L in the carrier of S & the carrier of S is join-closed Subset of L holds

for x being Element of L holds (waybelow x) /\ the carrier of S is Ideal of S

for S being non empty full SubRelStr of L st Bottom L in the carrier of S & the carrier of S is join-closed Subset of L holds

for x being Element of L holds (waybelow x) /\ the carrier of S is Ideal of S

proof end;

definition

let L be non empty reflexive transitive RelStr ;

let S be non empty full SubRelStr of L;

ex b_{1} being Function of (InclPoset (Ids S)),L st

for I being Ideal of S holds b_{1} . I = "\/" (I,L)

for b_{1}, b_{2} being Function of (InclPoset (Ids S)),L st ( for I being Ideal of S holds b_{1} . I = "\/" (I,L) ) & ( for I being Ideal of S holds b_{2} . I = "\/" (I,L) ) holds

b_{1} = b_{2}

end;
let S be non empty full SubRelStr of L;

func supMap S -> Function of (InclPoset (Ids S)),L means :Def10: :: WAYBEL23:def 10

for I being Ideal of S holds it . I = "\/" (I,L);

existence for I being Ideal of S holds it . I = "\/" (I,L);

ex b

for I being Ideal of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines supMap WAYBEL23:def 10 :

for L being non empty reflexive transitive RelStr

for S being non empty full SubRelStr of L

for b_{3} being Function of (InclPoset (Ids S)),L holds

( b_{3} = supMap S iff for I being Ideal of S holds b_{3} . I = "\/" (I,L) );

for L being non empty reflexive transitive RelStr

for S being non empty full SubRelStr of L

for b

( b

definition

let L be non empty reflexive transitive RelStr ;

let S be non empty full SubRelStr of L;

ex b_{1} being Function of (InclPoset (Ids S)),(InclPoset (Ids L)) st

for I being Ideal of S ex J being Subset of L st

( I = J & b_{1} . I = downarrow J )

for b_{1}, b_{2} being Function of (InclPoset (Ids S)),(InclPoset (Ids L)) st ( for I being Ideal of S ex J being Subset of L st

( I = J & b_{1} . I = downarrow J ) ) & ( for I being Ideal of S ex J being Subset of L st

( I = J & b_{2} . I = downarrow J ) ) holds

b_{1} = b_{2}

end;
let S be non empty full SubRelStr of L;

func idsMap S -> Function of (InclPoset (Ids S)),(InclPoset (Ids L)) means :Def11: :: WAYBEL23:def 11

for I being Ideal of S ex J being Subset of L st

( I = J & it . I = downarrow J );

existence for I being Ideal of S ex J being Subset of L st

( I = J & it . I = downarrow J );

ex b

for I being Ideal of S ex J being Subset of L st

( I = J & b

proof end;

uniqueness for b

( I = J & b

( I = J & b

b

proof end;

:: deftheorem Def11 defines idsMap WAYBEL23:def 11 :

for L being non empty reflexive transitive RelStr

for S being non empty full SubRelStr of L

for b_{3} being Function of (InclPoset (Ids S)),(InclPoset (Ids L)) holds

( b_{3} = idsMap S iff for I being Ideal of S ex J being Subset of L st

( I = J & b_{3} . I = downarrow J ) );

for L being non empty reflexive transitive RelStr

for S being non empty full SubRelStr of L

for b

( b

( I = J & b

registration
end;

registration
end;

registration
end;

definition

let L be lower-bounded continuous sup-Semilattice;

let B be with_bottom CLbasis of L;

ex b_{1} being Function of L,(InclPoset (Ids (subrelstr B))) st

for x being Element of L holds b_{1} . x = (waybelow x) /\ B

for b_{1}, b_{2} being Function of L,(InclPoset (Ids (subrelstr B))) st ( for x being Element of L holds b_{1} . x = (waybelow x) /\ B ) & ( for x being Element of L holds b_{2} . x = (waybelow x) /\ B ) holds

b_{1} = b_{2}

end;
let B be with_bottom CLbasis of L;

func baseMap B -> Function of L,(InclPoset (Ids (subrelstr B))) means :Def12: :: WAYBEL23:def 12

for x being Element of L holds it . x = (waybelow x) /\ B;

existence for x being Element of L holds it . x = (waybelow x) /\ B;

ex b

for x being Element of L holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def12 defines baseMap WAYBEL23:def 12 :

for L being lower-bounded continuous sup-Semilattice

for B being with_bottom CLbasis of L

for b_{3} being Function of L,(InclPoset (Ids (subrelstr B))) holds

( b_{3} = baseMap B iff for x being Element of L holds b_{3} . x = (waybelow x) /\ B );

for L being lower-bounded continuous sup-Semilattice

for B being with_bottom CLbasis of L

for b

( b

theorem Th51: :: WAYBEL23:51

for L being non empty reflexive transitive RelStr

for S being non empty full SubRelStr of L holds

( dom (supMap S) = Ids S & rng (supMap S) is Subset of L )

for S being non empty full SubRelStr of L holds

( dom (supMap S) = Ids S & rng (supMap S) is Subset of L )

proof end;

theorem Th52: :: WAYBEL23:52

for L being non empty reflexive transitive RelStr

for S being non empty full SubRelStr of L

for x being set holds

( x in dom (supMap S) iff x is Ideal of S )

for S being non empty full SubRelStr of L

for x being set holds

( x in dom (supMap S) iff x is Ideal of S )

proof end;

theorem Th53: :: WAYBEL23:53

for L being non empty reflexive transitive RelStr

for S being non empty full SubRelStr of L holds

( dom (idsMap S) = Ids S & rng (idsMap S) is Subset of (Ids L) )

for S being non empty full SubRelStr of L holds

( dom (idsMap S) = Ids S & rng (idsMap S) is Subset of (Ids L) )

proof end;

theorem Th54: :: WAYBEL23:54

for L being non empty reflexive transitive RelStr

for S being non empty full SubRelStr of L

for x being set holds

( x in dom (idsMap S) iff x is Ideal of S )

for S being non empty full SubRelStr of L

for x being set holds

( x in dom (idsMap S) iff x is Ideal of S )

proof end;

theorem Th55: :: WAYBEL23:55

for L being non empty reflexive transitive RelStr

for S being non empty full SubRelStr of L

for x being set st x in rng (idsMap S) holds

x is Ideal of L

for S being non empty full SubRelStr of L

for x being set st x in rng (idsMap S) holds

x is Ideal of L

proof end;

theorem :: WAYBEL23:56

for L being lower-bounded continuous sup-Semilattice

for B being with_bottom CLbasis of L holds

( dom (baseMap B) = the carrier of L & rng (baseMap B) is Subset of (Ids (subrelstr B)) ) by FUNCT_2:def 1, YELLOW_1:1;

for B being with_bottom CLbasis of L holds

( dom (baseMap B) = the carrier of L & rng (baseMap B) is Subset of (Ids (subrelstr B)) ) by FUNCT_2:def 1, YELLOW_1:1;

theorem :: WAYBEL23:57

for L being lower-bounded continuous sup-Semilattice

for B being with_bottom CLbasis of L

for x being set st x in rng (baseMap B) holds

x is Ideal of (subrelstr B)

for B being with_bottom CLbasis of L

for x being set st x in rng (baseMap B) holds

x is Ideal of (subrelstr B)

proof end;

theorem Th58: :: WAYBEL23:58

for L being non empty up-complete Poset

for S being non empty full SubRelStr of L holds supMap S is monotone

for S being non empty full SubRelStr of L holds supMap S is monotone

proof end;

theorem Th59: :: WAYBEL23:59

for L being non empty reflexive transitive RelStr

for S being non empty full SubRelStr of L holds idsMap S is monotone

for S being non empty full SubRelStr of L holds idsMap S is monotone

proof end;

theorem Th60: :: WAYBEL23:60

for L being lower-bounded continuous sup-Semilattice

for B being with_bottom CLbasis of L holds baseMap B is monotone

for B being with_bottom CLbasis of L holds baseMap B is monotone

proof end;

registration

let L be non empty up-complete Poset;

let S be non empty full SubRelStr of L;

coherence

supMap S is monotone by Th58;

end;
let S be non empty full SubRelStr of L;

coherence

supMap S is monotone by Th58;

registration

let L be non empty reflexive transitive RelStr ;

let S be non empty full SubRelStr of L;

coherence

idsMap S is monotone by Th59;

end;
let S be non empty full SubRelStr of L;

coherence

idsMap S is monotone by Th59;

registration

let L be lower-bounded continuous sup-Semilattice;

let B be with_bottom CLbasis of L;

coherence

baseMap B is monotone by Th60;

end;
let B be with_bottom CLbasis of L;

coherence

baseMap B is monotone by Th60;

theorem Th61: :: WAYBEL23:61

for L being lower-bounded continuous sup-Semilattice

for B being with_bottom CLbasis of L holds idsMap (subrelstr B) is sups-preserving

for B being with_bottom CLbasis of L holds idsMap (subrelstr B) is sups-preserving

proof end;

theorem Th62: :: WAYBEL23:62

for L being non empty up-complete Poset

for S being non empty full SubRelStr of L holds supMap S = (SupMap L) * (idsMap S)

for S being non empty full SubRelStr of L holds supMap S = (SupMap L) * (idsMap S)

proof end;

theorem Th63: :: WAYBEL23:63

for L being lower-bounded continuous sup-Semilattice

for B being with_bottom CLbasis of L holds [(supMap (subrelstr B)),(baseMap B)] is Galois

for B being with_bottom CLbasis of L holds [(supMap (subrelstr B)),(baseMap B)] is Galois

proof end;

theorem Th64: :: WAYBEL23:64

for L being lower-bounded continuous sup-Semilattice

for B being with_bottom CLbasis of L holds

( supMap (subrelstr B) is upper_adjoint & baseMap B is lower_adjoint )

for B being with_bottom CLbasis of L holds

( supMap (subrelstr B) is upper_adjoint & baseMap B is lower_adjoint )

proof end;

theorem Th65: :: WAYBEL23:65

for L being lower-bounded continuous sup-Semilattice

for B being with_bottom CLbasis of L holds rng (supMap (subrelstr B)) = the carrier of L

for B being with_bottom CLbasis of L holds rng (supMap (subrelstr B)) = the carrier of L

proof end;

theorem Th66: :: WAYBEL23:66

for L being lower-bounded continuous sup-Semilattice

for B being with_bottom CLbasis of L holds

( supMap (subrelstr B) is infs-preserving & supMap (subrelstr B) is sups-preserving )

for B being with_bottom CLbasis of L holds

( supMap (subrelstr B) is infs-preserving & supMap (subrelstr B) is sups-preserving )

proof end;

theorem :: WAYBEL23:67

for L being lower-bounded continuous sup-Semilattice

for B being with_bottom CLbasis of L holds baseMap B is sups-preserving by Th64, WAYBEL_1:13;

for B being with_bottom CLbasis of L holds baseMap B is sups-preserving by Th64, WAYBEL_1:13;

registration

let L be lower-bounded continuous sup-Semilattice;

let B be with_bottom CLbasis of L;

coherence

( supMap (subrelstr B) is infs-preserving & supMap (subrelstr B) is sups-preserving ) by Th66;

coherence

baseMap B is sups-preserving by Th64, WAYBEL_1:13;

end;
let B be with_bottom CLbasis of L;

coherence

( supMap (subrelstr B) is infs-preserving & supMap (subrelstr B) is sups-preserving ) by Th66;

coherence

baseMap B is sups-preserving by Th64, WAYBEL_1:13;

theorem Th68: :: WAYBEL23:68

for L being lower-bounded continuous sup-Semilattice

for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt (InclPoset (Ids (subrelstr B)))) = { (downarrow b) where b is Element of (subrelstr B) : verum }

for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt (InclPoset (Ids (subrelstr B)))) = { (downarrow b) where b is Element of (subrelstr B) : verum }

proof end;

theorem :: WAYBEL23:69

for L being lower-bounded continuous sup-Semilattice

for B being with_bottom CLbasis of L holds CompactSublatt (InclPoset (Ids (subrelstr B))), subrelstr B are_isomorphic

for B being with_bottom CLbasis of L holds CompactSublatt (InclPoset (Ids (subrelstr B))), subrelstr B are_isomorphic

proof end;

Lm4: for L being lower-bounded continuous LATTICE st L is algebraic holds

( the carrier of (CompactSublatt L) is with_bottom CLbasis of L & ( for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt L) c= B ) )

proof end;

theorem Th70: :: WAYBEL23:70

for L being lower-bounded continuous LATTICE

for B being with_bottom CLbasis of L st ( for B1 being with_bottom CLbasis of L holds B c= B1 ) holds

for J being Element of (InclPoset (Ids (subrelstr B))) holds J = (waybelow ("\/" (J,L))) /\ B

for B being with_bottom CLbasis of L st ( for B1 being with_bottom CLbasis of L holds B c= B1 ) holds

for J being Element of (InclPoset (Ids (subrelstr B))) holds J = (waybelow ("\/" (J,L))) /\ B

proof end;

Lm5: for L being lower-bounded continuous LATTICE st ex B being with_bottom CLbasis of L st

for B1 being with_bottom CLbasis of L holds B c= B1 holds

L is algebraic

proof end;

theorem :: WAYBEL23:71

for L being lower-bounded continuous LATTICE holds

( L is algebraic iff ( the carrier of (CompactSublatt L) is with_bottom CLbasis of L & ( for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt L) c= B ) ) ) by Lm4, Lm5;

( L is algebraic iff ( the carrier of (CompactSublatt L) is with_bottom CLbasis of L & ( for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt L) c= B ) ) ) by Lm4, Lm5;

theorem :: WAYBEL23:72

for L being lower-bounded continuous LATTICE holds

( L is algebraic iff ex B being with_bottom CLbasis of L st

for B1 being with_bottom CLbasis of L holds B c= B1 )

( L is algebraic iff ex B being with_bottom CLbasis of L st

for B1 being with_bottom CLbasis of L holds B c= B1 )

proof end;