:: WAYBEL22 semantic presentation

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

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

proof end;

theorem Th3: :: WAYBEL22:3

for L being non empty RelStr holds id L is infs-preserving

proof end;

theorem Th4: :: WAYBEL22:4

for L being non empty RelStr holds id L is directed-sups-preserving

proof end;

theorem Th5: :: WAYBEL22:5

for L being non empty complete Poset holds id L is CLHomomorphism of L,L

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;
cluster InclPoset (Filt L) -> continuous ;
coherence

proof end;

end;

registration

let L be non empty upper-bounded Poset;
cluster -> non empty Element of the carrier of (InclPoset (Filt L));
coherence

proof end;

end;

definition

let S be non empty complete continuous Poset;
let A be set ;
pred A is_FreeGen_set_of S means :Def1: :: 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 h' being CLHomomorphism of S,T st h' | A = f holds
h' = h ) );

end;

:: deftheorem Def1 defines is_FreeGen_set_of WAYBEL22:def 1 :

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

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 h' being CLHomomorphism of S,S st h' | A = id A holds
h' = id S

proof end;

definition

let X be set ;
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

proof end;

end;

:: deftheorem defines FixedUltraFilters WAYBEL22:def 2 :

theorem Th9: :: WAYBEL22:9

for X being set holds FixedUltraFilters X c= Filt (BoolePoset X)

proof end;

theorem Th10: :: WAYBEL22:10

for X being set holds Card (FixedUltraFilters X) = Card X

proof end;

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

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

proof end;

uniqueness

proof end;

end;

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

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

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

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;
cluster f -extension_to_hom -> directed-sups-preserving ;
coherence

proof end;

end;

Lm3: for X being with_non-empty_elements set holds id X is V2 ManySortedSet of X
;

registration

let X be set ;
let L be non empty complete continuous Poset;
let f be Function of FixedUltraFilters X,the carrier of L;
cluster f -extension_to_hom -> infs-preserving directed-sups-preserving ;
coherence

proof end;

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

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

proof end;

theorem Th16: :: WAYBEL22:16

for X being set holds FixedUltraFilters X is_FreeGen_set_of InclPoset (Filt (BoolePoset X))

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

proof end;

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

proof end;