:: Bases and Refinements of Topologies
:: by Grzegorz Bancerek
::
:: Received March 9, 1998
:: Copyright (c) 1998-2026 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, SUBSET_1, ORDERS_2, SETFAM_1, WAYBEL_0, XXREAL_0,
STRUCT_0, PRE_TOPC, FUNCT_1, RELAT_1, TARSKI, REWRITE1, ZFMISC_1,
WAYBEL_9, RELAT_2, NATTRA_1, FINSET_1, LATTICES, FUNCOP_1, YELLOW_0,
ORDINAL2, FUNCT_3, SEQM_3, CAT_1, WELLORD1, ARYTM_0, RLVECT_3, CANTOR_1,
FUNCT_2, RCOMP_1, CONNSP_2, TOPS_1, LATTICE3, BORSUK_1, PRELAMB,
CARD_FIL, PROB_1, YELLOW_6, WAYBEL11, YELLOW_9, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
FINSET_1, MCART_1, RELAT_2, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1,
STRUCT_0, WELLORD1, ORDERS_2, LATTICE3, ORDERS_3, YELLOW_0, WAYBEL_0,
TDLAT_3, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_2, YELLOW_6, YELLOW_7,
WAYBEL_9, WAYBEL11, CANTOR_1, BORSUK_1;
constructors SETFAM_1, TOLER_1, TOPS_1, TOPS_2, BORSUK_1, LATTICE3, TDLAT_3,
CANTOR_1, ORDERS_3, WAYBEL11, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FINSET_1, STRUCT_0,
BORSUK_1, LATTICE3, YELLOW_0, TDLAT_3, TEX_1, WAYBEL_0, YELLOW_2,
YELLOW_6, WAYBEL_9, WAYBEL11, FUNCT_2, CANTOR_1, RELSET_1;
requirements BOOLE, SUBSET;
definitions TARSKI, STRUCT_0, PRE_TOPC, CANTOR_1, ORDERS_2, WAYBEL_0,
WAYBEL_1, TOPS_2, WAYBEL11, XBOOLE_0;
equalities STRUCT_0, YELLOW_0, WAYBEL_0, WAYBEL11, WELLORD1;
expansions TARSKI, STRUCT_0, PRE_TOPC, ORDERS_2, WAYBEL_0, XBOOLE_0;
theorems STRUCT_0, SETFAM_1, ENUMSET1, PRE_TOPC, CANTOR_1, YELLOW_0, WAYBEL_0,
FUNCT_1, RELAT_1, FUNCT_2, TEX_1, ORDERS_2, ZFMISC_1, TARSKI, FINSET_1,
FUNCOP_1, TDLAT_3, BORSUK_1, YELLOW_6, YELLOW_8, TOPS_1, CONNSP_2,
WAYBEL_9, WAYBEL11, TOPS_2, LATTICE3, ORDERS_1, XBOOLE_0, XBOOLE_1,
SUBSET_1;
schemes FRAENKEL, FUNCT_1;
begin :: Subsets as nets
scheme FraenkelInvolution
{A() -> non empty set, X,Y() -> Subset of A(), F(set) -> Element of A()}:
X() = {F(a) where a is Element of A(): a in Y()}
provided
A1: Y() = {F(a) where a is Element of A(): a in X()} and
A2: for a being Element of A() holds F(F(a)) = a
proof
hereby
let x be object;
assume
A3: x in X();
then reconsider a = x as Element of A();
A4: F(a) in Y() by A1,A3;
F(F(a)) = a by A2;
hence x in {F(b) where b is Element of A(): b in Y()} by A4;
end;
let x be object;
assume x in {F(b) where b is Element of A(): b in Y()};
then consider b being Element of A() such that
A5: x = F(b) and
A6: b in Y();
ex a being Element of A() st ( b = F(a))&( a in X()) by A1,A6;
hence thesis by A2,A5;
end;
scheme FraenkelComplement1
{A() -> non empty RelStr, X() -> Subset-Family of A(), Y() -> set,
F(set) -> Subset of A()}:
COMPLEMENT X() = {F(a)` where a is Element of A(): a in Y()}
provided
A1: X() = {F(a) where a is Element of A(): a in Y()}
proof
hereby
let x be object;
assume
A2: x in COMPLEMENT X();
then reconsider y = x as Subset of A();
y` in X() by A2,SETFAM_1:def 7;
then
A3: ex b being Element of A() st ( y` = F(b))&( b in Y()) by A1;
x = y``;
hence x in {F(a)` where a is Element of A(): a in Y()} by A3;
end;
let x be object;
assume x in {F(a)` where a is Element of A(): a in Y()};
then consider a being Element of A() such that
A4: x = F(a)` and
A5: a in Y();
F(a) in X() by A1,A5;
hence thesis by A4,YELLOW_8:5;
end;
scheme FraenkelComplement2
{A() -> non empty RelStr, X() -> Subset-Family of A(), Y() -> set,
F(set) -> Subset of A()}:
COMPLEMENT X() = {F(a) where a is Element of A(): a in Y()}
provided
A1: X() = {F(a)` where a is Element of A(): a in Y()}
proof
hereby
let x be object;
assume
A2: x in COMPLEMENT X();
then reconsider y = x as Subset of A();
y` in X() by A2,SETFAM_1:def 7;
then
A3: ex b being Element of A() st ( y` = F(b)`)&( b in Y()) by A1;
x = y``;
hence x in {F(a) where a is Element of A(): a in Y()} by A3;
end;
let x be object;
assume x in {F(a) where a is Element of A(): a in Y()};
then consider a being Element of A() such that
A4: x = F(a) and
A5: a in Y();
F(a)` in X() by A1,A5;
hence thesis by A4,SETFAM_1:def 7;
end;
theorem
for R being non empty RelStr, x,y being Element of R holds
y in (uparrow x)` iff not x <= y
proof
let R be non empty RelStr, x,y be Element of R;
(uparrow x)` = (the carrier of R) \ uparrow x by SUBSET_1:def 4;
then y in (uparrow x)` iff not y in uparrow x by XBOOLE_0:def 5;
hence thesis by WAYBEL_0:18;
end;
scheme ABC {A() -> TopSpace, F(set) -> set, f() -> Function, P[set]}:
f()"union {F(x) where x is Subset of A(): P[x]} =
union {f()"(F(y)) where y is Subset of A(): P[y]}
proof
set X = {F(x) where x is Subset of A(): P[x]};
set Y = {f()"(F(y)) where y is Subset of A(): P[y]};
hereby
let x be object;
assume
A1: x in f()"union X;
then
A2: x in dom f() by FUNCT_1:def 7;
f().x in union X by A1,FUNCT_1:def 7;
then consider y being set such that
A3: f().x in y and
A4: y in X by TARSKI:def 4;
consider a being Subset of A() such that
A5: y = F(a) and
A6: P[a] by A4;
A7: x in f()"F(a) by A2,A3,A5,FUNCT_1:def 7;
f()"F(a) in Y by A6;
hence x in union Y by A7,TARSKI:def 4;
end;
let x be object;
assume x in union Y;
then consider y being set such that
A8: x in y and
A9: y in Y by TARSKI:def 4;
consider a being Subset of A() such that
A10: y = f()"F(a) and
A11: P[a] by A9;
A12: f().x in F(a) by A8,A10,FUNCT_1:def 7;
F(a) in X by A11;
then
A13: f().x in union X by A12,TARSKI:def 4;
x in dom f() by A8,A10,FUNCT_1:def 7;
hence thesis by A13,FUNCT_1:def 7;
end;
theorem Th2:
for S being 1-sorted, T being non empty 1-sorted, f being Function of S,T
for X being Subset of T holds (f"X)` = f"X`
proof
let S be 1-sorted, T be non empty 1-sorted, f be Function of S,T;
let X be Subset of T;
thus (f"X)` = (the carrier of S)\(f"X) by SUBSET_1:def 4
.= f"(the carrier of T)\(f"X) by FUNCT_2:40
.= f"((the carrier of T)\X) by FUNCT_1:69
.= f"X` by SUBSET_1:def 4;
end;
theorem Th3:
for T being 1-sorted, F being Subset-Family of T holds
COMPLEMENT F = {a` where a is Subset of T: a in F}
proof
let T be 1-sorted, F be Subset-Family of T;
set X = {a` where a is Subset of T: a in F};
hereby
let x be object;
assume
A1: x in COMPLEMENT F;
then reconsider P = x as Subset of T;
A2: P` in F by A1,SETFAM_1:def 7;
P`` = P;
hence x in X by A2;
end;
let x be object;
assume x in X;
then ex P being Subset of T st x = P` & P in F;
hence thesis by YELLOW_8:5;
end;
theorem Th4:
for R being non empty RelStr for F being Subset of R holds
uparrow F = union {uparrow x where x is Element of R: x in F} &
downarrow F = union {downarrow x where x is Element of R: x in F}
proof
let R be non empty RelStr, F be Subset of R;
A1: uparrow F = {x where x is Element of R:
ex y being Element of R st x >= y & y in F} by WAYBEL_0:15;
A2: downarrow F = {x where x is Element of R:
ex y being Element of R st x <= y & y in F} by WAYBEL_0:14;
hereby
let a be object;
assume a in uparrow F;
then consider x being Element of R such that
A3: a = x and
A4: ex y being Element of R st x >= y & y in F by A1;
consider y being Element of R such that
A5: x >= y and
A6: y in F by A4;
A7: uparrow y in {uparrow z where z is Element of R: z in F} by A6;
x in uparrow y by A5,WAYBEL_0:18;
hence a in union {uparrow z where z is Element of R: z in F}
by A3,A7,TARSKI:def 4;
end;
hereby
let a be object;
assume a in union {uparrow x where x is Element of R: x in F};
then consider X being set such that
A8: a in X and
A9: X in {uparrow x where x is Element of R: x in F} by TARSKI:def 4;
consider x being Element of R such that
A10: X = uparrow x and
A11: x in F by A9;
reconsider y = a as Element of R by A8,A10;
y >= x by A8,A10,WAYBEL_0:18;
hence a in uparrow F by A1,A11;
end;
hereby
let a be object;
assume a in downarrow F;
then consider x being Element of R such that
A12: a = x and
A13: ex y being Element of R st x <= y & y in F by A2;
consider y being Element of R such that
A14: x <= y and
A15: y in F by A13;
A16: downarrow y in {downarrow z where z is Element of R: z in F} by A15;
x in downarrow y by A14,WAYBEL_0:17;
hence a in union {downarrow z where z is Element of R: z in F}
by A12,A16,TARSKI:def 4;
end;
hereby
let a be object;
assume a in union {downarrow x where x is Element of R: x in F};
then consider X being set such that
A17: a in X and
A18: X in {downarrow x where x is Element of R: x in F} by TARSKI:def 4;
consider x being Element of R such that
A19: X = downarrow x and
A20: x in F by A18;
reconsider y = a as Element of R by A17,A19;
y <= x by A17,A19,WAYBEL_0:17;
hence a in downarrow F by A2,A20;
end;
end;
theorem
for R being non empty RelStr
for A being Subset-Family of R, F being Subset of R
st A = {(uparrow x)` where x is Element of R: x in F}
holds Intersect A = (uparrow F)`
proof
let R be non empty RelStr;
deffunc F(Element of R) = uparrow $1;
let A be Subset-Family of R, F be Subset of R such that
A1: A = {F(x)` where x is Element of R: x in F};
A2: COMPLEMENT A = {F(x) where x is Element of R: x in F}
from FraenkelComplement2(A1);
reconsider C = COMPLEMENT A as Subset-Family of R;
COMPLEMENT C = A;
hence Intersect A = (union C)` by YELLOW_8:6
.= (uparrow F)` by A2,Th4;
end;
registration
cluster strict complete 1-element for TopLattice;
existence
proof
take the strict reflexive 1-element discrete finite TopRelStr;
thus thesis;
end;
end;
registration
let S be non empty RelStr,
T be upper-bounded non empty reflexive antisymmetric RelStr;
cluster infs-preserving for Function of S,T;
existence
proof
take f = S --> Top T;
let A be Subset of S;
assume ex_inf_of A,S;
A1: rng f = {Top T} by FUNCOP_1:8;
f.:A c= rng f by RELAT_1:111;
then
A2: f.:A = {} or f.:A = {Top T} by A1,ZFMISC_1:33;
hence ex_inf_of f.:A,T by YELLOW_0:38,43;
thus inf (f.:A) = Top T by A2,YELLOW_0:39
.= f.inf A by FUNCOP_1:7;
end;
end;
registration
let S be non empty RelStr,
T be lower-bounded non empty reflexive antisymmetric RelStr;
cluster sups-preserving for Function of S,T;
existence
proof
take f = S --> Bottom T;
let A be Subset of S;
assume ex_sup_of A,S;
A1: rng f = {Bottom T} by FUNCOP_1:8;
f.:A c= rng f by RELAT_1:111;
then
A2: f.:A = {} or f.:A = {Bottom T} by A1,ZFMISC_1:33;
hence ex_sup_of f.:A,T by YELLOW_0:38,42;
thus sup (f.:A) = Bottom T by A2,YELLOW_0:39
.= f.sup A by FUNCOP_1:7;
end;
end;
definition
let R,S be 1-sorted;
assume
A1: the carrier of S c= the carrier of R;
A2: dom id the carrier of S = the carrier of S;
A3: rng id the carrier of S = the carrier of S;
func incl(S,R) -> Function of S,R equals
: Def1:
id the carrier of S;
coherence by A1,A2,A3,FUNCT_2:2;
end;
registration
let R be non empty RelStr;
let S be non empty SubRelStr of R;
cluster incl(S,R) -> monotone;
coherence
proof
let x,y be Element of S;
reconsider a = x, b = y as Element of R by YELLOW_0:58;
the carrier of S c= the carrier of R by YELLOW_0:def 13;
then
A1: incl(S,R) = id the carrier of S by Def1;
then
A2: incl(S,R).x = a;
incl(S,R).y = b by A1;
hence thesis by A2,YELLOW_0:59;
end;
end;
definition
let R be non empty RelStr, X be non empty Subset of R;
func X+id -> strict non empty NetStr over R equals
(incl(subrelstr X, R))* (
( subrelstr X)+id);
coherence;
func X opp+id -> strict non empty NetStr over R equals
(incl(subrelstr X, R
) )*((subrelstr X)opp+id);
coherence;
end;
theorem
for R being non empty RelStr, X being non empty Subset of R holds
the carrier of X+id = X & X+id is full SubRelStr of R &
for x being Element of X+id holds X+id.x = x
proof
let R be non empty RelStr, X be non empty Subset of R;
A1: the RelStr of X+id = the RelStr of (subrelstr X)+id by WAYBEL_9:def 8;
A2: the mapping of X+id = incl(subrelstr X, R)*the mapping of (subrelstr X)
+id by WAYBEL_9:def 8;
A3: the carrier of subrelstr X = X by YELLOW_0:def 15;
hence
A4: the carrier of X+id = X by A1,WAYBEL_9:def 5;
A5: the RelStr of (subrelstr X)+id = subrelstr X by WAYBEL_9:def 5;
the InternalRel of subrelstr X c= the InternalRel of R by YELLOW_0:def 13;
then reconsider S = X+id as SubRelStr of R by A1,A3,A5,YELLOW_0:def 13;
the InternalRel of S = (the InternalRel of R)|_2 the carrier of S
by A1,A5,YELLOW_0:def 14;
hence X+id is full SubRelStr of R by YELLOW_0:def 14;
let x be Element of X+id;
id subrelstr X = id X by YELLOW_0:def 15;
then
A6: the mapping of (subrelstr X)+id = id X by WAYBEL_9:def 5;
A7: dom id X = X;
incl(subrelstr X, R) = id X by A3,Def1;
then the mapping of X+id = id X by A2,A6,A7,RELAT_1:52;
hence thesis by A4;
end;
theorem
for R being non empty RelStr, X being non empty Subset of R holds
the carrier of X opp+id = X & X opp+id is full SubRelStr of R opp &
for x being Element of X opp+id holds X opp+id.x = x
proof
let R be non empty RelStr, X be non empty Subset of R;
A1: the RelStr of X opp+id = the RelStr of (subrelstr X)opp+id by
WAYBEL_9:def 8;
A2: the mapping of X opp+id = incl(subrelstr X, R)*the mapping of (subrelstr
X) opp+id by WAYBEL_9:def 8;
A3: the carrier of subrelstr X = X by YELLOW_0:def 15;
A4: the carrier of (subrelstr X) opp+id = the carrier of subrelstr X by
WAYBEL_9:def 6;
A5: the InternalRel of (subrelstr X) opp+id = (the InternalRel of subrelstr
X)~ by WAYBEL_9:def 6;
thus
the carrier of X opp+id = X by A1,A3,WAYBEL_9:def 6;
A6: R opp = RelStr(#the carrier of R, (the InternalRel of R)~#)
by LATTICE3:def 5;
the InternalRel of subrelstr X = (the InternalRel of R)|_2 X
by A3,YELLOW_0:def 14;
then
A7: the InternalRel of (subrelstr X)opp+id = (the InternalRel of R)~|_2 X
by A5,ORDERS_1:83;
then the InternalRel of (subrelstr X)opp+id c= the InternalRel of R opp
by A6,XBOOLE_1:17;
then reconsider S = X opp+id as SubRelStr of R opp by A1,A3,A4,A6,
YELLOW_0:def 13;
the InternalRel of S
= (the InternalRel of R opp)|_2 the carrier of S by A1,A4,A6,A7,
YELLOW_0:def 15;
hence X opp+id is full SubRelStr of R opp by YELLOW_0:def 14;
let x be Element of X opp+id;
id subrelstr X = id X by YELLOW_0:def 15;
then
A8: the mapping of (subrelstr X)opp+id = id X by WAYBEL_9:def 6;
A9: dom id X = X;
incl(subrelstr X, R) = id X by A3,Def1;
then the mapping of X opp+id = id X by A2,A8,A9,RELAT_1:52;
hence thesis by A1,A3,A4;
end;
registration
let R be non empty reflexive RelStr;
let X be non empty Subset of R;
cluster X +id -> reflexive;
coherence;
cluster X opp+id -> reflexive;
coherence;
end;
registration
let R be non empty transitive RelStr;
let X be non empty Subset of R;
cluster X +id -> transitive;
coherence;
cluster X opp+id -> transitive;
coherence;
end;
registration
let R be non empty reflexive RelStr;
let I be directed Subset of R;
cluster subrelstr I -> directed;
coherence
proof
let x,y be Element of subrelstr I;
A1: the carrier of subrelstr I = I by YELLOW_0:def 15;
assume that
A2: x in [#]subrelstr I and
A3: y in [#]subrelstr I;
reconsider a = x, b = y as Element of R by A1,A2,A3;
consider c being Element of R such that
A4: c in I and
A5: a <= c and
A6: b <= c by A1,A2,WAYBEL_0:def 1;
reconsider z = c as Element of subrelstr I by A4,YELLOW_0:def 15;
take z;
thus thesis by A2,A5,A6,YELLOW_0:60;
end;
end;
registration
let R be non empty reflexive RelStr;
let I be directed non empty Subset of R;
cluster I+id -> directed;
coherence;
end;
registration
let R be non empty reflexive RelStr;
let F be filtered non empty Subset of R;
cluster (subrelstr F) opp+id -> directed;
coherence
proof
set I = F, A = (subrelstr I)opp+id;
let x,y be Element of (subrelstr I)opp+id;
A1: the carrier of subrelstr I = I by YELLOW_0:def 15;
A2: the carrier of A = the carrier of subrelstr F by WAYBEL_9:def 6;
assume that
A3: x in [#]A and
A4: y in [#]A;
reconsider a = x, b = y as Element of R by A1,A2,A3,A4;
A5: the RelStr of A = the RelStr of (subrelstr F) opp by WAYBEL_9:11;
consider c being Element of R such that
A6: c in I and
A7: a >= c and
A8: b >= c by A1,A2,WAYBEL_0:def 2;
reconsider a1 = x, b1 = y, c1 = c as Element of subrelstr F
by A6,WAYBEL_9:def 6,YELLOW_0:def 15;
reconsider z = c as Element of A by A2,A6,YELLOW_0:def 15;
take z;
A9: a1~ = a1 by LATTICE3:def 6;
A10: b1~ = b1 by LATTICE3:def 6;
A11: c1~ = c1 by LATTICE3:def 6;
A12: a1 >= c1 by A7,YELLOW_0:60;
A13: b1 >= c1 by A8,YELLOW_0:60;
A14: a1~ <= c1~ by A12,LATTICE3:9;
b1~ <= c1~ by A13,LATTICE3:9;
hence thesis by A5,A9,A10,A11,A14;
end;
end;
registration
let R be non empty reflexive RelStr;
let F be filtered non empty Subset of R;
cluster F opp+id -> directed;
coherence;
end;
begin :: Operations on families of open sets
theorem Th8:
for T being TopSpace st T is empty holds the topology of T = {{}}
proof
let T1 be TopSpace;
assume T1 is empty;
then
A1: the carrier of T1 = {};
then {} in the topology of T1 by PRE_TOPC:def 1;
hence thesis by A1,ZFMISC_1:1,33;
end;
theorem Th9:
for T being 1-element TopSpace holds
the topology of T = bool the carrier of T & for x being Point of T holds
the carrier of T = {x} & the topology of T = {{},{x}}
proof
let T be 1-element TopSpace;
thus the topology of T c= bool the carrier of T;
consider x being Point of T such that
A1: the carrier of T = {x} by TEX_1:def 1;
A2: {} in the topology of T by PRE_TOPC:1;
A3: the carrier of T in the topology of T by PRE_TOPC:def 1;
A4: bool {x} = {{},{x}} by ZFMISC_1:24;
hence bool the carrier of T c= the topology of T by A1,A2,A3,ZFMISC_1:32;
let a be Point of T;
a = x by STRUCT_0:def 10;
hence the carrier of T = {a} & the topology of T c= {{},{a}} &
{{},{a}} c= the topology of T by A1,A2,A3,A4,ZFMISC_1:32;
end;
theorem
for T being 1-element TopSpace holds
{the carrier of T} is Basis of T &
{} is prebasis of T & {{}} is prebasis of T
proof
let T be 1-element TopSpace;
set BB = {the carrier of T};
A1: the carrier of T c= the carrier of T;
A2: the topology of T = bool the carrier of T by Th9;
reconsider BB as Subset-Family of T by A1,ZFMISC_1:31;
set x = the Element of T;
A3: the topology of T = {{}, {x}} by Th9;
A4: the carrier of T = {x} by Th9;
A5: {} c= bool the carrier of T;
A6: {} c= BB;
A7: {} c= the carrier of T;
reconsider C = {} as Subset-Family of T by XBOOLE_1:2;
the topology of T c= UniCl BB
proof
let a be object;
assume a in the topology of T;
then a = {x} & union {{x}} = {x} & BB c= BB & BB c= bool the carrier of
T or a = {} by A3,TARSKI:def 2,ZFMISC_1:25;
hence thesis by A4,A5,A6,A7,CANTOR_1:def 1,ZFMISC_1:2;
end;
hence
A8: {the carrier of T} is Basis of T by A2,CANTOR_1:def 2,TOPS_2:64;
A9: {} c= the topology of T;
BB c= FinMeetCl C
proof
let x be object;
assume x in BB;
then x = the carrier of T by TARSKI:def 1;
then Intersect C = x by SETFAM_1:def 9;
hence thesis by CANTOR_1:def 3;
end;
hence {} is prebasis of T by A8,A9,CANTOR_1:def 4,TOPS_2:64;
{} c= the carrier of T;
then reconsider D = {{}} as Subset-Family of T by ZFMISC_1:31;
A10: D c= the topology of T by A3,ZFMISC_1:7;
BB c= FinMeetCl D
proof
let x be object;
assume x in BB;
then
A11: x = the carrier of T by TARSKI:def 1;
A12: Intersect C = the carrier of T by SETFAM_1:def 9;
C c= D;
hence thesis by A11,A12,CANTOR_1:def 3;
end;
hence thesis by A8,A10,CANTOR_1:def 4,TOPS_2:64;
end;
theorem Th11:
for X,Y being set, A being Subset-Family of X st A = {Y}
holds FinMeetCl A = {Y,X} & UniCl A = {Y,{}}
proof
let X,Z be set, A be Subset-Family of X such that
A1: A = {Z};
thus FinMeetCl A c= {Z,X}
proof
let x be object;
assume x in FinMeetCl A;
then consider Y being Subset-Family of X such that
A2: Y c= A and Y is finite and
A3: x = Intersect Y by CANTOR_1:def 3;
Y = {} or Y = {Z} by A1,A2,ZFMISC_1:33;
then x = X or x = meet {Z} by A3,SETFAM_1:def 9;
then x = X or x = Z by SETFAM_1:10;
hence thesis by TARSKI:def 2;
end;
reconsider E = {} as Subset-Family of X by XBOOLE_1:2;
reconsider E as Subset-Family of X;
hereby
let x be object;
assume x in {Z,X};
then x = X or x = Z by TARSKI:def 2;
then x = X or x = meet {Z} by SETFAM_1:10;
then x = Intersect E & E c= A or x = Intersect A & A c= A
by A1,SETFAM_1:def 9;
hence x in FinMeetCl A by A1,CANTOR_1:def 3;
end;
hereby
let x be object;
assume x in UniCl A;
then consider Y being Subset-Family of X such that
A4: Y c= A and
A5: x = union Y by CANTOR_1:def 1;
Y = {} or Y = {Z} by A1,A4,ZFMISC_1:33;
then x = {} or x = Z by A5,ZFMISC_1:2,25;
hence x in {Z,{}} by TARSKI:def 2;
end;
let x be object;
assume x in {Z,{}};
then x = {} or x = Z by TARSKI:def 2;
then x = union E & E c= A or x = union A & A c= A by A1,ZFMISC_1:2
,25;
hence thesis by CANTOR_1:def 1;
end;
theorem
for X being set, A,B being Subset-Family of X st A = B \/ {X} or B = A \ { X
} holds Intersect A = Intersect B
proof
let X be set, A,B be Subset-Family of X;
assume
A1: A = B \/ {X} or B = A \ {X};
hereby
let x be object;
assume
A2: x in Intersect A;
now
let y be set;
assume y in B;
then y in A by A1,XBOOLE_0:def 3,def 5;
hence x in y by A2,SETFAM_1:43;
end;
hence x in Intersect B by A2,SETFAM_1:43;
end;
let x be object;
assume
A3: x in Intersect B;
now
let y be set;
assume y in A;
then y in B & not y in {X} or y in {X} by A1,XBOOLE_0:def 3,def 5;
then y in B or y = X by TARSKI:def 1;
hence x in y by A3,SETFAM_1:43;
end;
hence thesis by A3,SETFAM_1:43;
end;
theorem
for X being set, A,B being Subset-Family of X st A = B \/ {X} or B = A \ { X
} holds FinMeetCl A = FinMeetCl B
proof
let X be set, A,B be Subset-Family of X;
assume
A1: A = B \/ {X} or B = A \ {X};
X in FinMeetCl B by CANTOR_1:8;
then
A2: {X} c= FinMeetCl B by ZFMISC_1:31;
A3: B c= FinMeetCl B by CANTOR_1:4;
(A \ {X}) \/ {X} = A \/ {X} by XBOOLE_1:39;
then
A4: A c= B \/ {X} by A1,XBOOLE_1:7;
B \/ {X} c= FinMeetCl B by A2,A3,XBOOLE_1:8;
then A c= FinMeetCl B by A4;
then FinMeetCl A c= FinMeetCl FinMeetCl B by CANTOR_1:14;
hence FinMeetCl A c= FinMeetCl B by CANTOR_1:11;
thus thesis by A1,CANTOR_1:14,XBOOLE_1:7,36;
end;
theorem Th14:
for X being set, A being Subset-Family of X st X in A
for x being set holds x in FinMeetCl A iff
ex Y being finite non empty Subset-Family of X st Y c= A & x = Intersect Y
proof
let X be set, A be Subset-Family of X;
assume
A1: X in A;
then
A2: {X} c= A by ZFMISC_1:31;
reconsider Z = {X} as finite non empty Subset-Family of X by A1,ZFMISC_1:31;
reconsider Z as finite non empty Subset-Family of X;
A3: Intersect Z = meet Z by SETFAM_1:def 9
.= X by SETFAM_1:10;
let x be set;
hereby
assume x in FinMeetCl A;
then consider Y being Subset-Family of X such that
A4: Y c= A and
A5: Y is finite and
A6: x = Intersect Y by CANTOR_1:def 3;
per cases;
suppose Y = {};
then x = X by A6,SETFAM_1:def 9;
hence ex Y being finite non empty Subset-Family of X st
Y c= A & x = Intersect Y by A2,A3;
end;
suppose Y <> {};
hence ex Y being finite non empty Subset-Family of X st
Y c= A & x = Intersect Y by A4,A5,A6;
end;
end;
thus thesis by CANTOR_1:def 3;
end;
theorem Th15:
for X being set, A being Subset-Family of X holds UniCl UniCl A = UniCl A
proof
let X be set, A be Subset-Family of X;
hereby
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in UniCl UniCl A;
then consider Y being Subset-Family of X such that
A1: Y c= UniCl A and
A2: x = union Y by CANTOR_1:def 1;
set Z = {y where y is Subset of X: y in A & y c= xx};
Z c= bool X
proof
let a be object;
assume a in Z;
then ex y being Subset of X st a = y & y in A & y c= xx;
hence thesis;
end;
then reconsider Z as Subset-Family of X;
A3: xx = union Z
proof
hereby
let a be object;
assume a in xx;
then consider s being set such that
A4: a in s and
A5: s in Y by A2,TARSKI:def 4;
consider t being Subset-Family of X such that
A6: t c= A and
A7: s = union t by A1,A5,CANTOR_1:def 1;
consider u being set such that
A8: a in u and
A9: u in t by A4,A7,TARSKI:def 4;
reconsider u as Subset of X by A9;
A10: u c= s by A7,A9,ZFMISC_1:74;
s c= xx by A2,A5,ZFMISC_1:74;
then u c= xx by A10;
then u in Z by A6,A9;
hence a in union Z by A8,TARSKI:def 4;
end;
let a be object;
assume a in union Z;
then consider u being set such that
A11: a in u and
A12: u in Z by TARSKI:def 4;
ex y being Subset of X st u = y & y in A & y c= xx by A12;
hence thesis by A11;
end;
Z c= A
proof
let a be object;
assume a in Z;
then ex y being Subset of X st a = y & y in A & y c= xx;
hence thesis;
end;
hence x in UniCl A by A3,CANTOR_1:def 1;
end;
thus thesis by CANTOR_1:1;
end;
theorem Th16:
for X being set, A being empty Subset-Family of X holds UniCl A = {{}}
proof
let X be set, A be empty Subset-Family of X;
hereby
let x be object;
assume x in UniCl A;
then consider B being Subset-Family of X such that
A1: B c= A and
A2: x = union B by CANTOR_1:def 1;
B = {} by A1;
hence x in {{}} by A2,TARSKI:def 1,ZFMISC_1:2;
end;
let x be object;
assume x in {{}};
then
A3: x = {} by TARSKI:def 1;
union {}bool X = {} by ZFMISC_1:2;
hence thesis by A3,CANTOR_1:def 1;
end;
theorem Th17:
for X being set, A being empty Subset-Family of X holds FinMeetCl A = {X}
proof
let X be set, A be empty Subset-Family of X;
hereby
let x be object;
assume x in FinMeetCl A;
then consider B being Subset-Family of X such that
A1: B c= A and B is finite and
A2: x = Intersect B by CANTOR_1:def 3;
B = {} by A1;
then x = X by A2,SETFAM_1:def 9;
hence x in {X} by TARSKI:def 1;
end;
let x be object;
assume x in {X};
then
A3: x = X by TARSKI:def 1;
Intersect {}bool X = X by SETFAM_1:def 9;
hence thesis by A3,CANTOR_1:def 3;
end;
theorem Th18:
for X being set, A being Subset-Family of X st A = {{},X}
holds UniCl A = A & FinMeetCl A = A
proof
let X be set, A be Subset-Family of X such that
A1: A = {{},X};
hereby
let a be object;
assume a in UniCl A;
then consider y being Subset-Family of X such that
A2: y c= A and
A3: a = union y by CANTOR_1:def 1;
y = {} or y = {{}} or y = {X} or y = {{},X} by A1,A2,ZFMISC_1:36;
then a = {} or a = X or a = {} \/ X & {} \/ X = X by A3,ZFMISC_1:2,25,75;
hence a in A by A1,TARSKI:def 2;
end;
thus A c= UniCl A by CANTOR_1:1;
hereby
let a be object;
assume a in FinMeetCl A;
then consider y being Subset-Family of X such that
A4: y c= A and y is finite and
A5: a = Intersect y by CANTOR_1:def 3;
y = {} or y = {{}} or y = {X} or y = {{},X} by A1,A4,ZFMISC_1:36;
then a = X or a = meet {{}} or a = meet {X} or a = meet {{},X}
by A5,SETFAM_1:def 9;
then a = X or a = {} or a = {} /\ X & {} /\ X = {} by SETFAM_1:10,11;
hence a in A by A1,TARSKI:def 2;
end;
thus thesis by CANTOR_1:4;
end;
theorem Th19:
for X,Y being set, A being Subset-Family of X, B being Subset-Family of Y
holds (A c= B implies UniCl A c= UniCl B) &
(A = B implies UniCl A = UniCl B)
proof
let X,Y be set, A be Subset-Family of X, B be Subset-Family of Y;
A1: now
let X,Y be set;
let A be Subset-Family of X, B be Subset-Family of Y such that
A2: A c= B;
thus UniCl A c= UniCl B
proof
let x be object;
assume x in UniCl A;
then consider y being Subset-Family of X such that
A3: y c= A and
A4: x = union y by CANTOR_1:def 1;
y c= B by A2,A3;
then y is Subset-Family of Y by XBOOLE_1:1;
then ex y being Subset-Family of Y st y c= B & x = union y by A2,A3,A4,
XBOOLE_1:1;
hence thesis by CANTOR_1:def 1;
end;
end;
hence A c= B implies UniCl A c= UniCl B;
assume A = B;
hence UniCl A c= UniCl B & UniCl B c= UniCl A by A1;
end;
theorem Th20:
for X,Y being set, A being Subset-Family of X, B being Subset-Family of Y
st A = B & X in A
holds FinMeetCl B = {Y} \/ FinMeetCl A
proof
let X,Y be set, A be Subset-Family of X, B be Subset-Family of Y such that
A1: A = B and
A2: X in A;
thus FinMeetCl B c= {Y} \/ FinMeetCl A
proof
let x be object;
assume x in FinMeetCl B;
then consider y being Subset-Family of Y such that
A3: y c= B and
A4: y is finite and
A5: x = Intersect y by CANTOR_1:def 3;
reconsider z = y as Subset-Family of X by A1,A3,XBOOLE_1:1;
reconsider z as Subset-Family of X;
per cases;
suppose y = {};
then x = Y by A5,SETFAM_1:def 9;
then x in {Y} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A6: y <> {};
then
A7: Intersect y = meet y by SETFAM_1:def 9;
Intersect z = meet y by A6,SETFAM_1:def 9;
then x in FinMeetCl A by A1,A3,A4,A5,A7,CANTOR_1:def 3;
hence thesis by XBOOLE_0:def 3;
end;
end;
let x be object;
assume
A8: x in {Y} \/ FinMeetCl A;
per cases by A8,XBOOLE_0:def 3;
suppose x in {Y};
then
A9: x = Y by TARSKI:def 1;
A10: Intersect {}bool Y = Y by SETFAM_1:def 9;
{}bool Y c= B;
hence thesis by A9,A10,CANTOR_1:def 3;
end;
suppose x in FinMeetCl A;
then consider y being non empty finite Subset-Family of X such that
A11: y c= A and
A12: x = Intersect y by A2,Th14;
reconsider z = y as Subset-Family of Y by A1,A11,XBOOLE_1:1;
reconsider z as Subset-Family of Y;
x = meet z by A12,SETFAM_1:def 9
.= Intersect z by SETFAM_1:def 9;
hence thesis by A1,A11,CANTOR_1:def 3;
end;
end;
theorem Th21:
for X being set, A being Subset-Family of X holds
UniCl FinMeetCl UniCl A = UniCl FinMeetCl A
proof
let X be set, A be Subset-Family of X;
per cases;
suppose
A1: A = {};
then
A2: FinMeetCl A = {X} by Th17;
UniCl A = {{}} by A1,Th16;
then
A3: FinMeetCl UniCl A = {{},X} by Th11;
UniCl FinMeetCl A = {X,{}} by A2,Th11;
hence thesis by A3,Th18;
end;
suppose A <> {};
then reconsider A as non empty Subset-Family of X;
A4: UniCl FinMeetCl UniCl A c= UniCl UniCl FinMeetCl A
proof
let x be object;
assume x in UniCl FinMeetCl UniCl A;
then consider Y being Subset-Family of X such that
A5: Y c= FinMeetCl UniCl A and
A6: x = union Y by CANTOR_1:def 1;
Y c= UniCl FinMeetCl A
proof
let y be object;
reconsider yy=y as set by TARSKI:1;
assume y in Y;
then consider Z being Subset-Family of X such that
A7: Z c= UniCl A and
A8: Z is finite and
A9: y = Intersect Z by A5,CANTOR_1:def 3;
per cases;
suppose Z = {};
then y = X by A9,SETFAM_1:def 9;
then
A10: y in FinMeetCl A by CANTOR_1:8;
FinMeetCl A c= UniCl FinMeetCl A by CANTOR_1:1;
hence thesis by A10;
end;
suppose
A11: Z <> {};
then
A12: y = meet Z by A9,SETFAM_1:def 9;
set G = {meet rng f where f is Element of Funcs(Z,A):
for z being set st z in Z holds f.z c= z};
A13: G c= FinMeetCl A
proof
let a be object;
assume a in G;
then consider f being Element of Funcs(Z,A) such that
A14: a = meet rng f and for z being set st z in Z holds f.z c= z;
reconsider B = rng f as Subset-Family of X by XBOOLE_1:1;
reconsider B as Subset-Family of X;
Intersect B = a by A11,A14,SETFAM_1:def 9;
hence thesis by A8,CANTOR_1:def 3;
end;
then reconsider G as Subset-Family of X by XBOOLE_1:1;
reconsider G as Subset-Family of X;
union G = yy
proof
hereby
let a be object;
assume a in union G;
then consider b being set such that
A15: a in b and
A16: b in G by TARSKI:def 4;
consider f being Element of Funcs(Z,A) such that
A17: b = meet rng f and
A18: for z being set st z in Z holds f.z c= z by A16;
A19: dom f = Z by FUNCT_2:def 1;
reconsider B = rng f as Subset-Family of X by XBOOLE_1:1;
reconsider B as Subset-Family of X;
b c= yy
proof
let c be object;
assume
A20: c in b;
now
let d be set;
assume
A21: d in Z;
then f.d in B by A19,FUNCT_1:def 3;
then
A22: b c= f.d by A17,SETFAM_1:3;
A23: f.d c= d by A18,A21;
c in f.d by A20,A22;
hence c in d by A23;
end;
hence thesis by A11,A12,SETFAM_1:def 1;
end;
hence a in yy by A15;
end;
let a be object;
assume
A24: a in yy;
defpred P[object,object] means
ex A,B being set st A = $1 & B = $2 & a in B & B c= A;
A25: now
let z be object;
assume
A26: z in Z;
reconsider zz=z as set by TARSKI:1;
A27: a in zz by A12,A24,SETFAM_1:def 1,A26;
consider C being Subset-Family of X such that
A28: C c= A and
A29: z = union C by A7,A26,CANTOR_1:def 1;
consider w being set such that
A30: a in w and
A31: w in C by A27,A29,TARSKI:def 4;
reconsider w as object;
take w;
thus w in A by A28,A31;
thus P[z, w] by A29,A30,A31,ZFMISC_1:74;
end;
consider f being Function such that
A32: dom f = Z & rng f c= A and
A33: for z being object st z in Z holds P[z, f.z]
from FUNCT_1:sch 6(A25);
reconsider f as Element of Funcs(Z,A) by A32,FUNCT_2:def 2;
for z being set st z in Z holds f.z c= z
proof let z be set;
assume z in Z;
then P[z, f.z] by A33;
hence thesis;
end;
then
A34: meet rng f in G;
now
thus rng f <> {} by A11;
let y be set;
assume y in rng f;
then consider z being object such that
A35: z in Z & y = f.z by A32,FUNCT_1:def 3;
P[z,f.z] by A33,A35;
hence a in y by A35;
end;
then a in meet rng f by SETFAM_1:def 1;
hence thesis by A34,TARSKI:def 4;
end;
hence thesis by A13,CANTOR_1:def 1;
end;
end;
hence thesis by A6,CANTOR_1:def 1;
end;
FinMeetCl A c= FinMeetCl UniCl A by CANTOR_1:1,14;
then
A36: UniCl FinMeetCl A c= UniCl FinMeetCl UniCl A by CANTOR_1:9;
UniCl UniCl FinMeetCl A = UniCl FinMeetCl A by Th15;
hence thesis by A4,A36;
end;
end;
begin :: Bases
theorem Th22:
for T being TopSpace, K being Subset-Family of T
holds the topology of T = UniCl K iff K is Basis of T
proof
let T be TopSpace, K be Subset-Family of T;
thus the topology of T = UniCl K implies K is Basis of T
by CANTOR_1:1,CANTOR_1:def 2,TOPS_2:64;
assume
A1: K is Basis of T;
then K c= the topology of T by TOPS_2:64;
then
A2: UniCl K c= UniCl the topology of T by CANTOR_1:9;
the topology of T c= UniCl K by A1,CANTOR_1:def 2;
hence the topology of T c= UniCl K & UniCl K c= the topology of T
by A2,CANTOR_1:6;
end;
theorem Th23:
for T being TopSpace, K being Subset-Family of T
holds K is prebasis of T iff FinMeetCl K is Basis of T
proof
let T be TopSpace, BB be Subset-Family of T;
A1: T is empty implies the topology of T = bool the carrier of T
by ZFMISC_1:1,Th8;
thus BB is prebasis of T implies FinMeetCl BB is Basis of T
proof
assume
A2: BB is prebasis of T;
then BB c= the topology of T by TOPS_2:64;
then FinMeetCl BB c= FinMeetCl the topology of T by CANTOR_1:14;
then
A3: FinMeetCl BB c= the topology of T by A1,CANTOR_1:5;
consider A being Basis of T such that
A4: A c= FinMeetCl BB by A2,CANTOR_1:def 4;
A5: the topology of T c= UniCl A by CANTOR_1:def 2;
UniCl A c= UniCl FinMeetCl BB by A4,CANTOR_1:9;
then the topology of T c= UniCl FinMeetCl BB by A5;
hence thesis by A3,CANTOR_1:def 2,TOPS_2:64;
end;
assume
A6: FinMeetCl BB is Basis of T;
A7: BB c= FinMeetCl BB by CANTOR_1:4;
FinMeetCl BB c= the topology of T by A6,TOPS_2:64;
then BB c= the topology of T by A7;
hence thesis by A6,CANTOR_1:def 4,TOPS_2:64;
end;
theorem Th24:
for T being non empty TopSpace, B being Subset-Family of T
st UniCl B is prebasis of T holds B is prebasis of T
proof
let T be non empty TopSpace, B be Subset-Family of T;
assume UniCl B is prebasis of T;
then FinMeetCl UniCl B is Basis of T by Th23;
then UniCl FinMeetCl UniCl B = the topology of T by Th22;
then UniCl FinMeetCl B = the topology of T by Th21;
then FinMeetCl B is Basis of T by Th22;
hence thesis by Th23;
end;
theorem Th25:
for T1, T2 being TopSpace, B being Basis of T1
st the carrier of T1 = the carrier of T2 & B is Basis of T2
holds the topology of T1 = the topology of T2
proof
let T1, T2 be TopSpace, B be Basis of T1;
assume that
A1: the carrier of T1 = the carrier of T2 and
A2: B is Basis of T2;
reconsider C = B as Basis of T2 by A2;
thus the topology of T1 = UniCl C by A1,Th22
.= the topology of T2 by Th22;
end;
theorem Th26:
for T1, T2 being TopSpace, P being prebasis of T1
st the carrier of T1 = the carrier of T2 & P is prebasis of T2
holds the topology of T1 = the topology of T2
proof
let T1, T2 be TopSpace, P be prebasis of T1;
assume that
A1: the carrier of T1 = the carrier of T2 and
A2: P is prebasis of T2;
reconsider C = P as prebasis of T2 by A2;
A3: FinMeetCl P is Basis of T1 by Th23;
FinMeetCl C is Basis of T2 by Th23;
hence thesis by A1,A3,Th25;
end;
theorem
for T being TopSpace, K being Basis of T holds
K is open & K is prebasis of T;
theorem
for T being TopSpace, K being prebasis of T holds K is open;
theorem Th29:
for T being non empty TopSpace, B being prebasis of T holds
B \/ {the carrier of T} is prebasis of T
proof
let T be non empty TopSpace, B be prebasis of T;
set C = B \/ {the carrier of T};
A1: the carrier of T in the topology of T by PRE_TOPC:def 1;
A2: B c= the topology of T by TOPS_2:64;
A3: {the carrier of T} c= the topology of T by A1,ZFMISC_1:31;
then C c= the topology of T by A2,XBOOLE_1:8;
then reconsider C as Subset-Family of T by XBOOLE_1:1;
A4: C c= the topology of T by A2,A3,XBOOLE_1:8;
A5: FinMeetCl B c= FinMeetCl C by CANTOR_1:14,XBOOLE_1:7;
FinMeetCl B is Basis of T by Th23;
hence thesis by A4,A5,CANTOR_1:def 4,TOPS_2:64;
end;
theorem
for T being TopSpace, B being Basis of T holds
B \/ {the carrier of T} is Basis of T
proof
let T be TopSpace, B be Basis of T;
set C = B \/ {the carrier of T};
A1: the carrier of T in the topology of T by PRE_TOPC:def 1;
A2: B c= the topology of T by TOPS_2:64;
A3: {the carrier of T} c= the topology of T by A1,ZFMISC_1:31;
then C c= the topology of T by A2,XBOOLE_1:8;
then reconsider C as Subset-Family of T by XBOOLE_1:1;
A4: C c= the topology of T by A2,A3,XBOOLE_1:8;
A5: UniCl B c= UniCl C by CANTOR_1:9,XBOOLE_1:7;
the topology of T c= UniCl B by CANTOR_1:def 2;
then the topology of T c= UniCl C by A5;
hence thesis by A4,CANTOR_1:def 2,TOPS_2:64;
end;
theorem Th31:
for T being TopSpace, B being Basis of T for A being Subset of T holds
A is open iff for p being Point of T st p in A
ex a being Subset of T st a in B & p in a & a c= A
proof
let T be TopSpace, K be Basis of T, A be Subset of T;
hereby
assume A is open;
then
A1: A = union {G where G is Subset of T: G in K & G c= A} by YELLOW_8:9;
let p be Point of T;
assume p in A;
then consider Z being set such that
A2: p in Z and
A3: Z in {G where G is Subset of T: G in K & G c= A} by A1,TARSKI:def 4;
ex a being Subset of T st Z = a & a in K & a c= A by A3;
hence ex a being Subset of T st a in K & p in a & a c= A by A2;
end;
assume
A4: for p being Point of T st p in A
ex a being Subset of T st a in K & p in a & a c= A;
set F = {G where G is Subset of T: G in K & G c= A};
F c= bool the carrier of T
proof
let x be object;
assume x in F;
then ex G being Subset of T st x = G & G in K & G c= A;
hence thesis;
end;
then reconsider F as Subset-Family of T;
reconsider F as Subset-Family of T;
A5: F is open
proof
let x be Subset of T;
assume x in F;
then
A6: ex G being Subset of T st x = G & G in K & G c= A;
K c= the topology of T by TOPS_2:64;
hence x in the topology of T by A6;
end;
A = union F
proof
hereby
let x be object;
assume
A7: x in A;
then reconsider p = x as Point of T;
consider a being Subset of T such that
A8: a in K and
A9: p in a and
A10: a c= A by A4,A7;
a in F by A8,A10;
hence x in union F by A9,TARSKI:def 4;
end;
F c= bool A
proof
let x be object;
assume x in F;
then ex G being Subset of T st x = G & G in K & G c= A;
hence thesis;
end;
then union F c= union bool A by ZFMISC_1:77;
hence thesis by ZFMISC_1:81;
end;
hence thesis by A5,TOPS_2:19;
end;
theorem Th32:
for T being TopSpace, B being Subset-Family of T st B c= the topology of T &
for A being Subset of T st A is open for p being Point of T st p in A
ex a being Subset of T st a in B & p in a & a c= A holds B is Basis of T
proof
let T be TopSpace, B be Subset-Family of T such that
A1: B c= the topology of T and
A2: for A being Subset of T st A is open for p being Point of T st p in A
ex a being Subset of T st a in B & p in a & a c= A;
A3: B is open by A1,TOPS_2:64;
B is quasi_basis
proof
let x be object;
assume
A4: x in the topology of T;
then reconsider A = x as Subset of T;
set Y = {V where V is Subset of T: V in B & V c= A};
Y c= bool the carrier of T
proof
let y be object;
assume y in Y;
then ex V being Subset of T st y = V & V in B & V c= A;
hence thesis;
end;
then reconsider Y as Subset-Family of T;
A5: Y c= B
proof
let y be object;
assume y in Y;
then ex V being Subset of T st y = V & V in B & V c= A;
hence thesis;
end;
A = union Y
proof
hereby
let p be object;
assume
A6: p in A;
then p in A;
then reconsider q = p as Point of T;
A is open by A4;
then consider a being Subset of T such that
A7: a in B and
A8: q in a and
A9: a c= A by A2,A6;
a in Y by A7,A9;
hence p in union Y by A8,TARSKI:def 4;
end;
let p be object;
assume p in union Y;
then consider a being set such that
A10: p in a and
A11: a in Y by TARSKI:def 4;
ex V being Subset of T st a = V & V in B & V c= A by A11;
hence thesis by A10;
end;
hence thesis by A5,CANTOR_1:def 1;
end;
hence thesis by A3;
end;
theorem Th33:
for S being TopSpace, T being non empty TopSpace, K being Basis of T
for f being Function of S,T holds
f is continuous iff for A being Subset of T st A in K holds f"A` is closed
proof
let S be TopSpace, T be non empty TopSpace,
BB be Basis of T, f be Function of S,T;
A1: BB c= the topology of T by TOPS_2:64;
hereby
assume
A2: f is continuous;
let A be Subset of T;
assume A in BB;
then A is open by A1;
then A` is closed by TOPS_1:4;
hence f"A` is closed by A2;
end;
assume
A3: for A being Subset of T st A in BB holds f"A` is closed;
let A be Subset of T;
assume A is closed;
then A` is open by TOPS_1:3;
then
A4: A` = union {G where G is Subset of T: G in BB & G c= A`} by YELLOW_8:9;
set F = {f"G where G is Subset of T: G in BB & G c= A`};
F c= bool the carrier of S
proof
let a be object;
assume a in F;
then ex G being Subset of T st a = f"G & G in BB & G c= A`;
hence thesis;
end;
then reconsider F as Subset-Family of S;
reconsider F as Subset-Family of S;
F c= the topology of S
proof
let a be object;
assume a in F;
then consider G being Subset of T such that
A5: a = f"G and
A6: G in BB and G c= A`;
A7: f"G` is closed by A3,A6;
(f"G)` = f"G` by Th2;
then f"G is open by A7,TOPS_1:4;
hence thesis by A5;
end;
then
A8: union F in the topology of S by PRE_TOPC:def 1;
defpred P[Subset of T] means $1 in BB & $1 c= A`;
deffunc F(Subset of T) = $1;
f"union {F(G) where G is Subset of T: P[G]}
= union {f"F(G) where G is Subset of T: P[G]} from ABC;
then f"A` is open by A4,A8;
then (f"A)` is open by Th2;
hence thesis by TOPS_1:3;
end;
theorem
for S being TopSpace,T being non empty TopSpace, K being Basis of T
for f being Function of S,T holds
f is continuous iff for A being Subset of T st A in K holds f"A is open
proof
let S be TopSpace,T be non empty TopSpace, K be Basis of T;
let f be Function of S,T;
hereby
assume
A1: f is continuous;
let A be Subset of T;
assume A in K;
then f"A` is closed by A1,Th33;
then (f"A)` is closed by Th2;
hence f"A is open by TOPS_1:4;
end;
assume
A2: for A being Subset of T st A in K holds f"A is open;
now
let A be Subset of T;
assume A in K;
then f"A is open by A2;
then (f"A)` is closed by TOPS_1:4;
hence f"A` is closed by Th2;
end;
hence thesis by Th33;
end;
theorem Th35:
for S being TopSpace,T being non empty TopSpace, K being prebasis of T
for f being Function of S,T holds
f is continuous iff for A being Subset of T st A in K holds f"A` is closed
proof
let S be TopSpace,T be non empty TopSpace,
BB be prebasis of T, f be Function of S,T;
A1: BB c= the topology of T by TOPS_2:64;
hereby
assume
A2: f is continuous;
let A be Subset of T;
assume A in BB;
then A is open by A1;
then A` is closed by TOPS_1:4;
hence f"A` is closed by A2;
end;
assume
A3: for A being Subset of T st A in BB holds f"A` is closed;
reconsider C = FinMeetCl BB as Basis of T by Th23;
now
let A be Subset of T;
assume A in C;
then consider Y being Subset-Family of T such that
A4: Y c= BB and
A5: Y is finite and
A6: A = Intersect Y by CANTOR_1:def 3;
reconsider Y as Subset-Family of T;
reconsider CY = COMPLEMENT Y as Subset-Family of T;
defpred P[set] means $1 in Y;
deffunc F(Subset of T) = $1`;
A7: f"A` = f"union CY by A6,YELLOW_8:7
.= f"union {F(a) where a is Subset of T: P[a]} by Th3
.= union {f"F(y) where y is Subset of T: P[y]} from ABC;
set X = {f"y` where y is Subset of T: y in Y};
X c= bool the carrier of S
proof
let x be object;
assume x in X;
then ex y being Subset of T st x = f"y` & y in Y;
hence thesis;
end;
then reconsider X as Subset-Family of S;
reconsider X as Subset-Family of S;
A8: X is closed
proof
let a be Subset of S;
assume a in X;
then ex y being Subset of T st a = f"y` & y in Y;
hence thesis by A3,A4;
end;
A9: Y is finite by A5;
deffunc F(Subset of T) = f"$1`;
{F(y) where y is Subset of T: y in Y} is finite from FRAENKEL:sch 21(
A9);
hence f"A` is closed by A7,A8,TOPS_2:21;
end;
hence thesis by Th33;
end;
theorem
for S being TopSpace,T being non empty TopSpace, K being prebasis of T
for f being Function of S,T holds
f is continuous iff for A being Subset of T st A in K holds f"A is open
proof
let S be TopSpace,T be non empty TopSpace, K be prebasis of T;
let f be Function of S,T;
hereby
assume
A1: f is continuous;
let A be Subset of T;
assume A in K;
then f"A` is closed by A1,Th35;
then (f"A)` is closed by Th2;
hence f"A is open by TOPS_1:4;
end;
assume
A2: for A being Subset of T st A in K holds f"A is open;
now
let A be Subset of T;
assume A in K;
then f"A is open by A2;
then (f"A)` is closed by TOPS_1:4;
hence f"A` is closed by Th2;
end;
hence thesis by Th35;
end;
theorem Th37:
for T being non empty TopSpace, x being Point of T, X being Subset of T
for K being Basis of T
st for A being Subset of T st A in K & x in A holds A meets X
holds x in Cl X
proof
let T be non empty TopSpace, x be Point of T, X be Subset of T;
let BB be Basis of T such that
A1: for A being Subset of T st A in BB & x in A holds A meets X;
now
let G be a_neighborhood of x;
A2: Int
G = union {A where A is Subset of T: A in BB & A c= G} by YELLOW_8:11;
x in Int G by CONNSP_2:def 1;
then consider Z being set such that
A3: x in Z and
A4: Z in {A where A is Subset of T: A in BB & A c= G} by A2,TARSKI:def 4;
ex A being Subset of T st ( Z = A)&( A in BB)&( A c= G) by A4;
hence G meets X by A1,A3,XBOOLE_1:63;
end;
hence thesis by CONNSP_2:27;
end;
theorem Th38:
for T being non empty TopSpace, x being Point of T, X being Subset of T
for K being prebasis of T
st for Z being finite Subset-Family of T st Z c= K & x in Intersect Z
holds Intersect Z meets X holds x in Cl X
proof
let T be non empty TopSpace, x be Point of T, X be Subset of T;
let BB be prebasis of T such that
A1: for Z being finite Subset-Family of T st Z c= BB & x in Intersect Z
holds Intersect Z meets X;
reconsider BB9 = FinMeetCl BB as Basis of T by Th23;
now
let A be Subset of T;
assume A in BB9;
then
A2: ex Y being Subset-Family of T st ( Y c= BB)&( Y is finite)&
( A = Intersect Y) by CANTOR_1:def 3;
assume x in A;
hence A meets X by A1,A2;
end;
hence thesis by Th37;
end;
theorem
for T being non empty TopSpace, K being prebasis of T, x being Point of T
for N being net of T
st for A being Subset of T st A in K & x in A holds N is_eventually_in A
for S being Subset of T st rng netmap(N,T) c= S holds x in Cl S
proof
let T be non empty TopSpace, BB be prebasis of T, x be Point of T,
N be net of T such that
A1: for A being Subset of T st A in BB & x in A holds N is_eventually_in A;
let S be Subset of T such that
A2: rng netmap(N,T) c= S;
A3: [#]N is directed by WAYBEL_0:def 6;
now
let Z be finite Subset-Family of T;
assume that
A4: Z c= BB and
A5: x in Intersect Z;
defpred P[object,object] means
for i,j being Element of N st $2 = i & i <= j
ex pp being set st pp = $1 & N.j in pp;
A6: now
let a be object;
assume
A7: a in Z;
then reconsider A = a as Subset of T;
x in A by A5,A7,SETFAM_1:43;
then N is_eventually_in A by A1,A4,A7;
then consider i being Element of N such that
A8: for j being Element of N st i <= j holds N.j in A;
reconsider b = i as object;
take b;
thus b in the carrier of N & P[a, b] by A8;
end;
consider f being Function such that
A9: dom f = Z & rng f c= the carrier of N &
for a being object st a in Z holds P[a, f.a]
from FUNCT_1:sch 6(A6);
set k = the Element of N;
per cases by A9,RELAT_1:42;
suppose Z = {};
then
A10: Intersect Z = the carrier of T by SETFAM_1:def 9;
N.k in rng netmap(N,T) by FUNCT_2:4;
hence Intersect Z meets S by A2,A10,XBOOLE_0:3;
end;
suppose rng f <> {};
then reconsider Y = rng f as finite non empty Subset of N
by A9,FINSET_1:8;
consider i being Element of N such that
i in the carrier of N and
A11: i is_>=_than Y by A3,WAYBEL_0:1;
now
let y be set;
assume
A12: y in Z;
then
A13: f.y in Y by A9,FUNCT_1:def 3;
then reconsider j = f.y as Element of N;
A14: j <= i by A11,A13,LATTICE3:def 9;
P[y,j] by A9,A12;
then ex pp being set st pp = y & N.i in pp by A14;
hence N.i in y;
end;
then
A15: N.i in Intersect Z by SETFAM_1:43;
N.i in rng netmap(N,T) by FUNCT_2:4;
hence Intersect Z meets S by A2,A15,XBOOLE_0:3;
end;
end;
hence thesis by Th38;
end;
begin :: Product topology
theorem Th40:
for T1,T2 being non empty TopSpace
for B1 being Basis of T1, B2 being Basis of T2 holds
{[:a,b:] where a is Subset of T1, b is Subset of T2: a in B1 & b in B2}
is Basis of [:T1,T2:]
proof
let T1,T2 be non empty TopSpace;
let B1 be Basis of T1, B2 be Basis of T2;
set BB = {[:a,b:] where a is Subset of T1, b is Subset of T2:
a in B1 & b in B2};
set T = [:T1,T2:];
A1: the carrier of T = [:the carrier of T1, the carrier of T2:]
by BORSUK_1:def 2;
BB c= bool the carrier of T
proof
let x be object;
assume x in BB;
then ex a being Subset of T1, b being Subset of T2 st x = [:a,b:] &
a in B1 & b in B2;
hence thesis;
end;
then reconsider BB as Subset-Family of T;
A2: B1 c= the topology of T1 by TOPS_2:64;
A3: B2 c= the topology of T2 by TOPS_2:64;
BB is Basis of T
proof
A4: BB is open
proof
let x be Subset of T;
assume x in BB;
then consider a being Subset of T1, b being Subset of T2 such that
A5: x = [:a,b:] and
A6: a in B1 and
A7: b in B2;
A8: a is open by A2,A6;
b is open by A3,A7;
hence x is open by A5,A8,BORSUK_1:6;
end;
BB is quasi_basis
proof
let x be object;
assume
A9: x in the topology of T;
then reconsider X = x as Subset of T;
X is open by A9;
then
A10: X = union Base-Appr X by BORSUK_1:13;
set Y = BB /\ Base-Appr X;
A11: Y c= BB by XBOOLE_1:17;
reconsider Y as Subset-Family of T;
union Y = X
proof
thus union Y c= X by A10,XBOOLE_1:17,ZFMISC_1:77;
let z be object;
assume
A12: z in X;
then reconsider p = z as Point of T;
consider z1,z2 being object such that
A13: z1 in the carrier of T1 and
A14: z2 in the carrier of T2 and
A15: p = [z1,z2] by A1,ZFMISC_1:def 2;
reconsider z1 as Point of T1 by A13;
reconsider z2 as Point of T2 by A14;
consider Z being set such that
A16: z in Z and
A17: Z in Base-Appr X by A10,A12,TARSKI:def 4;
A18: Base-Appr X = {[:a,b:] where a is Subset of T1, b is Subset of T2:
[:a,b:] c= X & a is open & b is open} by BORSUK_1:def 3;
then consider a being Subset of T1, b being Subset of T2 such that
A19: Z = [:a,b:] and
A20: [:a,b:] c= X and
A21: a is open and
A22: b is open by A17;
A23: z1 in a by A15,A16,A19,ZFMISC_1:87;
A24: z2 in b by A15,A16,A19,ZFMISC_1:87;
consider a9 being Subset of T1 such that
A25: a9 in B1 and
A26: z1 in a9 and
A27: a9 c= a by A21,A23,Th31;
consider b9 being Subset of T2 such that
A28: b9 in B2 and
A29: z2 in b9 and
A30: b9 c= b by A22,A24,Th31;
[:a9,b9:] c= [:a,b:] by A27,A30,ZFMISC_1:96;
then
A31: [:a9,b9:] c= X by A20;
A32: a9 is open by A2,A25;
b9 is open by A3,A28;
then
A33: [:a9,b9:] in Base-Appr X by A18,A31,A32;
A34: [:a9,b9:] in BB by A25,A28;
A35: p in [:a9,b9:] by A15,A26,A29,ZFMISC_1:87;
[:a9,b9:] in Y by A33,A34,XBOOLE_0:def 4;
hence thesis by A35,TARSKI:def 4;
end;
hence thesis by A11,CANTOR_1:def 1;
end;
hence thesis by A4;
end;
hence thesis;
end;
theorem Th41:
for T1,T2 being non empty TopSpace
for B1 being prebasis of T1, B2 being prebasis of T2 holds
{[:the carrier of T1, b:] where b is Subset of T2: b in B2} \/
{[:a, the carrier of T2:] where a is Subset of T1: a in B1}
is prebasis of [:T1,T2:]
proof
let T1,T2 be non empty TopSpace;
set T = [:T1,T2:];
let B1 be prebasis of T1, B2 be prebasis of T2;
set C2 = {[:the carrier of T1, b:] where b is Subset of T2: b in B2};
set C1 = {[:a, the carrier of T2:] where a is Subset of T1: a in B1};
reconsider D1 = FinMeetCl B1 as Basis of T1 by Th23;
reconsider D2 = FinMeetCl B2 as Basis of T2 by Th23;
reconsider D = {[:a,b:] where a is Subset of T1, b is Subset of T2:
a in D1 & b in D2} as Basis of T by Th40;
the carrier of T1 c= the carrier of T1;
then reconsider cT1 = the carrier of T1 as Subset of T1;
the carrier of T2 c= the carrier of T2;
then reconsider cT2 = the carrier of T2 as Subset of T2;
A1: cT1 in the topology of T1 by PRE_TOPC:def 1;
A2: cT2 in the topology of T2 by PRE_TOPC:def 1;
A3: B1 c= the topology of T1 by TOPS_2:64;
A4: B2 c= the topology of T2 by TOPS_2:64;
C1 c= bool the carrier of T
proof
let x be object;
assume x in C1;
then ex a being Subset of T1 st x = [:a, cT2:] & a in B1;
hence thesis;
end;
then reconsider C1 as Subset-Family of T;
reconsider C1 as Subset-Family of T;
C2 c= bool the carrier of T
proof
let x be object;
assume x in C2;
then ex a being Subset of T2 st x = [:cT1, a:] & a in B2;
hence thesis;
end;
then reconsider C2 as Subset-Family of T;
reconsider C2 as Subset-Family of T;
reconsider C = C2 \/ C1 as Subset-Family of T;
C is prebasis of T
proof
A5: C is open
proof
let x be Subset of T;
assume x in C;
then x in C1 or x in C2 by XBOOLE_0:def 3;
then (ex a being Subset of T1 st x = [:a, cT2:] & a in B1) or
ex a being Subset of T2 st x = [:cT1, a:] & a in B2;
then consider a being Subset of T1, b being Subset of T2 such that
A6: x = [:a,b:] and
A7: a in the topology of T1 and
A8: b in the topology of T2 by A1,A2,A3,A4;
A9: a is open by A7;
b is open by A8;
hence x is open by A6,A9,BORSUK_1:6;
end;
C is quasi_prebasis
proof
take D;
let d be object;
assume d in D;
then consider a being Subset of T1, b being Subset of T2 such that
A10: d = [:a,b:] and
A11: a in D1 and
A12: b in D2;
consider aY being Subset-Family of T1 such that
A13: aY c= B1 and
A14: aY is finite and
A15: a = Intersect aY by A11,CANTOR_1:def 3;
consider bY being Subset-Family of T2 such that
A16: bY c= B2 and
A17: bY is finite and
A18: b = Intersect bY by A12,CANTOR_1:def 3;
deffunc F(Subset of T1) = [:$1, cT2:];
A19: {F(s) where s is Subset of T1: s in aY} is finite
from FRAENKEL:sch 21(A14);
deffunc G(Subset of T2) = [:cT1, $1:];
A20: {G(s) where s is Subset of T2: s in bY} is finite
from FRAENKEL:sch 21(A17);
set Y1 = {[:s, cT2:] where s is Subset of T1: s in aY};
set Y2 = {[:cT1, s:] where s is Subset of T2: s in bY};
A21: Y1 c= C
proof
let x be object;
assume x in Y1;
then ex s being Subset of T1 st ( x = [:s, cT2:])&( s in aY);
then x in C1 by A13;
hence thesis by XBOOLE_0:def 3;
end;
A22: Y2 c= C
proof
let x be object;
assume x in Y2;
then ex s being Subset of T2 st ( x = [:cT1, s:])&( s in bY);
then x in C2 by A16;
hence thesis by XBOOLE_0:def 3;
end;
set Y = Y1 \/ Y2;
A23: Y c= C by A21,A22,XBOOLE_1:8;
then reconsider Y as Subset-Family of T by XBOOLE_1:1;
Intersect Y = [:a,b:]
proof
hereby
let p be object;
assume
A24: p in Intersect Y;
then consider p1 being Point of T1, p2 being Point of T2 such that
A25: p = [p1,p2] by BORSUK_1:10;
now
let z be set;
assume
A26: z in aY;
then reconsider z9 = z as Subset of T1;
[:z9, cT2:] in Y1 by A26;
then [:z9, cT2:] in Y by XBOOLE_0:def 3;
then p in [:z9, cT2:] by A24,SETFAM_1:43;
hence p1 in z by A25,ZFMISC_1:87;
end;
then
A27: p1 in a by A15,SETFAM_1:43;
now
let z be set;
assume
A28: z in bY;
then reconsider z9 = z as Subset of T2;
[:cT1, z9:] in Y2 by A28;
then [:cT1, z9:] in Y by XBOOLE_0:def 3;
then p in [:cT1, z9:] by A24,SETFAM_1:43;
hence p2 in z by A25,ZFMISC_1:87;
end;
then p2 in b by A18,SETFAM_1:43;
hence p in [:a,b:] by A25,A27,ZFMISC_1:87;
end;
let p be object;
assume p in [:a,b:];
then consider p1,p2 being object such that
A29: p1 in a and
A30: p2 in b and
A31: [p1,p2] = p by ZFMISC_1:def 2;
reconsider p1 as Point of T1 by A29;
reconsider p2 as Point of T2 by A30;
now
let z be set;
assume
A32: z in Y;
per cases by A32,XBOOLE_0:def 3;
suppose z in Y1;
then consider s being Subset of T1 such that
A33: z = [:s, cT2:] and
A34: s in aY;
p1 in s by A15,A29,A34,SETFAM_1:43;
hence [p1,p2] in z by A33,ZFMISC_1:87;
end;
suppose z in Y2;
then consider s being Subset of T2 such that
A35: z = [:cT1, s:] and
A36: s in bY;
p2 in s by A18,A30,A36,SETFAM_1:43;
hence [p1,p2] in z by A35,ZFMISC_1:87;
end;
end;
hence thesis by A31,SETFAM_1:43;
end;
hence thesis by A19,A20,A23,CANTOR_1:def 3,A10;
end;
hence thesis by A5;
end;
hence thesis;
end;
theorem
for X1,X2 being set, A being Subset-Family of [:X1,X2:]
for A1 being non empty Subset-Family of X1
for A2 being non empty Subset-Family of X2
st A = {[:a,b:] where a is Subset of X1, b is Subset of X2: a in A1 & b in
A2} holds Intersect A = [:Intersect A1, Intersect A2:]
proof
let X1,X2 be set, A be Subset-Family of [:X1,X2:];
let A1 be non empty Subset-Family of X1,
A2 be non empty Subset-Family of X2 such that
A1: A = {[:a,b:] where a is Subset of X1, b is Subset of X2: a in A1 & b in
A2};
hereby
let x be object;
assume
A2: x in Intersect A;
then consider x1,x2 being object such that
A3: x1 in X1 and
A4: x2 in X2 and
A5: [x1,x2] = x by ZFMISC_1:def 2;
set a1 = the Element of A1,a2 = the Element of A2;
reconsider a1 as Subset of X1;
reconsider a2 as Subset of X2;
now
let a be set;
assume a in A1;
then [:a,a2:] in A by A1;
then x in [:a,a2:] by A2,SETFAM_1:43;
hence x1 in a by A5,ZFMISC_1:87;
end;
then
A6: x1 in Intersect A1 by A3,SETFAM_1:43;
now
let a be set;
assume a in A2;
then [:a1,a:] in A by A1;
then x in [:a1,a:] by A2,SETFAM_1:43;
hence x2 in a by A5,ZFMISC_1:87;
end;
then x2 in Intersect A2 by A4,SETFAM_1:43;
hence x in [:Intersect A1, Intersect A2:] by A5,A6,ZFMISC_1:87;
end;
let x be object;
assume
A7: x in [:Intersect A1, Intersect A2:];
then consider x1,x2 being object such that
A8: x1 in Intersect A1 and
A9: x2 in Intersect A2 and
A10: [x1,x2] = x by ZFMISC_1:def 2;
now
let c be set;
assume c in A;
then consider a being Subset of X1, b being Subset of X2 such that
A11: c = [:a,b:] and
A12: a in A1 and
A13: b in A2 by A1;
A14: x1 in a by A8,A12,SETFAM_1:43;
x2 in b by A9,A13,SETFAM_1:43;
hence x in c by A10,A11,A14,ZFMISC_1:87;
end;
hence thesis by A7,SETFAM_1:43;
end;
theorem
for T1,T2 being non empty TopSpace
for B1 being prebasis of T1, B2 being prebasis of T2
st union B1 = the carrier of T1 & union B2 = the carrier of T2 holds
{[:a,b:] where a is Subset of T1, b is Subset of T2: a in B1 & b in B2}
is prebasis of [:T1,T2:]
proof
let T1,T2 be non empty TopSpace;
let B1 be prebasis of T1, B2 be prebasis of T2 such that
A1: union B1 = the carrier of T1 and
A2: union B2 = the carrier of T2;
set cT1 = the carrier of T1, cT2 = the carrier of T2;
set BB1 = {[:the carrier of T1, b:] where b is Subset of T2: b in B2},
BB2 = {[:a, the carrier of T2:] where a is Subset of T1: a in B1};
set CC = {[:a,b:] where a is Subset of T1, b is Subset of T2:
a in B1 & b in B2};
set T = [:T1,T2:];
reconsider BB=BB1 \/ BB2 as prebasis of [:T1,T2:] by Th41;
A3: FinMeetCl BB is Basis of T by Th23;
CC c= bool the carrier of [:T1,T2:]
proof
let x be object;
assume x in CC;
then ex a being Subset of T1, b being Subset of T2
st x = [:a,b:] & a in B1 & b in B2;
hence thesis;
end;
then reconsider CC as Subset-Family of [:T1,T2:];
reconsider CC as Subset-Family of [:T1,T2:];
CC c= the topology of T
proof
let x be object;
assume x in CC;
then consider a being Subset of T1, b being Subset of T2 such that
A4: x = [:a,b:] and
A5: a in B1 and
A6: b in B2;
A7: B1 c= the topology of T1 by TOPS_2:64;
A8: B2 c= the topology of T2 by TOPS_2:64;
A9: a is open by A5,A7;
b is open by A6,A8;
then [:a,b:] is open by A9,BORSUK_1:6;
hence thesis by A4;
end;
then UniCl CC c= UniCl the topology of T by CANTOR_1:9;
then
A10: UniCl CC c= the topology of T by CANTOR_1:6;
BB c= UniCl CC
proof
let x be object;
assume
A11: x in BB;
per cases by A11,XBOOLE_0:def 3;
suppose x in BB1;
then consider b being Subset of T2 such that
A12: x = [:cT1,b:] and
A13: b in B2;
set Y = {[:a,b:] where a is Subset of T1: a in B1};
Y c= bool the carrier of T
proof
let y be object;
assume y in Y;
then ex a being Subset of T1 st y = [:a,b:] & a in B1;
hence thesis;
end;
then reconsider Y as Subset-Family of T;
reconsider Y as Subset-Family of T;
A14: Y c= CC
proof
let y be object;
assume y in Y;
then ex a being Subset of T1 st y = [:a,b:] & a in B1;
hence thesis by A13;
end;
[:cT1,b:] = union Y
proof
hereby
let z be object;
assume z in [:cT1,b:];
then consider p1, p2 being object such that
A15: p1 in cT1 and
A16: p2 in b and
A17: [p1,p2] = z by ZFMISC_1:def 2;
consider a being set such that
A18: p1 in a and
A19: a in B1 by A1,A15,TARSKI:def 4;
reconsider a as Subset of T1 by A19;
A20: [:a,b:] in Y by A19;
z in [:a,b:] by A16,A17,A18,ZFMISC_1:def 2;
hence z in union Y by A20,TARSKI:def 4;
end;
let z be object;
assume z in union Y;
then consider y being set such that
A21: z in y and
A22: y in Y by TARSKI:def 4;
ex a being Subset of T1 st y = [:a,b:] & a in B1 by A22;
then y c= [:cT1,b:] by ZFMISC_1:95;
hence thesis by A21;
end;
hence thesis by A14,CANTOR_1:def 1,A12;
end;
suppose x in BB2;
then consider a being Subset of T1 such that
A23: x = [:a,cT2:] and
A24: a in B1;
set Y = {[:a,b:] where b is Subset of T2: b in B2};
Y c= bool the carrier of T
proof
let y be object;
assume y in Y;
then ex b being Subset of T2 st y = [:a,b:] & b in B2;
hence thesis;
end;
then reconsider Y as Subset-Family of T;
reconsider Y as Subset-Family of T;
A25: Y c= CC
proof
let y be object;
assume y in Y;
then ex b being Subset of T2 st y = [:a,b:] & b in B2;
hence thesis by A24;
end;
[:a,cT2:] = union Y
proof
hereby
let z be object;
assume z in [:a,cT2:];
then consider p1, p2 being object such that
A26: p1 in a and
A27: p2 in cT2 and
A28: [p1,p2] = z by ZFMISC_1:def 2;
consider b being set such that
A29: p2 in b and
A30: b in B2 by A2,A27,TARSKI:def 4;
reconsider b as Subset of T2 by A30;
A31: [:a,b:] in Y by A30;
z in [:a,b:] by A26,A28,A29,ZFMISC_1:def 2;
hence z in union Y by A31,TARSKI:def 4;
end;
let z be object;
assume z in union Y;
then consider y being set such that
A32: z in y and
A33: y in Y by TARSKI:def 4;
ex b being Subset of T2 st y = [:a,b:] & b in B2 by A33;
then y c= [:a,cT2:] by ZFMISC_1:95;
hence thesis by A32;
end;
hence thesis by A25,CANTOR_1:def 1,A23;
end;
end;
then FinMeetCl BB c= FinMeetCl UniCl CC by CANTOR_1:14;
then UniCl CC is prebasis of T by A3,A10,CANTOR_1:def 4,TOPS_2:64;
hence thesis by Th24;
end;
begin :: Topological augmentations
definition
let R be RelStr;
mode TopAugmentation of R -> TopRelStr means
:
Def4: the RelStr of it = the RelStr of R;
existence
proof
take TopRelStr(#the carrier of R, the InternalRel of R,
{}bool the carrier of R#);
thus thesis;
end;
end;
notation
let R be RelStr;
let T be TopAugmentation of R;
synonym T is correct for T is TopSpace-like;
end;
registration
let R be RelStr;
cluster correct discrete strict for TopAugmentation of R;
existence
proof reconsider BB = bool the carrier of R
as Subset-Family of R;
set T = TopRelStr(#the carrier of R, the InternalRel of R, BB#);
the RelStr of R = the RelStr of T;
then reconsider T as TopAugmentation of R by Def4;
take T;
T is discrete TopStruct by TDLAT_3:def 1;
hence thesis;
end;
end;
theorem
for T being TopRelStr holds T is TopAugmentation of T
proof
let T be TopRelStr;
thus the RelStr of T = the RelStr of T;
end;
theorem
for S being TopRelStr, T being TopAugmentation of S holds
S is TopAugmentation of T
proof
let S be TopRelStr, T be TopAugmentation of S;
thus the RelStr of S = the RelStr of T by Def4;
end;
theorem
for R being RelStr, T1 being TopAugmentation of R
for T2 being TopAugmentation of T1 holds T2 is TopAugmentation of R
proof
let R be RelStr, T1 be TopAugmentation of R;
let T2 be TopAugmentation of T1;
thus the RelStr of T2 = the RelStr of T1 by Def4
.= the RelStr of R by Def4;
end;
registration
let R be non empty RelStr;
cluster -> non empty for TopAugmentation of R;
coherence
proof
let T be TopAugmentation of R;
the RelStr of T = the RelStr of R by Def4;
hence the carrier of T is non empty;
end;
end;
registration
let R be reflexive RelStr;
cluster -> reflexive for TopAugmentation of R;
coherence
proof
let T be TopAugmentation of R;
the RelStr of T = the RelStr of R by Def4;
hence the InternalRel of T is_reflexive_in the carrier of T
by ORDERS_2:def 2;
end;
end;
registration
let R be transitive RelStr;
cluster -> transitive for TopAugmentation of R;
coherence
proof
let T be TopAugmentation of R;
the RelStr of T = the RelStr of R by Def4;
then the InternalRel of T is_transitive_in the carrier of T
by ORDERS_2:def 3;
hence thesis;
end;
end;
registration
let R be antisymmetric RelStr;
cluster -> antisymmetric for TopAugmentation of R;
coherence
proof
let T be TopAugmentation of R;
the RelStr of T = the RelStr of R by Def4;
then the InternalRel of T is_antisymmetric_in the carrier of T
by ORDERS_2:def 4;
hence thesis;
end;
end;
registration
let R be complete non empty RelStr;
cluster -> complete for TopAugmentation of R;
coherence
proof
let T be TopAugmentation of R;
the RelStr of T = the RelStr of R by Def4;
hence thesis by YELLOW_0:3;
end;
end;
theorem Th47:
for S being up-complete antisymmetric non empty reflexive RelStr,
T being non empty reflexive RelStr st the RelStr of S = the RelStr of T
for A being Subset of S, C being Subset of T st A = C & A is inaccessible
holds C is inaccessible
proof
let S be up-complete antisymmetric non empty reflexive RelStr,
T be non empty reflexive RelStr such that
A1: the RelStr of S = the RelStr of T;
let A be Subset of S, C be Subset of T such that
A2: A = C and
A3: for D being non empty directed Subset of S st sup D in A holds D meets A;
let D be non empty directed Subset of T such that
A4: sup D in C;
reconsider E = D as non empty directed Subset of S by A1,WAYBEL_0:3;
ex_sup_of E,S by WAYBEL_0:75;
then sup D = sup E by A1,YELLOW_0:26;
hence thesis by A2,A3,A4;
end;
theorem Th48:
for S being non empty reflexive RelStr, T being TopAugmentation of S
st the topology of T = sigma S holds T is correct
proof
let R be non empty reflexive RelStr;
let T be TopAugmentation of R such that
A1: the topology of T = sigma R;
A2: the RelStr of T = the RelStr of R by Def4;
set IT = ConvergenceSpace Scott-Convergence R;
A3: the carrier of IT = the carrier of R by YELLOW_6:def 24;
then
A4: the carrier of T in sigma R by A2,PRE_TOPC:def 1;
A5: for a being Subset-Family of T st a c= the topology of T holds union a
in the topology of T by A1,A2,A3,PRE_TOPC:def 1;
for a,b being Subset of T st a in the topology of T & b in the topology
of T holds a /\ b in the topology of T by A1,PRE_TOPC:def 1;
hence thesis by A1,A4,A5;
end;
theorem Th49:
for S being complete LATTICE, T being TopAugmentation of S
st the topology of T = sigma S holds T is Scott
proof
let R be complete LATTICE;
let T be TopAugmentation of R such that
A1: the topology of T = sigma R;
A2: the RelStr of T = the RelStr of R by Def4;
T is Scott
proof
let S be Subset of T;
reconsider A = S as Subset of R by A2;
thus S is open implies S is inaccessible upper
by A1,WAYBEL11:31,A2,Th47,WAYBEL_0:25;
assume S is inaccessible upper;
then A is inaccessible upper by A2,Th47,WAYBEL_0:25;
hence S in the topology of T by A1,WAYBEL11:31;
end;
hence thesis;
end;
registration
let R be complete LATTICE;
cluster Scott strict correct for TopAugmentation of R;
existence
proof
set T = TopRelStr(#the carrier of R, the InternalRel of R, sigma R#);
the RelStr of T = the RelStr of R;
then reconsider T as TopAugmentation of R by Def4;
take T;
thus thesis by Th48,Th49;
end;
end;
theorem Th50:
for S,T being complete
Scott non empty reflexive transitive antisymmetric TopRelStr
st the RelStr of S = the RelStr of T
for F being Subset of S, G being Subset of T st F = G
holds F is open implies G is open
proof
let S,T be complete
Scott non empty reflexive transitive antisymmetric TopRelStr such that
A1: the RelStr of S = the RelStr of T;
let F be Subset of S, G be Subset of T;
assume that
A2: F = G and
A3: F is open;
F is upper inaccessible by A3,WAYBEL11:def 4;
then G is upper inaccessible by A1,A2,Th47,WAYBEL_0:25;
hence thesis by WAYBEL11:def 4;
end;
theorem Th51:
for S being complete LATTICE, T being Scott TopAugmentation of S
holds the topology of T = sigma S
proof
let S be complete LATTICE;
let T be Scott TopAugmentation of S;
set R = TopRelStr(#the carrier of S, the InternalRel of S, sigma S#);
the RelStr of R = the RelStr of S;
then reconsider R as TopAugmentation of S by Def4;
reconsider R as correct Scott TopAugmentation of S by Th48,Th49;
A1: the RelStr of T = the RelStr of R by Def4;
thus the topology of T c= sigma S
proof
let x be object;
assume
A2: x in the topology of T;
then reconsider A = x as Subset of T;
reconsider C = A as Subset of R by A1;
A is open by A2;
then C is open by A1,Th50;
hence thesis;
end;
let x be object;
assume
A3: x in sigma S;
then reconsider A = x as Subset of R;
reconsider C = A as Subset of T by A1;
A is open by A3;
then C is open by A1,Th50;
hence thesis;
end;
theorem
for S,T being complete LATTICE st the RelStr of S = the RelStr of T
holds sigma S = sigma T
proof
let S,T be complete LATTICE such that
A1: the RelStr of S = the RelStr of T;
set A = the Scott correct TopAugmentation of S;
the RelStr of A = the RelStr of S by Def4;
then A is Scott correct TopAugmentation of T by A1,Def4;
then the topology of A = sigma T by Th51;
hence thesis by Th51;
end;
registration
let R be complete LATTICE;
cluster Scott -> correct for TopAugmentation of R;
coherence
proof
let T be TopAugmentation of R;
assume T is Scott;
then the topology of T = sigma R by Th51;
hence thesis by Th48;
end;
end;
Lm1: for S being TopStruct
ex T being strict TopSpace st the carrier of T = the carrier of S &
the topology of S is prebasis of T
proof
let S be TopStruct;
set T = TopStruct(#the carrier of S, UniCl FinMeetCl the topology of S#);
A1: {{},{}} = {{}} by ENUMSET1:29;
now
assume
A2: the carrier of S = {};
then the topology of S = {} or the topology of S = {{}} by ZFMISC_1:1,33;
then FinMeetCl the topology of S = {{}} by A1,A2,Th11,Th17;
then UniCl FinMeetCl the topology of S = {{}} by A1,Th11;
hence T is discrete TopStruct by A2,TDLAT_3:def 1,ZFMISC_1:1;
end;
then reconsider T as strict TopSpace by CANTOR_1:15;
take T;
A3: the topology of S c= FinMeetCl the topology of S by CANTOR_1:4;
FinMeetCl the topology of S c= the topology of T by CANTOR_1:1;
then
A4: the topology of S c= the topology of T by A3;
FinMeetCl the topology of S is Basis of T by Th22;
hence thesis by A4,CANTOR_1:def 4,TOPS_2:64;
end;
begin :: Refinements
definition
let T be TopStruct;
mode TopExtension of T -> TopSpace means
:
Def5: the carrier of T = the carrier of it &
the topology of T c= the topology of it;
existence
proof consider R being strict TopSpace such that
A1: the carrier of R = the carrier of T and
A2: the topology of T is prebasis of R by Lm1;
take R;
thus thesis by A1,A2,TOPS_2:64;
end;
end;
theorem Th53:
for S being TopStruct ex T being TopExtension of S st
T is strict & the topology of S is prebasis of T
proof
let S be TopStruct;
consider T being strict TopSpace such that
A1: the carrier of T = the carrier of S and
A2: the topology of S is prebasis of T by Lm1;
the topology of S c= the topology of T by A2,TOPS_2:64;
then reconsider T as TopExtension of S by A1,Def5;
take T;
thus thesis by A2;
end;
registration
let T be TopStruct;
cluster strict discrete for TopExtension of T;
existence
proof
reconsider S = bool the carrier of T as Subset-Family of T;
reconsider S as Subset-Family of T;
set R = TopStruct(#the carrier of T, S#);
A1: R is discrete TopStruct by TDLAT_3:def 1;
the topology of T c= S;
then R is TopExtension of T by A1,Def5;
hence thesis by A1;
end;
end;
definition
let T1,T2 be TopStruct;
mode Refinement of T1,T2 -> TopSpace means
:
Def6: the carrier of it = (the carrier of T1) \/ (the carrier of T2) &
(the topology of T1) \/ (the topology of T2) is prebasis of it;
existence
proof
set c1 = the carrier of T1, c2 = the carrier of T2;
set t1 = the topology of T1, t2 = the topology of T2;
A1: bool c1 c= bool (c1 \/ c2) by XBOOLE_1:7,ZFMISC_1:67;
A2: bool c2 c= bool (c1 \/ c2) by XBOOLE_1:7,ZFMISC_1:67;
A3: t1 c= bool (c1 \/ c2) by A1;
t2 c= bool (c1 \/ c2) by A2;
then reconsider t = t1 \/ t2 as Subset-Family of (c1 \/ c2) by A3,
XBOOLE_1:8;
reconsider t as Subset-Family of c1 \/ c2;
set S = TopStruct(#c1 \/ c2, t#);
consider T being TopExtension of S such that
A4: T is strict and
A5: t is prebasis of T by Th53;
reconsider T as strict TopExtension of S by A4;
take T;
thus thesis by A5,Def5;
end;
end;
registration
let T1 be non empty TopStruct, T2 be TopStruct;
cluster -> non empty for Refinement of T1,T2;
coherence
proof
let T be Refinement of T1,T2;
the carrier of T = (the carrier of T2) \/ (the carrier of T1) by Def6;
hence the carrier of T is non empty;
end;
cluster -> non empty for Refinement of T2,T1;
coherence
proof
let T be Refinement of T2,T1;
the carrier of T = (the carrier of T2) \/ (the carrier of T1) by Def6;
hence the carrier of T is non empty;
end;
end;
theorem
for T1,T2 being TopStruct, T, T9 being Refinement of T1,T2 holds
the TopStruct of T = the TopStruct of T9
proof
let T1, T2 be TopStruct, T,T9 be Refinement of T1,T2;
A1: the carrier of T = (the carrier of T1) \/ (the carrier of T2) by Def6;
A2: (the topology of T1) \/ (the topology of T2) is prebasis of T by Def6;
A3: the carrier of T9 = (the carrier of T1) \/ (the carrier of T2) by Def6;
(the topology of T1) \/ (the topology of T2) is prebasis of T9 by Def6;
hence thesis by A1,A2,A3,Th26;
end;
theorem
for T1,T2 being TopStruct, T being Refinement of T1,T2
holds T is Refinement of T2,T1
proof
let T1, T2 be TopStruct, T be Refinement of T1,T2;
A1: the carrier of T = (the carrier of T1) \/ (the carrier of T2) by Def6;
(the topology of T1) \/ (the topology of T2) is prebasis of T by Def6;
hence thesis by A1,Def6;
end;
theorem
for T1,T2 being TopStruct, T being Refinement of T1,T2
for X being Subset-Family of T
st X = (the topology of T1) \/ (the topology of T2)
holds the topology of T = UniCl FinMeetCl X
proof
let T1,T2 be TopStruct, T be Refinement of T1,T2;
let X be Subset-Family of T;
assume X = (the topology of T1) \/ (the topology of T2);
then X is prebasis of T by Def6;
then FinMeetCl X is Basis of T by Th23;
hence thesis by Th22;
end;
theorem
for T1, T2 being TopStruct st the carrier of T1 = the carrier of T2
for T being Refinement of T1, T2
holds T is TopExtension of T1 & T is TopExtension of T2
proof
let T1, T2 be TopStruct such that
A1: the carrier of T1 = the carrier of T2;
let T be Refinement of T1, T2;
A2: the carrier of T = (the carrier of T1) \/ the carrier of T2 by Def6
.= the carrier of T1 by A1;
A3: (the topology of T1) \/ the topology of T2 is prebasis of T by Def6;
A4: the topology of T1 c= (the topology of T1) \/ the topology of T2 by
XBOOLE_1:7;
A5: the topology of T2 c= (the topology of T1) \/ the topology of T2 by
XBOOLE_1:7;
A6: (the topology of T1) \/ the topology of T2 c= the topology of T by A3,
TOPS_2:64;
then
A7: the topology of T1 c= the topology of T by A4;
the topology of T2 c= the topology of T by A5,A6;
hence thesis by A1,A2,A7,Def5;
end;
theorem
for T1,T2 being non empty TopSpace, T be Refinement of T1, T2
for B1 being prebasis of T1, B2 being prebasis of T2
holds B1 \/ B2 \/ {the carrier of T1, the carrier of T2} is prebasis of T
proof
let T1,T2 be non empty TopSpace, T be Refinement of T1,T2;
let B1 be prebasis of T1, B2 be prebasis of T2;
reconsider B = (the topology of T1) \/ (the topology of T2) as prebasis of T
by Def6;
set cT1 = the carrier of T1, cT2 = the carrier of T2;
reconsider C1 = B1 \/ {cT1} as prebasis of T1 by Th29;
reconsider C2 = B2 \/ {cT2} as prebasis of T2 by Th29;
A1: B1 c= the topology of T1 by TOPS_2:64;
A2: C1 c= the topology of T1 by TOPS_2:64;
A3: B2 c= the topology of T2 by TOPS_2:64;
A4: C2 c= the topology of T2 by TOPS_2:64;
A5: cT1 in the topology of T1 by PRE_TOPC:def 1;
A6: cT2 in the topology of T2 by PRE_TOPC:def 1;
A7: B1 \/ B2 c= B by A1,A3,XBOOLE_1:13;
A8: B c= the topology of T by TOPS_2:64;
A9: cT1 in B by A5,XBOOLE_0:def 3;
A10: cT2 in B by A6,XBOOLE_0:def 3;
A11: B1 \/ B2 c= the topology of T by A7,A8;
A12: {cT1,cT2} c= the topology of T by A8,A9,A10,ZFMISC_1:32;
A13: {cT1,cT2} c= B by A9,A10,ZFMISC_1:32;
B1 \/ B2 \/ {cT1,cT2} c= the topology of T by A11,A12,XBOOLE_1:8;
then reconsider BB = B1 \/ B2 \/
{cT1, cT2} as Subset-Family of T by XBOOLE_1:1;
A14: the topology of T1 c= B by XBOOLE_1:7;
A15: the topology of T2 c= B by XBOOLE_1:7;
A16: C1 c= B by A2,A14;
C2 c= B by A4,A15;
then reconsider D1 = C1, D2 = C2 as Subset-Family of T by A16,XBOOLE_1:1;
reconsider D1, D2 as Subset-Family of T;
reconsider D1, D2 as Subset-Family of T;
A17: UniCl FinMeetCl BB = UniCl FinMeetCl FinMeetCl BB by CANTOR_1:11
.= UniCl FinMeetCl UniCl FinMeetCl BB by Th21;
A18: FinMeetCl B is Basis of T by Th23;
A19: FinMeetCl C1 is Basis of T1 by Th23;
A20: FinMeetCl C2 is Basis of T2 by Th23;
A21: UniCl FinMeetCl B = the topology of T by A18,Th22;
A22: UniCl FinMeetCl C1 = the topology of T1 by A19,Th22;
A23: UniCl FinMeetCl C2 = the topology of T2 by A20,Th22;
A24: B1 c= B1 \/ B2 by XBOOLE_1:7;
A25: B2 c= B1 \/ B2 by XBOOLE_1:7;
A26: {cT1} c= {cT1,cT2} by ZFMISC_1:7;
A27: {cT2} c= {cT1, cT2 } by ZFMISC_1:7;
A28: D1 c= BB by A24,A26,XBOOLE_1:13;
A29: D2 c= BB by A25,A27,XBOOLE_1:13;
BB c= B by A7,A13,XBOOLE_1:8;
then
A30: FinMeetCl BB c= FinMeetCl B by CANTOR_1:14;
A31: FinMeetCl D1 c= FinMeetCl BB by A28,CANTOR_1:14;
A32: FinMeetCl D2 c= FinMeetCl BB by A29,CANTOR_1:14;
A33: UniCl FinMeetCl BB c= the topology of T by A21,A30,CANTOR_1:9;
A34: cT1 in {cT1} by TARSKI:def 1;
A35: cT2 in {cT2} by TARSKI:def 1;
A36: cT1 in C1 by A34,XBOOLE_0:def 3;
A37: cT2 in C2 by A35,XBOOLE_0:def 3;
A38: FinMeetCl D1 = {the carrier of T} \/ FinMeetCl C1 by A36,Th20;
A39: FinMeetCl D2 = {the carrier of T} \/ FinMeetCl C2 by A37,Th20;
A40: FinMeetCl C1 c= FinMeetCl D1 by A38,XBOOLE_1:7;
A41: FinMeetCl C2 c= FinMeetCl D2 by A39,XBOOLE_1:7;
A42: FinMeetCl C1 c= FinMeetCl BB by A31,A40;
A43: FinMeetCl C2 c= FinMeetCl BB by A32,A41;
A44: the topology of T1 c= UniCl FinMeetCl BB by A22,A42,Th19;
the topology of T2 c= UniCl FinMeetCl BB by A23,A43,Th19;
then B c= UniCl FinMeetCl BB by A44,XBOOLE_1:8;
then FinMeetCl B c= FinMeetCl UniCl FinMeetCl BB by CANTOR_1:14;
then the topology of T c= UniCl FinMeetCl BB by A17,A21,CANTOR_1:9;
then the topology of T = UniCl FinMeetCl BB by A33;
then FinMeetCl BB is Basis of T by Th22;
hence thesis by Th23;
end;
theorem Th59:
for T1,T2 being non empty TopSpace
for B1 being Basis of T1, B2 being Basis of T2
for T being Refinement of T1, T2
holds B1 \/ B2 \/ INTERSECTION(B1,B2) is Basis of T
proof
let T1,T2 be non empty TopSpace;
let B1 be Basis of T1, B2 be Basis of T2;
let T be Refinement of T1,T2;
set BB = B1 \/ B2 \/ INTERSECTION(B1,B2);
reconsider B = (the topology of T1) \/ the topology of T2 as prebasis of T
by Def6;
A1: FinMeetCl B is Basis of T by Th23;
A2: (the carrier of T1) \/ the carrier of T2 = the carrier of T by Def6;
A3: B1 c= the topology of T1 by TOPS_2:64;
A4: B2 c= the topology of T2 by TOPS_2:64;
A5: the topology of T1 c= B by XBOOLE_1:7;
A6: the topology of T2 c= B by XBOOLE_1:7;
A7: B1 c= B by A3,A5;
A8: B2 c= B by A4,A6;
A9: B c= FinMeetCl B by CANTOR_1:4;
then
A10: B1 c= FinMeetCl B by A7;
A11: B2 c= FinMeetCl B by A8,A9;
A12: B1 \/ B2 c= B by A3,A4,XBOOLE_1:13;
A13: INTERSECTION(B1,B2) c= FinMeetCl B by A10,A11,CANTOR_1:13;
B1 \/ B2 c= FinMeetCl B by A9,A12;
then
A14: BB c= FinMeetCl B by A13,XBOOLE_1:8;
A15: FinMeetCl B c= the topology of T by A1,TOPS_2:64;
reconsider BB as Subset-Family of T by A14,XBOOLE_1:1;
now
let A be Subset of T such that
A16: A is open;
let p be Point of T;
assume p in A;
then consider a being Subset of T such that
A17: a in FinMeetCl B and
A18: p in a and
A19: a c= A by A1,A16,Th31;
consider Y being Subset-Family of T such that
A20: Y c= B and
A21: Y is finite and
A22: a = Intersect Y by A17,CANTOR_1:def 3;
reconsider Y1 = Y /\ the topology of T1 as Subset-Family of T1;
reconsider Y2 = Y /\ the topology of T2 as Subset-Family of T2;
A23: Y = B /\ Y by A20,XBOOLE_1:28
.= Y1 \/ Y2 by XBOOLE_1:23;
the carrier of T1 c= the carrier of T1;
then reconsider cT1 = the carrier of T1 as Subset of T1;
the carrier of T2 c= the carrier of T2;
then reconsider cT2 = the carrier of T2 as Subset of T2;
A24: cT1 in the topology of T1 by PRE_TOPC:def 1;
A25: cT2 in the topology of T2 by PRE_TOPC:def 1;
A26: cT1 is open by A24;
A27: cT2 is open by A25;
thus ex a being Subset of T st a in BB & p in a & a c= A
proof per cases by A2,XBOOLE_0:def 3;
suppose
A28: Y1 \/ Y2 = {} & p in cT1;
then consider b1 being Subset of T1 such that
A29: b1 in B1 and
A30: p in b1 and b1 c= cT1 by A26,Th31;
A31: b1 in B1 \/ B2 by A29,XBOOLE_0:def 3;
A32: a = the carrier of T by A22,A23,A28,SETFAM_1:def 9;
b1 in BB by A31,XBOOLE_0:def 3;
hence thesis by A19,A30,A32,XBOOLE_1:1;
end;
suppose
A33: Y1 \/ Y2 = {} & p in cT2;
then consider b2 being Subset of T2 such that
A34: b2 in B2 and
A35: p in b2 and b2 c= cT2 by A27,Th31;
A36: b2 in B1 \/ B2 by A34,XBOOLE_0:def 3;
A37: a = the carrier of T by A22,A23,A33,SETFAM_1:def 9;
b2 in BB by A36,XBOOLE_0:def 3;
hence thesis by A19,A35,A37,XBOOLE_1:1;
end;
suppose
A38: Y1 = {} & Y2 <> {} & Y <> {};
then
A39: a = meet Y2 by A22,A23,SETFAM_1:def 9
.= Intersect Y2 by A38,SETFAM_1:def 9;
Y2 c= the topology of T2 by XBOOLE_1:17;
then a in FinMeetCl the topology of T2 by A21,A39,CANTOR_1:def 3;
then
A40: a in the topology of T2 by CANTOR_1:5;
the topology of T2 = UniCl B2 by Th22;
then consider Z being Subset-Family of T2 such that
A41: Z c= B2 and
A42: a = union Z by A40,CANTOR_1:def 1;
consider z being set such that
A43: p in z and
A44: z in Z by A18,A42,TARSKI:def 4;
z in B1 \/ B2 by A41,A44,XBOOLE_0:def 3;
then
A45: z in BB by XBOOLE_0:def 3;
z c= a by A42,A44,ZFMISC_1:74;
hence thesis by A19,A43,A45,XBOOLE_1:1;
end;
suppose
A46: Y1 <> {} & Y2 = {} & Y <> {};
then
A47: a = meet Y1 by A22,A23,SETFAM_1:def 9
.= Intersect Y1 by A46,SETFAM_1:def 9;
Y1 c= the topology of T1 by XBOOLE_1:17;
then a in FinMeetCl the topology of T1 by A21,A47,CANTOR_1:def 3;
then
A48: a in the topology of T1 by CANTOR_1:5;
the topology of T1 = UniCl B1 by Th22;
then consider Z being Subset-Family of T1 such that
A49: Z c= B1 and
A50: a = union Z by A48,CANTOR_1:def 1;
consider z being set such that
A51: p in z and
A52: z in Z by A18,A50,TARSKI:def 4;
z in B1 \/ B2 by A49,A52,XBOOLE_0:def 3;
then
A53: z in BB by XBOOLE_0:def 3;
z c= a by A50,A52,ZFMISC_1:74;
hence thesis by A19,A51,A53,XBOOLE_1:1;
end;
suppose
A54: Y1 <> {} & Y2 <> {} & Y <> {};
then
A55: a = meet Y by A22,SETFAM_1:def 9
.= (meet Y1)/\meet Y2 by A23,A54,SETFAM_1:9
.= (meet Y1)/\Intersect Y2 by A54,SETFAM_1:def 9
.= (Intersect Y1)/\Intersect Y2 by A54,SETFAM_1:def 9;
A56: Y1 c= the topology of T1 by XBOOLE_1:17;
A57: Y2 c= the topology of T2 by XBOOLE_1:17;
A58: Intersect Y1 in FinMeetCl the topology of T1 by A21,A56,CANTOR_1:def 3;
A59: Intersect Y2 in FinMeetCl the topology of T2 by A21,A57,CANTOR_1:def 3;
A60: Intersect Y1 in the topology of T1 by A58,CANTOR_1:5;
A61: the topology of T1 = UniCl B1 by Th22;
A62: Intersect Y2 in the topology of T2 by A59,CANTOR_1:5;
A63: the topology of T2 = UniCl B2 by Th22;
consider Z1 being Subset-Family of T1 such that
A64: Z1 c= B1 and
A65: Intersect Y1 = union Z1 by A60,A61,CANTOR_1:def 1;
p in Intersect Y1 by A18,A55,XBOOLE_0:def 4;
then consider z1 being set such that
A66: p in z1 and
A67: z1 in Z1 by A65,TARSKI:def 4;
consider Z2 being Subset-Family of T2 such that
A68: Z2 c= B2 and
A69: Intersect Y2 = union Z2 by A62,A63,CANTOR_1:def 1;
p in Intersect Y2 by A18,A55,XBOOLE_0:def 4;
then consider z2 being set such that
A70: p in z2 and
A71: z2 in Z2 by A69,TARSKI:def 4;
A72: z1 /\ z2 in INTERSECTION(B1,B2) by A64,A67,A68,A71,SETFAM_1:def 5;
A73: z1 c= union Z1 by A67,ZFMISC_1:74;
A74: z2 c= union Z2 by A71,ZFMISC_1:74;
A75: z1 /\ z2 in BB by A72,XBOOLE_0:def 3;
A76: z1 /\ z2 c= a by A55,A65,A69,A73,A74,XBOOLE_1:27;
p in z1 /\ z2 by A66,A70,XBOOLE_0:def 4;
hence thesis by A19,A75,A76,XBOOLE_1:1;
end;
end;
end;
hence thesis by A14,A15,Th32,XBOOLE_1:1;
end;
theorem Th60:
for T1,T2 being non empty TopSpace st the carrier of T1 = the carrier of T2
for T being Refinement of T1, T2
holds INTERSECTION(the topology of T1, the topology of T2) is Basis of T
proof
let T1,T2 be non empty TopSpace such that
A1: the carrier of T1 = the carrier of T2;
let T be Refinement of T1, T2;
set B1 = the topology of T1, B2 = the topology of T2;
UniCl B1 = B1 by CANTOR_1:6;
then reconsider B1 as Basis of T1 by Th22;
UniCl B2 = B2 by CANTOR_1:6;
then reconsider B2 as Basis of T2 by Th22;
A2: B1 \/ B2 \/ INTERSECTION(B1,B2) is Basis of T by Th59;
A3: the carrier of T1 in B1 by PRE_TOPC:def 1;
A4: the carrier of T2 in B2 by PRE_TOPC:def 1;
A5: B1 c= INTERSECTION(B1,B2)
proof
let a be object;
reconsider aa=a as set by TARSKI:1;
assume
A6: a in B1;
then aa /\ the carrier of T1 in INTERSECTION(B1,B2)
by A1,A4,SETFAM_1:def 5;
hence thesis by A6,XBOOLE_1:28;
end;
B2 c= INTERSECTION(B1,B2)
proof
let a be object;
reconsider aa=a as set by TARSKI:1;
assume
A7: a in B2;
then aa /\ the carrier of T2 in INTERSECTION(B1,B2)
by A1,A3,SETFAM_1:def 5;
hence thesis by A7,XBOOLE_1:28;
end;
hence thesis by A2,A5,XBOOLE_1:8,12;
end;
theorem
for L being non empty RelStr for T1,T2 being correct TopAugmentation of L
for T be Refinement of T1, T2
holds INTERSECTION(the topology of T1, the topology of T2) is Basis of T
proof
let L be non empty RelStr;
let T1,T2 be correct TopAugmentation of L;
A1: the RelStr of T1 = the RelStr of L by Def4;
the RelStr of T2 = the RelStr of L by Def4;
hence thesis by A1,Th60;
end;