:: by Piotr Rudnicki

::

:: Received July 21, 1998

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

Lm1: for L being complete LATTICE

for X being set st X c= bool the carrier of L holds

"/\" ((union X),L) = "/\" ( { (inf Y) where Y is Subset of L : Y in X } ,L)

proof end;

Lm2: for L being complete LATTICE

for X being set st X c= bool the carrier of L holds

"\/" ((union X),L) = "\/" ( { (sup Y) where Y is Subset of L : Y in X } ,L)

proof end;

theorem Th1: :: WAYBEL22:1

for L being upper-bounded Semilattice

for F being non empty directed Subset of (InclPoset (Filt L)) holds sup F = union F

for F being non empty directed Subset of (InclPoset (Filt L)) holds sup F = union F

proof end;

theorem Th2: :: WAYBEL22:2

for L, S, T being non empty complete Poset

for f being CLHomomorphism of L,S

for g being CLHomomorphism of S,T holds g * f is CLHomomorphism of L,T

for f being CLHomomorphism of L,S

for g being CLHomomorphism of S,T holds g * f is CLHomomorphism of L,T

proof end;

theorem Th6: :: WAYBEL22:6

for L being non empty upper-bounded with_infima Poset holds InclPoset (Filt L) is CLSubFrame of BoolePoset the carrier of L

proof end;

registration

let L be non empty upper-bounded with_infima Poset;

coherence

InclPoset (Filt L) is continuous

end;
coherence

InclPoset (Filt L) is continuous

proof end;

registration

let L be non empty upper-bounded Poset;

coherence

for b_{1} being Element of (InclPoset (Filt L)) holds not b_{1} is empty

end;
coherence

for b

proof end;

definition

let S be non empty complete continuous Poset;

let A be set ;

end;
let A be set ;

pred A is_FreeGen_set_of S means :: WAYBEL22:def 1

for T being non empty complete continuous Poset

for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st

( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds

h9 = h ) );

for T being non empty complete continuous Poset

for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st

( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds

h9 = h ) );

:: deftheorem defines is_FreeGen_set_of WAYBEL22:def 1 :

for S being non empty complete continuous Poset

for A being set holds

( A is_FreeGen_set_of S iff for T being non empty complete continuous Poset

for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st

( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds

h9 = h ) ) );

for S being non empty complete continuous Poset

for A being set holds

( A is_FreeGen_set_of S iff for T being non empty complete continuous Poset

for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st

( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds

h9 = h ) ) );

theorem Th7: :: WAYBEL22:7

for S being non empty complete continuous Poset

for A being set st A is_FreeGen_set_of S holds

A is Subset of S

for A being set st A is_FreeGen_set_of S holds

A is Subset of S

proof end;

theorem Th8: :: WAYBEL22:8

for S being non empty complete continuous Poset

for A being set st A is_FreeGen_set_of S holds

for h9 being CLHomomorphism of S,S st h9 | A = id A holds

h9 = id S

for A being set st A is_FreeGen_set_of S holds

for h9 being CLHomomorphism of S,S st h9 | A = id A holds

h9 = id S

proof end;

definition

let X be set ;

{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } is Subset-Family of (BoolePoset X)

end;
func FixedUltraFilters X -> Subset-Family of (BoolePoset X) equals :: WAYBEL22:def 2

{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } ;

coherence { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } ;

{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } is Subset-Family of (BoolePoset X)

proof end;

:: deftheorem defines FixedUltraFilters WAYBEL22:def 2 :

for X being set holds FixedUltraFilters X = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } ;

for X being set holds FixedUltraFilters X = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } ;

theorem Th11: :: WAYBEL22:11

for X being set

for F being Filter of (BoolePoset X) holds F = "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X))))

for F being Filter of (BoolePoset X) holds F = "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X))))

proof end;

definition

let X be set ;

let L be non empty complete continuous Poset;

let f be Function of (FixedUltraFilters X), the carrier of L;

ex b_{1} being Function of (InclPoset (Filt (BoolePoset X))),L st

for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b_{1} . Fi = "\/" ( { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in Fi } ,L)

for b_{1}, b_{2} being Function of (InclPoset (Filt (BoolePoset X))),L st ( for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b_{1} . Fi = "\/" ( { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in Fi } ,L) ) & ( for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b_{2} . Fi = "\/" ( { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in Fi } ,L) ) holds

b_{1} = b_{2}

end;
let L be non empty complete continuous Poset;

let f be Function of (FixedUltraFilters X), the carrier of L;

func f -extension_to_hom -> Function of (InclPoset (Filt (BoolePoset X))),L means :Def3: :: WAYBEL22:def 3

for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it . Fi = "\/" ( { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in Fi } ,L);

existence for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it . Fi = "\/" ( { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in Fi } ,L);

ex b

for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in Fi } ,L)

proof end;

uniqueness for b

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in Fi } ,L) ) & ( for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in Fi } ,L) ) holds

b

proof end;

:: deftheorem Def3 defines -extension_to_hom WAYBEL22:def 3 :

for X being set

for L being non empty complete continuous Poset

for f being Function of (FixedUltraFilters X), the carrier of L

for b_{4} being Function of (InclPoset (Filt (BoolePoset X))),L holds

( b_{4} = f -extension_to_hom iff for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b_{4} . Fi = "\/" ( { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in Fi } ,L) );

for X being set

for L being non empty complete continuous Poset

for f being Function of (FixedUltraFilters X), the carrier of L

for b

( b

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in Fi } ,L) );

theorem :: WAYBEL22:12

for X being set

for L being non empty complete continuous Poset

for f being Function of (FixedUltraFilters X), the carrier of L holds f -extension_to_hom is monotone

for L being non empty complete continuous Poset

for f being Function of (FixedUltraFilters X), the carrier of L holds f -extension_to_hom is monotone

proof end;

theorem Th13: :: WAYBEL22:13

for X being set

for L being non empty complete continuous Poset

for f being Function of (FixedUltraFilters X), the carrier of L holds (f -extension_to_hom) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L

for L being non empty complete continuous Poset

for f being Function of (FixedUltraFilters X), the carrier of L holds (f -extension_to_hom) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L

proof end;

registration

let X be set ;

let L be non empty complete continuous Poset;

let f be Function of (FixedUltraFilters X), the carrier of L;

coherence

f -extension_to_hom is directed-sups-preserving

end;
let L be non empty complete continuous Poset;

let f be Function of (FixedUltraFilters X), the carrier of L;

coherence

f -extension_to_hom is directed-sups-preserving

proof end;

registration

let X be set ;

let L be non empty complete continuous Poset;

let f be Function of (FixedUltraFilters X), the carrier of L;

coherence

f -extension_to_hom is infs-preserving

end;
let L be non empty complete continuous Poset;

let f be Function of (FixedUltraFilters X), the carrier of L;

coherence

f -extension_to_hom is infs-preserving

proof end;

theorem Th14: :: WAYBEL22:14

for X being set

for L being non empty complete continuous Poset

for f being Function of (FixedUltraFilters X), the carrier of L holds (f -extension_to_hom) | (FixedUltraFilters X) = f

for L being non empty complete continuous Poset

for f being Function of (FixedUltraFilters X), the carrier of L holds (f -extension_to_hom) | (FixedUltraFilters X) = f

proof end;

theorem Th15: :: WAYBEL22:15

for X being set

for L being non empty complete continuous Poset

for f being Function of (FixedUltraFilters X), the carrier of L

for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds

h = f -extension_to_hom

for L being non empty complete continuous Poset

for f being Function of (FixedUltraFilters X), the carrier of L

for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds

h = f -extension_to_hom

proof end;

theorem Th17: :: WAYBEL22:17

for L, M being complete continuous LATTICE

for F, G being set st F is_FreeGen_set_of L & G is_FreeGen_set_of M & card F = card G holds

L,M are_isomorphic

for F, G being set st F is_FreeGen_set_of L & G is_FreeGen_set_of M & card F = card G holds

L,M are_isomorphic

proof end;

:: Representation Theorem for Free Continuous Lattices

theorem :: WAYBEL22:18

for X being set

for L being complete continuous LATTICE

for G being set st G is_FreeGen_set_of L & card G = card X holds

L, InclPoset (Filt (BoolePoset X)) are_isomorphic

for L being complete continuous LATTICE

for G being set st G is_FreeGen_set_of L & card G = card X holds

L, InclPoset (Filt (BoolePoset X)) are_isomorphic

proof end;