:: WAYBEL22 semantic presentation

Lemma1: for b₁ being complete LATTICE
for b₂ being set st b₂ c= bool the carrier of b₁ holds
"/\" (union b₂),b₁ = "/\" { (inf b₃) where B is Subset of b₁ : b₃ in b₂ } ,b₁

proof end;

Lemma2: for b₁ being complete LATTICE
for b₂ being set st b₂ c= bool the carrier of b₁ holds
"\/" (union b₂),b₁ = "\/" { (sup b₃) where B is Subset of b₁ : b₃ in b₂ } ,b₁

proof end;

theorem Th1: :: WAYBEL22:1

for b₁ being upper-bounded Semilattice
for b₂ being non empty directed Subset of (InclPoset (Filt b₁)) holds sup b₂ = union b₂

proof end;

theorem Th2: :: WAYBEL22:2

for b₁, b₂, b₃ being non empty complete Poset
for b₄ being CLHomomorphism of b₁,b₂
for b₅ being CLHomomorphism of b₂,b₃ holds b₅ * b₄ is CLHomomorphism of b₁,b₃

proof end;

theorem Th3: :: WAYBEL22:3

for b₁ being non empty RelStr holds id b₁ is infs-preserving

proof end;

theorem Th4: :: WAYBEL22:4

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

proof end;

theorem Th5: :: WAYBEL22:5

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

proof end;

theorem Th6: :: WAYBEL22:6

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

proof end;

registration

let c₁ be non empty upper-bounded with_infima Poset;
cluster InclPoset (Filt a₁) -> continuous ;
coherence

proof end;

end;

registration

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

proof end;

end;

definition

let c₁ be non empty complete continuous Poset;
let c₂ be set ;
pred c₂ is_FreeGen_set_of c₁ means :Def1: :: WAYBEL22:def 1
for b₁ being non empty complete continuous Poset
for b₂ being Function of a₂,the carrier of b₁ ex b₃ being CLHomomorphism of a₁,b₁ st
( b₃ | a₂ = b₂ & ( for b₄ being CLHomomorphism of a₁,b₁ st b₄ | a₂ = b₂ holds
b₄ = b₃ ) );

end;

:: deftheorem Def1 defines is_FreeGen_set_of WAYBEL22:def 1 :

theorem Th7: :: WAYBEL22:7

for b₁ being non empty complete continuous Poset
for b₂ being set st b₂ is_FreeGen_set_of b₁ holds
b₂ is Subset of b₁

proof end;

theorem Th8: :: WAYBEL22:8

for b₁ being non empty complete continuous Poset
for b₂ being set st b₂ is_FreeGen_set_of b₁ holds
for b₃ being CLHomomorphism of b₁,b₁ st b₃ | b₂ = id b₂ holds
b₃ = id b₁

proof end;

definition

let c₁ be set ;
func FixedUltraFilters c₁ -> Subset-Family of (BoolePoset a₁) equals :: WAYBEL22:def 2
{ (uparrow b₁) where B is Element of (BoolePoset a₁) : ex b₁ being Element of a₁ st b₁ = {b₂} } ;
coherence

proof end;

end;

:: deftheorem Def2 defines FixedUltraFilters WAYBEL22:def 2 :

theorem Th9: :: WAYBEL22:9

for b₁ being set holds FixedUltraFilters b₁ c= Filt (BoolePoset b₁)

proof end;

theorem Th10: :: WAYBEL22:10

for b₁ being set holds Card (FixedUltraFilters b₁) = Card b₁

proof end;

theorem Th11: :: WAYBEL22:11

for b₁ being set
for b₂ being Filter of (BoolePoset b₁) holds b₂ = "\/" { ("/\" { (uparrow b₄) where B is Element of (BoolePoset b₁) : ex b₁ being Element of b₁ st
( b₄ = {b₅} & b₅ in b₃ ) } ,(InclPoset (Filt (BoolePoset b₁)))) where B is Subset of b₁ : b₃ in b₂ } ,(InclPoset (Filt (BoolePoset b₁)))

proof end;

definition

let c₁ be set ;
let c₂ be non empty complete continuous Poset;
let c₃ be Function of FixedUltraFilters c₁,the carrier of c₂;
func c₃ -extension_to_hom -> Function of (InclPoset (Filt (BoolePoset a₁))),a₂ means :Def3: :: WAYBEL22:def 3
for b₁ being Element of (InclPoset (Filt (BoolePoset a₁))) holds a₄ . b₁ = "\/" { ("/\" { (a₃ . (uparrow b₃)) where B is Element of (BoolePoset a₁) : ex b₁ being Element of a₁ st
( b₃ = {b₄} & b₄ in b₂ ) } ,a₂) where B is Subset of a₁ : b₂ in b₁ } ,a₂;
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th12: :: WAYBEL22:12

for b₁ being set
for b₂ being non empty complete continuous Poset
for b₃ being Function of FixedUltraFilters b₁,the carrier of b₂ holds b₃ -extension_to_hom is monotone

proof end;

theorem Th13: :: WAYBEL22:13

for b₁ being set
for b₂ being non empty complete continuous Poset
for b₃ being Function of FixedUltraFilters b₁,the carrier of b₂ holds (b₃ -extension_to_hom ) . (Top (InclPoset (Filt (BoolePoset b₁)))) = Top b₂

proof end;

registration

let c₁ be set ;
let c₂ be non empty complete continuous Poset;
let c₃ be Function of FixedUltraFilters c₁,the carrier of c₂;
cluster a₃ -extension_to_hom -> directed-sups-preserving ;
coherence

proof end;

end;

Lemma17: for b₁ being with_non-empty_elements set holds id b₁ is V2 ManySortedSet of b₁
;

registration

let c₁ be set ;
let c₂ be non empty complete continuous Poset;
let c₃ be Function of FixedUltraFilters c₁,the carrier of c₂;
cluster a₃ -extension_to_hom -> infs-preserving directed-sups-preserving ;
coherence

proof end;

end;

theorem Th14: :: WAYBEL22:14

for b₁ being set
for b₂ being non empty complete continuous Poset
for b₃ being Function of FixedUltraFilters b₁,the carrier of b₂ holds (b₃ -extension_to_hom ) | (FixedUltraFilters b₁) = b₃

proof end;

theorem Th15: :: WAYBEL22:15

for b₁ being set
for b₂ being non empty complete continuous Poset
for b₃ being Function of FixedUltraFilters b₁,the carrier of b₂
for b₄ being CLHomomorphism of InclPoset (Filt (BoolePoset b₁)),b₂ st b₄ | (FixedUltraFilters b₁) = b₃ holds
b₄ = b₃ -extension_to_hom

proof end;

theorem Th16: :: WAYBEL22:16

for b₁ being set holds FixedUltraFilters b₁ is_FreeGen_set_of InclPoset (Filt (BoolePoset b₁))

proof end;

theorem Th17: :: WAYBEL22:17

for b₁, b₂ being complete continuous LATTICE
for b₃, b₄ being set st b₃ is_FreeGen_set_of b₁ & b₄ is_FreeGen_set_of b₂ & Card b₃ = Card b₄ holds
b₁,b₂ are_isomorphic

proof end;

theorem Th18: :: WAYBEL22:18

for b₁ being set
for b₂ being complete continuous LATTICE
for b₃ being set st b₃ is_FreeGen_set_of b₂ & Card b₃ = Card b₁ holds
b₂, InclPoset (Filt (BoolePoset b₁)) are_isomorphic

proof end;