:: Representation theorem for free continuous lattices
:: by Piotr Rudnicki
::
:: Received July 21, 1998
:: Copyright (c) 1998-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies REWRITE1, WAYBEL_0, TARSKI, ZFMISC_1, STRUCT_0, LATTICES,
ORDINAL2, SUBSET_1, EQREL_1, XBOOLE_0, YELLOW_1, ARYTM_0, ORDERS_2,
WAYBEL16, RELAT_1, YELLOW_0, LATTICE3, WAYBEL_5, WELLORD2, CARD_FIL,
WELLORD1, CAT_1, SETFAM_1, XXREAL_0, FUNCT_1, CARD_1, SEQM_3, PBOOLE,
FUNCOP_1, YELLOW_2, CARD_3, FUNCT_6, WAYBEL22, FUNCT_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_6, ORDERS_1, STRUCT_0,
WELLORD1, CARD_1, CARD_3, ORDERS_2, LATTICE3, FUNCOP_1, YELLOW_0,
YELLOW_1, YELLOW_2, YELLOW_7, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_5,
WAYBEL16;
constructors DOMAIN_1, TOLER_1, ORDERS_3, PRALG_3, WAYBEL_5, WAYBEL_8,
WAYBEL16, RELSET_1, WAYBEL20;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, FUNCOP_1, CARD_3, PBOOLE,
STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_5, YELLOW_7,
WAYBEL_8, WAYBEL16, FUNCT_1, RELAT_1;
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;
registration
let L be upper-bounded with_infima non empty Poset;
cluster InclPoset Filt L -> continuous;
end;
registration
let L be upper-bounded non empty Poset;
cluster -> non empty for Element of InclPoset Filt L;
end;
begin :: Free generators of continuous lattices
definition
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 h9 being CLHomomorphism of S,T st h9|A = f holds h9 = 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 h9 being CLHomomorphism of S, S st h9|A = id A holds
h9 = 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 -> Function 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;
registration :: 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;
registration :: 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;
::$N Representation Theorem for Free Continuous Lattices
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;