Volume 10, 1998

University of Bialystok

Copyright (c) 1998 Association of Mizar Users

### The abstract of the Mizar article:

### Representation Theorem for Free Continuous Lattices

**by****Piotr Rudnicki**- Received July 21, 1998
- MML identifier: WAYBEL22

- [ Mizar article, MML identifier index ]

environ vocabulary BHSP_3, WAYBEL_0, LATTICES, TARSKI, ORDINAL2, QUANTAL1, YELLOW_1, OPPCAT_1, ORDERS_1, PRE_TOPC, WAYBEL16, FUNCT_1, YELLOW_0, RELAT_1, LATTICE3, WAYBEL_5, WELLORD2, FILTER_0, WELLORD1, BOOLE, CAT_1, SUBSET_1, SETFAM_1, CARD_1, FILTER_1, SEQM_3, AMI_1, ZF_REFLE, PBOOLE, FUNCOP_1, PRALG_1, YELLOW_2, FUNCT_6, CARD_3, FRAENKEL, WAYBEL22; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, STRUCT_0, FUNCT_2, FUNCT_6, PRALG_3, GRCAT_1, WELLORD1, CARD_1, CARD_3, PRE_TOPC, ORDERS_1, LATTICE3, PBOOLE, MSUALG_1, AMI_1, FRAENKEL, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_7, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_5, WAYBEL16; constructors ORDERS_3, TOPS_2, GRCAT_1, TOLER_1, PRALG_3, WAYBEL_1, WAYBEL_5, WAYBEL_8, WAYBEL16; clusters STRUCT_0, FUNCT_1, LATTICE3, PBOOLE, PRALG_1, PRVECT_1, AMI_1, YELLOW_0, YELLOW_7, WAYBEL_0, WAYBEL_3, WAYBEL_5, WAYBEL_8, WAYBEL16, RELSET_1, SUBSET_1, FRAENKEL, XBOOLE_0; requirements SUBSET, BOOLE; begin theorem :: WAYBEL22:1 :: cf. WAYBEL13:9 for L being upper-bounded Semilattice, F being non empty directed Subset of InclPoset Filt L holds sup F = union F; theorem :: WAYBEL22:2 for L, S, T being complete (non empty Poset), f being CLHomomorphism of L, S, g being CLHomomorphism of S, T holds g*f is CLHomomorphism of L, T; theorem :: WAYBEL22:3 for L being non empty RelStr holds id L is infs-preserving; theorem :: WAYBEL22:4 for L being non empty RelStr holds id L is directed-sups-preserving; theorem :: WAYBEL22:5 for L being complete (non empty Poset) holds id L is CLHomomorphism of L, L; theorem :: WAYBEL22:6 for L being upper-bounded with_infima non empty Poset holds InclPoset Filt L is CLSubFrame of BoolePoset the carrier of L; definition let L be upper-bounded with_infima non empty Poset; cluster InclPoset Filt L -> continuous; end; definition let L be upper-bounded non empty Poset; cluster -> non empty Element of InclPoset Filt L; end; begin :: Free generators of continuous lattices definition :: replaces :: WAYBEL16:def 2 let S be continuous complete (non empty Poset); let A be set; pred A is_FreeGen_set_of S means :: WAYBEL22:def 1 for T be continuous complete (non empty Poset) for f be Function of A, the carrier of T ex h be CLHomomorphism of S, T st h|A = f & for h' being CLHomomorphism of S,T st h'|A = f holds h' = h; end; theorem :: WAYBEL22:7 for S being continuous complete (non empty Poset), A being set st A is_FreeGen_set_of S holds A is Subset of S; theorem :: WAYBEL22:8 for S being continuous complete (non empty Poset), A being set st A is_FreeGen_set_of S for h' being CLHomomorphism of S, S st h'|A = id A holds h' = id S; begin :: Representation theorem for free continuous lattices reserve X for set, F for Filter of BoolePoset X, x for Element of BoolePoset X, z for Element of X; definition :: See proof of Theorem 4.17, p. 90 let X; func FixedUltraFilters X -> Subset-Family of BoolePoset X equals :: WAYBEL22:def 2 { uparrow x : ex z st x = {z} }; end; theorem :: WAYBEL22:9 FixedUltraFilters X c= Filt BoolePoset X; theorem :: WAYBEL22:10 Card FixedUltraFilters X = Card X; theorem :: WAYBEL22:11 F = "\/"({"/\"({uparrow x : ex z st x = {z} & z in Y}, InclPoset Filt BoolePoset X) where Y is Subset of X : Y in F}, InclPoset Filt BoolePoset X); definition :: See proof of Theorem 4.17, p. 90 let X; let L be continuous complete (non empty Poset); let f be Function of FixedUltraFilters X, the carrier of L; func f-extension_to_hom -> map of InclPoset Filt BoolePoset X, L means :: WAYBEL22:def 3 for Fi being Element of InclPoset Filt BoolePoset X holds it.Fi = "\/"({"/\"({f.(uparrow x) : ex z st x = {z} & z in Y }, L) where Y is Subset of X : Y in Fi }, L); end; theorem :: WAYBEL22:12 for L being continuous complete (non empty Poset), f being Function of FixedUltraFilters X, the carrier of L holds f-extension_to_hom is monotone; theorem :: WAYBEL22:13 for L being continuous complete (non empty Poset), f being Function of FixedUltraFilters X, the carrier of L holds (f-extension_to_hom).Top (InclPoset Filt BoolePoset X) = Top L; definition :: See proof of Theorem 4.17, p. 91 let X; let L be continuous complete (non empty Poset), f be Function of FixedUltraFilters X, the carrier of L; cluster f-extension_to_hom -> directed-sups-preserving; end; definition :: See proof of Theorem 4.17, p. 91 let X; let L be continuous complete (non empty Poset), f be Function of FixedUltraFilters X, the carrier of L; cluster f-extension_to_hom -> infs-preserving; end; theorem :: WAYBEL22:14 for L being continuous complete (non empty Poset), f being Function of FixedUltraFilters X, the carrier of L holds f-extension_to_hom | FixedUltraFilters X = f; theorem :: WAYBEL22:15 for L being continuous complete (non empty Poset), f being Function of FixedUltraFilters X, the carrier of L, h being CLHomomorphism of InclPoset Filt BoolePoset X, L st h | FixedUltraFilters X = f holds h = f-extension_to_hom; theorem :: WAYBEL22:16 FixedUltraFilters X is_FreeGen_set_of InclPoset Filt BoolePoset X; theorem :: WAYBEL22:17 for L, M being continuous complete LATTICE, 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; theorem :: WAYBEL22:18 :: Theorem 4.17, p. 90-91 for L being continuous complete LATTICE, G being set st G is_FreeGen_set_of L & Card G = Card X holds L, InclPoset Filt BoolePoset X are_isomorphic;

Back to top