:: Continuous Lattices between T$_0$ Spaces
:: by Grzegorz Bancerek
::
:: Received September 24, 1999
:: Copyright (c) 1999-2018 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 YELLOW_1, PBOOLE, CARD_3, WAYBEL18, WAYBEL_3, XBOOLE_0, PRE_TOPC,
STRUCT_0, ORDERS_2, WAYBEL24, WAYBEL25, RELAT_2, MONOID_0, SUBSET_1,
ORDINAL2, FUNCT_1, XXREAL_0, CAT_1, YELLOW_0, NEWTON, TARSKI, YELLOW_9,
WAYBEL11, ZFMISC_1, CARD_1, RCOMP_1, FUNCT_3, RELAT_1, WELLORD1,
VALUED_1, T_0TOPSP, WAYBEL_0, SEQM_3, BINOP_1, FUNCOP_1, BORSUK_1,
GROUP_6, YELLOW16, TOPS_2, REWRITE1, LATTICE3, EQREL_1, FUNCTOR0,
WAYBEL_1, FUNCT_6, RLVECT_2, FUNCT_2, CANTOR_1, FUNCT_4, WAYBEL_9,
MCART_1, FINSET_1, SETFAM_1, WAYBEL26;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1,
MCART_1, FINSET_1, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, TOPS_2,
FUNCT_3, FUNCT_4, ORDINAL1, NUMBERS, SETFAM_1, FUNCT_2, FUNCOP_1,
STRUCT_0, CARD_3, FUNCT_6, MONOID_0, PRALG_1, FUNCT_7, WELLORD1,
ORDERS_2, LATTICE3, PRE_TOPC, CANTOR_1, T_0TOPSP, BORSUK_1, QUANTAL1,
YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_9, WAYBEL_3,
WAYBEL_9, WAYBEL11, WAYBEL18, WAYBEL24, WAYBEL25, YELLOW16;
constructors TOLER_1, FUNCT_7, TOPS_2, BORSUK_1, T_0TOPSP, CANTOR_1, MONOID_0,
QUANTAL1, ORDERS_3, PRALG_3, WAYBEL_1, WAYBEL11, YELLOW_9, WAYBEL18,
WAYBEL24, WAYBEL25, YELLOW16, XTUPLE_0, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, FINSET_1, STRUCT_0,
PRE_TOPC, BORSUK_1, LATTICE3, YELLOW_0, TSP_1, MONOID_0, WAYBEL_0,
YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_2, WAYBEL_3, YELLOW_6, WAYBEL10,
WAYBEL17, YELLOW_9, WAYBEL18, WAYBEL24, YELLOW14, WAYBEL25, YELLOW16,
FUNCT_1, XTUPLE_0;
requirements SUBSET, BOOLE, NUMERALS;
begin
notation
let I be set;
let J be RelStr-yielding ManySortedSet of I;
synonym I-POS_prod J for product J;
end;
notation
let I be set;
let J be TopStruct-yielding non-Empty ManySortedSet of I;
synonym I-TOP_prod J for product J;
end;
:: 4.1. DEFINITION (a)
definition
let X,Y be non empty TopSpace;
func oContMaps(X, Y) -> non empty strict RelStr equals
:: WAYBEL26:def 1
ContMaps(X, Omega Y);
end;
registration
let X,Y be non empty TopSpace;
cluster oContMaps(X, Y) -> reflexive transitive constituted-Functions;
end;
registration
let X be non empty TopSpace;
let Y be non empty T_0 TopSpace;
cluster oContMaps(X, Y) -> antisymmetric;
end;
theorem :: WAYBEL26:1
for X,Y being non empty TopSpace for a being set holds a is
Element of oContMaps(X, Y) iff a is continuous Function of X, Omega Y;
theorem :: WAYBEL26:2
for X,Y being non empty TopSpace for a being set holds a is
Element of oContMaps(X, Y) iff a is continuous Function of X, Y;
theorem :: WAYBEL26:3 :: see yellow14:9
for X,Y being non empty TopSpace for a,b being Element of
oContMaps(X,Y) for f,g being Function of X, Omega Y st a = f & b = g holds a <=
b iff f <= g;
definition
let X,Y be non empty TopSpace;
let x be Point of X;
let A be Subset of oContMaps(X,Y);
redefine func pi(A,x) -> Subset of Omega Y;
end;
registration
let X,Y be non empty TopSpace;
let x be set;
let A be non empty Subset of oContMaps(X,Y);
cluster pi(A,x) -> non empty;
end;
theorem :: WAYBEL26:4
Omega Sierpinski_Space is TopAugmentation of BoolePoset{0};
theorem :: WAYBEL26:5
for X being non empty TopSpace ex f being Function of InclPoset
the topology of X, oContMaps(X, Sierpinski_Space) st f is isomorphic & for V
being open Subset of X holds f.V = chi(V, the carrier of X);
theorem :: WAYBEL26:6
for X being non empty TopSpace holds InclPoset the topology of X,
oContMaps(X, Sierpinski_Space) are_isomorphic;
:: 4.1. DEFINITION (b)
definition
let X,Y,Z be non empty TopSpace;
let f be continuous Function of Y,Z;
func oContMaps(X, f) -> Function of oContMaps(X, Y), oContMaps(X, Z) means
:: WAYBEL26:def 2
for g being continuous Function of X,Y holds it.g = f*g;
func oContMaps(f, X) -> Function of oContMaps(Z, X), oContMaps(Y, X) means
:: WAYBEL26:def 3
for g being continuous Function of Z, X holds it.g = g*f;
end;
theorem :: WAYBEL26:7
for X being non empty TopSpace for Y being monotone-convergence
T_0-TopSpace holds oContMaps(X, Y) is up-complete;
theorem :: WAYBEL26:8
for X,Y,Z being non empty TopSpace for f being continuous
Function of Y,Z holds oContMaps(X, f) is monotone;
theorem :: WAYBEL26:9
for X,Y being non empty TopSpace for f being continuous Function of Y,
Y st f is idempotent holds oContMaps(X, f) is idempotent;
theorem :: WAYBEL26:10
for X,Y,Z being non empty TopSpace for f being continuous
Function of Y,Z holds oContMaps(f, X) is monotone;
theorem :: WAYBEL26:11
for X,Y being non empty TopSpace for f being continuous Function
of Y,Y st f is idempotent holds oContMaps(f, X) is idempotent;
theorem :: WAYBEL26:12
for X,Y,Z being non empty TopSpace for f being continuous
Function of Y,Z for x being Element of X, A being Subset of oContMaps(X, Y)
holds pi(oContMaps(X,f).:A, x) = f.:pi(A, x);
:: 4.2. LEMMA (ii)
theorem :: WAYBEL26:13
for X being non empty TopSpace for Y,Z being
monotone-convergence T_0-TopSpace for f being continuous Function of Y,Z holds
oContMaps(X, f) is directed-sups-preserving;
theorem :: WAYBEL26:14
for X,Y,Z being non empty TopSpace for f being continuous
Function of Y,Z for x being Element of Y, A being Subset of oContMaps(Z, X)
holds pi(oContMaps(f, X).:A, x) = pi(A, f.x);
theorem :: WAYBEL26:15
for Y,Z being non empty TopSpace for X being
monotone-convergence T_0-TopSpace for f being continuous Function of Y,Z holds
oContMaps(f, X) is directed-sups-preserving;
:: 4.3. LEMMA (i) genralized
theorem :: WAYBEL26:16
for X,Z being non empty TopSpace for Y being non empty SubSpace
of Z holds oContMaps(X, Y) is full SubRelStr of oContMaps(X, Z);
theorem :: WAYBEL26:17
for Z being monotone-convergence T_0-TopSpace for Y being non
empty SubSpace of Z for f being continuous Function of Z,Y st f is
being_a_retraction holds Omega Y is directed-sups-inheriting SubRelStr of Omega
Z;
theorem :: WAYBEL26:18
for X being non empty TopSpace for Z being monotone-convergence
T_0-TopSpace for Y being non empty SubSpace of Z for f being continuous
Function of Z,Y st f is being_a_retraction holds oContMaps(X, f)
is_a_retraction_of oContMaps(X, Z), oContMaps(X, Y);
theorem :: WAYBEL26:19
for X being non empty TopSpace for Z being monotone-convergence
T_0-TopSpace for Y being non empty SubSpace of Z st Y is_a_retract_of Z holds
oContMaps(X, Y) is_a_retract_of oContMaps(X, Z);
theorem :: WAYBEL26:20
for X,Y,Z being non empty TopSpace for f being continuous
Function of Y,Z st f is being_homeomorphism holds oContMaps(X, f) is isomorphic
;
theorem :: WAYBEL26:21
for X,Y,Z being non empty TopSpace st Y,Z are_homeomorphic holds
oContMaps(X, Y), oContMaps(X, Z) are_isomorphic;
:: 4.3. LEMMA (ii)
theorem :: WAYBEL26:22
for X being non empty TopSpace for Z being monotone-convergence
T_0-TopSpace for Y being non empty SubSpace of Z st Y is_a_retract_of Z &
oContMaps(X, Z) is complete continuous holds oContMaps(X, Y) is complete
continuous;
theorem :: WAYBEL26:23
for X being non empty TopSpace for Y,Z being
monotone-convergence T_0-TopSpace st Y is_Retract_of Z & oContMaps(X, Z) is
complete continuous holds oContMaps(X, Y) is complete continuous;
theorem :: WAYBEL26:24
for Y being non trivial T_0-TopSpace st not Y is T_1 holds
Sierpinski_Space is_Retract_of Y;
theorem :: WAYBEL26:25
for X being non empty TopSpace for Y being non trivial
T_0-TopSpace st oContMaps(X, Y) is with_suprema holds not Y is T_1;
registration
cluster Sierpinski_Space -> non trivial monotone-convergence;
end;
registration
cluster injective monotone-convergence non trivial for T_0-TopSpace;
end;
:: 4.4. PROPOSITION
theorem :: WAYBEL26:26
for X being non empty TopSpace for Y being monotone-convergence
non trivial T_0-TopSpace st oContMaps(X, Y) is complete continuous holds
InclPoset the topology of X is continuous;
theorem :: WAYBEL26:27
for X being non empty TopSpace, x being Point of X for Y being
monotone-convergence T_0-TopSpace ex F being directed-sups-preserving
projection Function of oContMaps(X,Y), oContMaps(X,Y) st (for f being
continuous Function of X,Y holds F.f = X --> (f.x)) & ex h being continuous
Function of X,X st h = X --> x & F = oContMaps(h, Y);
:: 4.5. PROPOSITION
theorem :: WAYBEL26:28
for X being non empty TopSpace, Y being monotone-convergence
T_0-TopSpace st oContMaps(X, Y) is complete continuous holds Omega Y is
complete continuous;
theorem :: WAYBEL26:29
for X being non empty 1-sorted, I being non empty set for J
being TopStruct-yielding non-Empty ManySortedSet of I
for f being Function of X,
I-TOP_prod J for i being Element of I holds (commute f).i = proj(J,i)*f;
theorem :: WAYBEL26:30
for S being 1-sorted, M being set holds Carrier (M --> S) = M
--> the carrier of S;
theorem :: WAYBEL26:31
for X,Y being non empty TopSpace, M being non empty set for f
being continuous Function of X, M-TOP_prod (M --> Y) holds commute f is
Function of M, the carrier of oContMaps(X, Y);
theorem :: WAYBEL26:32
for X,Y being non empty TopSpace holds the carrier of oContMaps(
X, Y) c= Funcs(the carrier of X, the carrier of Y);
theorem :: WAYBEL26:33
for X,Y being non empty TopSpace, M being non empty set for f
being Function of M, the carrier of oContMaps(X, Y) holds commute f is
continuous Function of X, M-TOP_prod (M --> Y);
theorem :: WAYBEL26:34
for X being non empty TopSpace, M being non empty set ex F being
Function of oContMaps(X, M-TOP_prod (M --> Sierpinski_Space)), M-POS_prod (M
--> oContMaps(X, Sierpinski_Space)) st F is isomorphic & for f being continuous
Function of X, M-TOP_prod (M --> Sierpinski_Space) holds F.f = commute f;
theorem :: WAYBEL26:35
for X being non empty TopSpace, M being non empty set holds
oContMaps(X, M-TOP_prod (M --> Sierpinski_Space)), M-POS_prod (M --> oContMaps(
X, Sierpinski_Space)) are_isomorphic;
:: 4.6. PROPOSITION
theorem :: WAYBEL26:36
for X being non empty TopSpace st InclPoset the topology of X is
continuous for Y being injective T_0-TopSpace holds oContMaps(X, Y) is complete
continuous;
registration
cluster non trivial complete Scott for TopLattice;
end;
:: 4.7. THEOREM p.129.
theorem :: WAYBEL26:37
for X being non empty TopSpace for L being non trivial complete Scott
TopLattice holds oContMaps(X, L) is complete continuous iff InclPoset the
topology of X is continuous & L is continuous;
registration
let f be Function;
cluster Union disjoin f -> Relation-like;
end;
definition
let f be Function;
func *graph f -> Relation equals
:: WAYBEL26:def 4
(Union disjoin f)~;
end;
reserve x,y for object,
f for Function;
theorem :: WAYBEL26:38
[x,y] in *graph f iff x in dom f & y in f.x;
theorem :: WAYBEL26:39
for X being finite set holds proj1 X is finite & proj2 X is finite;
:: 4.8. LEMMA p.130.
theorem :: WAYBEL26:40
for X,Y being non empty TopSpace for S being Scott
TopAugmentation of InclPoset the topology of Y for f being Function of X, S st
*graph f is open Subset of [:X,Y:] holds f is continuous;
definition
let W be Relation, X be set;
func (W,X)*graph -> Function means
:: WAYBEL26:def 5
dom it = X & for x being object st x in X holds it.x = Im(W,x);
end;
theorem :: WAYBEL26:41
for W being Relation, X being set st dom W c= X holds *graph((W,
X)*graph) = W;
registration
let X, Y be TopSpace;
cluster -> Relation-like for Subset of [:X,Y:];
cluster -> Relation-like for Element of the topology of [:X,Y:];
end;
theorem :: WAYBEL26:42
for X,Y being non empty TopSpace for W being open Subset of [:X,
Y:] for x being Point of X holds Im(W,x) is open Subset of Y;
:: 4.9. PROPOSITION a) p.130.
theorem :: WAYBEL26:43
for X,Y being non empty TopSpace for S being Scott
TopAugmentation of InclPoset the topology of Y for W being open Subset of [:X,Y
:] holds (W, the carrier of X)*graph is continuous Function of X, S;
:: 4.9. PROPOSITION b) p.130.
theorem :: WAYBEL26:44
for X,Y being non empty TopSpace for S being Scott
TopAugmentation of InclPoset the topology of Y for W1, W2 being open Subset of
[:X,Y:] st W1 c= W2 for f1, f2 being Element of oContMaps(X, S) st f1 = (W1,
the carrier of X)*graph & f2 = (W2, the carrier of X)*graph holds f1 <= f2;
:: 4.9. PROPOSITION p.130.
theorem :: WAYBEL26:45
for X,Y being non empty TopSpace for S being Scott TopAugmentation of
InclPoset the topology of Y ex F being Function of InclPoset the topology of [:
X, Y:], oContMaps(X, S) st F is monotone & for W being open Subset of [:X,Y:]
holds F.W = (W, the carrier of X)*graph;