:: The Lawson Topology
:: by Grzegorz Bancerek
::
:: Received June 21, 1998
:: Copyright (c) 1998-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 XBOOLE_0, WAYBEL_9, WAYBEL_0, SUBSET_1, CANTOR_1, ORDERS_2,
ZFMISC_1, RELAT_2, PRE_TOPC, STRUCT_0, RLVECT_3, TARSKI, SETFAM_1,
XXREAL_0, REWRITE1, PRELAMB, YELLOW_9, ORDINAL1, RCOMP_1, FINSET_1,
FUNCT_1, RELAT_1, ORDINAL2, YELLOW_0, LATTICES, CAT_1, ARYTM_0, LATTICE3,
SEQM_3, WAYBEL_2, WAYBEL_3, CONNSP_2, TOPS_1, PROB_1, WAYBEL11, DIRAF,
CARD_FIL, YELLOW_1, EQREL_1, COMPTS_1, WAYBEL19, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
FINSET_1, RELSET_1, FUNCT_2, DOMAIN_1, STRUCT_0, ORDERS_2, LATTICE3,
ORDERS_3, PRE_TOPC, TOPS_1, CONNSP_2, BORSUK_1, COMPTS_1, YELLOW_0,
WAYBEL_0, YELLOW_1, CANTOR_1, YELLOW_3, WAYBEL_2, YELLOW_6, YELLOW_7,
WAYBEL_3, WAYBEL_9, WAYBEL11, YELLOW_9;
constructors TOPS_1, TOPS_2, BORSUK_1, LATTICE3, TDLAT_3, CANTOR_1, ORDERS_3,
WAYBEL_3, WAYBEL11, YELLOW_9, COMPTS_1, WAYBEL_2;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, BORSUK_1,
LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_3, WAYBEL_3, YELLOW_6,
WAYBEL11, YELLOW_9, YELLOW12, TOPS_1, PRE_TOPC;
requirements BOOLE, SUBSET, NUMERALS;
begin :: Lower topoplogy
definition :: 1.1. DEFINITION, p. 142 (part I)
let T be non empty TopRelStr;
attr T is lower means
:: WAYBEL19:def 1
the set of all (uparrow x)` where x is Element of T is prebasis of T;
end;
registration
cluster -> lower for 1-element reflexive TopSpace-like TopRelStr;
end;
registration
cluster lower trivial complete strict for TopLattice;
end;
theorem :: WAYBEL19:1
for LL being non empty RelStr ex T being strict correct
TopAugmentation of LL st T is lower;
registration
let R be non empty RelStr;
cluster lower for strict correct TopAugmentation of R;
end;
theorem :: WAYBEL19:2
for L1,L2 being TopSpace-like lower non empty TopRelStr st the
RelStr of L1 = the RelStr of L2 holds the topology of L1 = the topology of L2
;
definition :: 1.1. DEFINITION, p. 142 (part II)
let R be non empty RelStr;
func omega R -> Subset-Family of R means
:: WAYBEL19:def 2
for T being lower correct TopAugmentation of R holds it = the topology of T;
end;
theorem :: WAYBEL19:3
for R1,R2 being non empty RelStr st the RelStr of R1 = the RelStr
of R2 holds omega R1 = omega R2;
theorem :: WAYBEL19:4
for T being lower non empty TopRelStr for x being Point of T
holds (uparrow x)` is open & uparrow x is closed;
theorem :: WAYBEL19:5
for T being transitive lower non empty TopRelStr for A being
Subset of T st A is open holds A is lower;
theorem :: WAYBEL19:6
for T being transitive lower non empty TopRelStr for A being
Subset of T st A is closed holds A is upper;
theorem :: WAYBEL19:7
for T being non empty TopSpace-like TopRelStr holds T is lower
iff {(uparrow F)` where F is Subset of T: F is finite} is Basis of T;
theorem :: WAYBEL19:8
:: 1.2. LEMMA, (i) generalized, p. 143
for S,T being lower complete TopLattice, f being Function of S, T
st for X being non empty Subset of S holds f preserves_inf_of X holds f is
continuous;
theorem :: WAYBEL19:9
:: 1.2. LEMMA (i), p. 143
for S,T being lower complete TopLattice, f being Function of S, T
st f is infs-preserving holds f is continuous;
theorem :: WAYBEL19:10
for T being lower complete TopLattice, BB being prebasis of T
for F being non empty filtered Subset of T st for A being Subset of T st A in
BB & inf F in A holds F meets A holds inf F in Cl F;
theorem :: WAYBEL19:11
:: 1.2. LEMMA (ii), p. 143
for S,T being lower complete TopLattice for f being Function of
S,T st f is continuous holds f is filtered-infs-preserving;
theorem :: WAYBEL19:12
:: 1.2. LEMMA (iii), p. 143
for S,T being lower complete TopLattice for f being Function of S,T st
f is continuous & for X being finite Subset of S holds f preserves_inf_of X
holds f is infs-preserving;
theorem :: WAYBEL19:13
:: Remark before 1.3., p. 143
for T being lower TopSpace-like reflexive transitive non empty
TopRelStr for x being Point of T holds Cl {x} = uparrow x;
definition
mode TopPoset is TopSpace-like reflexive transitive antisymmetric TopRelStr;
end;
registration
:: Remark before 1.3., p. 143
cluster lower -> T_0 for non empty TopPoset;
end;
registration
let R be lower-bounded non empty RelStr;
cluster -> lower-bounded for TopAugmentation of R;
end;
theorem :: WAYBEL19:14
for S, T being non empty RelStr, s being Element of S, t being
Element of T holds (uparrow [s,t])` = [:(uparrow s)`, the carrier of T:] \/ [:
the carrier of S, (uparrow t)`:];
theorem :: WAYBEL19:15
:: 1.3. LEMMA, p. 143 (variant I)
for S,T being lower-bounded non empty Poset for S9 being lower
correct TopAugmentation of S for T9 being lower correct TopAugmentation of T
holds omega [:S,T:] = the topology of [:S9,T9 qua non empty TopSpace:];
theorem :: WAYBEL19:16
:: 1.3. LEMMA, p. 143 (variant II)
for S,T being lower lower-bounded non empty TopPoset holds omega [:S
,T qua Poset:] = the topology of [:S,T qua non empty TopSpace:];
theorem :: WAYBEL19:17
:: 1.4. LEMMA, p. 144:: Refinements
for T,T2 being lower complete TopLattice st T2 is TopAugmentation of
[:T, T qua LATTICE:] for f being Function of T2,T st f = inf_op T holds f is
continuous;
begin :: Refinements
scheme :: WAYBEL19:sch 1
TopInd {T() -> TopLattice, P[set]}: for A being Subset of T() st A is open
holds P[A]
provided
ex K being prebasis of T() st for A being Subset of T() st A in K
holds P[A] and
for F being Subset-Family of T() st for A being Subset of T() st A
in F holds P[A] holds P[union F] and
for A1,A2 being Subset of T() st P[A1] & P[A2] holds P[A1 /\ A2] and
P[[#]T()];
theorem :: WAYBEL19:18
for L1,L2 being up-complete antisymmetric non empty reflexive RelStr
st the RelStr of L1 = the RelStr of L2 & for x being Element of L1 holds
waybelow x is directed non empty holds L1 is satisfying_axiom_of_approximation
implies L2 is satisfying_axiom_of_approximation;
registration
let T be continuous non empty Poset;
cluster -> continuous for TopAugmentation of T;
end;
theorem :: WAYBEL19:19
for T,S being TopSpace, R being Refinement of T,S for W being
Subset of R st W in the topology of T or W in the topology of S holds W is open
;
theorem :: WAYBEL19:20
for T,S being TopSpace, R being Refinement of T,S for V being
Subset of T, W being Subset of R st W = V holds V is open implies W is open;
theorem :: WAYBEL19:21
for T,S being TopSpace st the carrier of T = the carrier of S
for R being Refinement of T,S for V being Subset of T, W being Subset of R st W
= V holds V is closed implies W is closed;
theorem :: WAYBEL19:22
for T being non empty TopSpace, K,O being set st K c= O & O c=
the topology of T holds (K is Basis of T implies O is Basis of T) & (K is
prebasis of T implies O is prebasis of T);
theorem :: WAYBEL19:23
:: YELLOW_9:58 revised
for T1,T2 being non empty TopSpace st the carrier of T1 = the
carrier of T2 for T be Refinement of T1, T2 for B1 being prebasis of T1, B2
being prebasis of T2 holds B1 \/ B2 is prebasis of T;
theorem :: WAYBEL19:24
for T1,S1,T2,S2 being non empty TopSpace for R1 being Refinement of T1
,S1, R2 being Refinement of T2,S2 for f being Function of T1,T2, g being
Function of S1,S2 for h being Function of R1,R2 st h = f & h = g holds f is
continuous & g is continuous implies h is continuous;
theorem :: WAYBEL19:25
for T being non empty TopSpace, K being prebasis of T for N
being net of T, p being Point of T st for A being Subset of T st p in A & A in
K holds N is_eventually_in A holds p in Lim N;
theorem :: WAYBEL19:26
for T being non empty TopSpace for N being net of T for S being
Subset of T st N is_eventually_in S holds Lim N c= Cl S;
theorem :: WAYBEL19:27
for R being non empty RelStr, X being non empty Subset of R
holds the mapping of X+id = id X & the mapping of X opp+id = id X;
theorem :: WAYBEL19:28
for R being reflexive antisymmetric non empty RelStr, x being
Element of R holds (uparrow x) /\ (downarrow x) = {x};
begin :: Lawson topology
definition
let T be reflexive non empty TopRelStr;
attr T is Lawson means
:: WAYBEL19:def 3
(omega T) \/ (sigma T) is prebasis of T;
end;
theorem :: WAYBEL19:29
for R being complete LATTICE for LL being lower correct
TopAugmentation of R for S being Scott TopAugmentation of R for T being correct
TopAugmentation of R holds T is Lawson iff T is Refinement of S,LL;
registration
let R be complete LATTICE;
cluster Lawson strict correct for TopAugmentation of R;
end;
registration
cluster Scott complete strict for TopLattice;
cluster Lawson continuous for complete strict TopLattice;
end;
theorem :: WAYBEL19:30
for T being Lawson complete TopLattice holds (sigma T) \/ the set of all (
uparrow x)` where x is Element of T is prebasis of T;
theorem :: WAYBEL19:31
for T being Lawson complete TopLattice holds (sigma T) \/ {W\uparrow
x where W is Subset of T, x is Element of T: W in sigma T} is prebasis of T;
theorem :: WAYBEL19:32
for T being Lawson complete TopLattice holds {W\uparrow F where W,F
is Subset of T: W in sigma T & F is finite} is Basis of T;
definition :: 1.5. DEFINITION, p. 144 (part II)
let T be complete LATTICE;
func lambda T -> Subset-Family of T means
:: WAYBEL19:def 4
for S being Lawson correct TopAugmentation of T holds it = the topology of S;
end;
theorem :: WAYBEL19:33
for R being complete LATTICE holds lambda R = UniCl FinMeetCl ((
sigma R) \/ (omega R));
theorem :: WAYBEL19:34
for R being complete LATTICE for T being lower correct TopAugmentation
of R for S being Scott correct TopAugmentation of R for M being Refinement of S
,T holds lambda R = the topology of M;
theorem :: WAYBEL19:35
for T being lower up-complete TopLattice for A being Subset of T
st A is open holds A is property(S);
theorem :: WAYBEL19:36
:: Remark after 1.5. p. 144
for T being Lawson complete TopLattice for A being Subset of T
st A is open holds A is property(S);
theorem :: WAYBEL19:37
for S being Scott complete TopLattice for T being Lawson correct
TopAugmentation of S for A being Subset of S st A is open for C being Subset of
T st C = A holds C is open;
theorem :: WAYBEL19:38
for T being Lawson complete TopLattice
for x being Element of T holds
uparrow x is closed & downarrow x is closed & {x} is closed;
theorem :: WAYBEL19:39
for T being Lawson complete TopLattice for x being Element of
T holds (uparrow x)` is open & (downarrow x)` is open & {x}` is open;
theorem :: WAYBEL19:40
for T being Lawson complete continuous TopLattice for x being
Element of T holds wayabove x is open & (wayabove x)` is closed;
theorem :: WAYBEL19:41
:: 1.6. PROPOSITION (i), p. 144
for S being Scott complete TopLattice for T being Lawson correct
TopAugmentation of S for A being upper Subset of T st A is open for C being
Subset of S st C = A holds C is open;
theorem :: WAYBEL19:42
:: 1.6. PROPOSITION (ii), p. 144
for T being Lawson complete TopLattice for A being lower Subset of T
holds A is closed iff A is closed_under_directed_sups;
theorem :: WAYBEL19:43
:: 1.7. LEMMA, p. 145
for T being Lawson complete TopLattice for F being non empty
filtered Subset of T holds Lim (F opp+id) = {inf F};
registration
:: 1.9. THEOREM, p. 146
cluster Lawson -> T_1 compact for complete TopLattice;
end;
registration
:: 1.10. THEOREM, p. 146
cluster Lawson -> Hausdorff for complete continuous TopLattice;
end;