Copyright (c) 1998 Association of Mizar Users
environ
vocabulary ORDERS_1, SETFAM_1, WAYBEL_0, SUBSET_1, BOOLE, PRE_TOPC, FUNCT_1,
RELAT_1, TARSKI, CANTOR_1, WAYBEL_9, REALSET1, RELAT_2, NATTRA_1,
FINSET_1, BHSP_3, LATTICES, FUNCOP_1, YELLOW_0, ORDINAL2, FUNCT_3,
SEQM_3, CAT_1, WELLORD1, OPPCAT_1, QUANTAL1, FUNCT_2, FRAENKEL, CONNSP_2,
TOPS_1, LATTICE3, BORSUK_1, PRELAMB, WAYBEL11, PROB_1, YELLOW_6,
YELLOW_9, RLVECT_3;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
FINSET_1, MCART_1, STRUCT_0, RELAT_2, RELSET_1, REALSET1, FRAENKEL,
FUNCT_2, WELLORD1, GRCAT_1, ORDERS_1, LATTICE3, ORDERS_3, YELLOW_0,
WAYBEL_0, TDLAT_3, GROUP_1, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_2, YELLOW_6,
YELLOW_7, WAYBEL_9, WAYBEL11, CANTOR_1, BORSUK_1;
constructors RELAT_2, WAYBEL11, CANTOR_1, TOPS_1, TDLAT_3, GROUP_1, TOLER_1,
WAYBEL_3, WAYBEL_5, ORDERS_3, WAYBEL_1, GRCAT_1, TOPS_2, BORSUK_1,
LATTICE3, PARTFUN1;
clusters TDLAT_3, FRAENKEL, YELLOW_6, YELLOW_2, FINSET_1, RELSET_1, BORSUK_1,
STRUCT_0, TEX_1, YELLOW_0, LATTICE3, WAYBEL_0, WAYBEL_7, WAYBEL_9,
WAYBEL11, SUBSET_1, RLVECT_2, FUNCT_2, SETFAM_1, XBOOLE_0, ZFMISC_1,
PARTFUN1;
requirements BOOLE, SUBSET;
definitions TARSKI, STRUCT_0, PRE_TOPC, CANTOR_1, ORDERS_1, GROUP_1, YELLOW_0,
WAYBEL_0, WAYBEL_1, TOPS_2, WAYBEL11, XBOOLE_0;
theorems STRUCT_0, SETFAM_1, FRAENKEL, ENUMSET1, REALSET1, PRE_TOPC, CANTOR_1,
YELLOW_0, WAYBEL_0, FUNCT_1, RELAT_1, FUNCT_2, TEX_1, ORDERS_1, ZFMISC_1,
TARSKI, FINSET_1, FUNCOP_1, RELSET_1, TDLAT_3, GRCAT_1, BORSUK_1,
YELLOW_6, YELLOW_8, TOPS_1, CONNSP_2, WAYBEL_9, WAYBEL11, TOPS_2,
LATTICE3, ORDERS_2, WELLORD1, XBOOLE_0, XBOOLE_1;
schemes FRAENKEL, COMPTS_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 set; assume
A3: x in X();
then reconsider a = x as Element of A();
F(a) in Y() & F(F(a)) = a by A1,A2,A3;
hence x in {F(b) where b is Element of A(): b in Y()};
end;
let x be set; assume
x in {F(b) where b is Element of A(): b in Y()};
then consider b being Element of A() such that
A4: x = F(b) & b in Y();
consider a being Element of A() such that
A5: b = F(a) & a in X() by A1,A4;
thus x in X() by A2,A4,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 set; assume
A2: x in COMPLEMENT X();
then reconsider y = x as Subset of A();
y` in X() by A2,YELLOW_8:13;
then consider b being Element of A() such that
A3: y` = F(b) & b in Y() by A1;
x = y`` & F(b) = F(b)``;
hence x in {F(a)` where a is Element of A(): a in Y()} by A3;
end;
let x be set; 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)` & a in Y();
F(a) in X() by A1,A4;
hence x in COMPLEMENT X() by A4,YELLOW_8:14;
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 set; assume
A2: x in COMPLEMENT X();
then reconsider y = x as Subset of A();
y` in X() by A2,YELLOW_8:13;
then consider b being Element of A() such that
A3: y` = F(b)` & b in Y() by A1;
x = y`` & F(b) = F(b)``;
hence x in {F(a) where a is Element of A(): a in Y()} by A3;
end;
let x be set; 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) & a in Y();
F(a)` in X() by A1,A4;
hence x in COMPLEMENT X() by A4,YELLOW_8:13;
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;
[#]R = the carrier of R by PRE_TOPC:12;
then (uparrow x)` = (the carrier of R) \ uparrow x by PRE_TOPC:17;
then y in (uparrow x)` iff not y in uparrow x by XBOOLE_0:def 4;
hence y in (uparrow x)` iff not x <= y by WAYBEL_0:18;
end;
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 set; assume x in f()"union X;
then A1: x in dom f() & f().x in union X by FUNCT_1:def 13;
then consider y being set such that
A2: f().x in y & y in X by TARSKI:def 4;
consider a being Subset of A() such that
A3: y = F(a) & P[a] by A2;
x in f()"F(a) & f()"F(a) in Y by A1,A2,A3,FUNCT_1:def 13;
hence x in union Y by TARSKI:def 4;
end;
let x be set; assume x in union Y;
then consider y being set such that
A4: x in y & y in Y by TARSKI:def 4;
consider a being Subset of A() such that
A5: y = f()"F(a) & P[a] by A4;
f().x in F(a) & F(a) in X by A4,A5,FUNCT_1:def 13;
then f().x in union X & x in dom f() by A4,A5,FUNCT_1:def 13,TARSKI:def 4;
hence thesis by FUNCT_1:def 13;
end;
theorem Th2:
for S being 1-sorted, T being non empty 1-sorted, f being map 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 map of S,T;
let X be Subset of T;
A1: the carrier of T = [#]T & the carrier of S = [#]S by PRE_TOPC:12;
hence (f"X)` = (the carrier of S)\(f"X) by PRE_TOPC:17
.= f"(the carrier of T)\(f"X) by FUNCT_2:48
.= f"((the carrier of T)\X) by FUNCT_1:138
.= f"X` by A1,PRE_TOPC:17;
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 set; assume
A1: x in COMPLEMENT F;
then reconsider P = x as Subset of T;
P` in F & P`` = P by A1,YELLOW_8:13;
hence x in X;
end;
let x be set; assume x in X;
then ex P being Subset of T st x = P` & P in F;
hence thesis by YELLOW_8:14;
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 set; assume a in uparrow F;
then consider x being Element of R such that
A3: a = x & ex y being Element of R st x >= y & y in F by A1;
consider y being Element of R such that
A4: x >= y & y in F by A3;
uparrow y in {uparrow z where z is Element of R: z in F} &
x in uparrow y by A4,WAYBEL_0:18;
hence a in union {uparrow z where z is Element of R: z in F}
by A3,TARSKI:def 4;
end;
hereby let a be set; assume
a in union {uparrow x where x is Element of R: x in F};
then consider X being set such that
A5: a in X & 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
A6: X = uparrow x & x in F by A5;
reconsider y = a as Element of R by A5,A6;
y >= x by A5,A6,WAYBEL_0:18;
hence a in uparrow F by A1,A6;
end;
hereby let a be set; assume a in downarrow F;
then consider x being Element of R such that
A7: a = x & ex y being Element of R st x <= y & y in F by A2;
consider y being Element of R such that
A8: x <= y & y in F by A7;
downarrow y in {downarrow z where z is Element of R: z in F} &
x in downarrow y by A8,WAYBEL_0:17;
hence a in union {downarrow z where z is Element of R: z in F}
by A7,TARSKI:def 4;
end;
hereby let a be set; assume
a in union {downarrow x where x is Element of R: x in F};
then consider X being set such that
A9: a in X & 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
A10: X = downarrow x & x in F by A9;
reconsider y = a as Element of R by A9,A10;
y <= x by A9,A10,WAYBEL_0:17;
hence a in downarrow F by A2,A10;
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:15
.= (uparrow F)` by A2,Th4;
end;
Lm1:
for tau being Subset-Family of {0}, r being Relation of {0}
st tau = {{},{0}} & r = {[0,0]}
holds TopRelStr (#{0},r,tau#) is trivial reflexive non empty discrete finite
proof
let tau be Subset-Family of {0}, r be Relation of {0} such that
A1: tau = {{},{0}} and
A2: r = {[0,0]};
set T = TopRelStr (#{0},r,tau#);
thus T is trivial;
thus T is reflexive
proof
let x be Element of T;
x = 0 by TARSKI:def 1;
then [x,x] in {[0,0]} by TARSKI:def 1;
hence x <= x by A2,ORDERS_1:def 9;
end;
thus T is non empty;
the topology of T = bool the carrier of T by A1,ZFMISC_1:30;
hence T is discrete by TDLAT_3:def 1;
thus the carrier of T is finite;
end;
definition
cluster strict trivial reflexive non empty discrete finite TopRelStr;
existence
proof
{{},{0}} = bool {0} & bool {0} c= bool {0} by ZFMISC_1:30;
then reconsider tau = {{},{0}} as Subset of bool {0};
reconsider tau as Subset-Family of {0} by SETFAM_1:def 7;
0 in {0} by TARSKI:def 1;
then reconsider r = {[0,0]} as Relation of {0} by RELSET_1:8;
take TopRelStr (#{0},r,tau#);
thus thesis by Lm1;
end;
end;
definition
cluster strict complete trivial TopLattice;
existence
proof
consider T being
strict trivial reflexive non empty discrete finite TopRelStr;
take T; thus thesis;
end;
end;
definition
let S be non empty RelStr,
T be upper-bounded non empty reflexive antisymmetric RelStr;
cluster infs-preserving map of S,T;
existence
proof take f = S --> Top T;
let A be Subset of S; assume ex_inf_of A,S;
A1: f = (the carrier of S) --> Top T by BORSUK_1:def 3;
then rng f = {Top T} & f.:A c= rng f by FUNCOP_1:14,RELAT_1:144;
then A2: f.:A = {} or f.:A = {Top T} by ZFMISC_1:39;
hence ex_inf_of f.:A,T by YELLOW_0:38,43;
thus inf (f.:A) = Top
T by A2,YELLOW_0:39,def 12 .= f.inf A by A1,FUNCOP_1:13;
end;
end;
definition
let S be non empty RelStr,
T be lower-bounded non empty reflexive antisymmetric RelStr;
cluster sups-preserving map of S,T;
existence
proof take f = S --> Bottom T;
let A be Subset of S; assume ex_sup_of A,S;
A1: f = (the carrier of S) --> Bottom T by BORSUK_1:def 3;
then rng f = {Bottom T} & f.:A c= rng f by FUNCOP_1:14,RELAT_1:144;
then A2: f.:A = {} or f.:A = {Bottom T} by ZFMISC_1:39;
hence ex_sup_of f.:A,T by YELLOW_0:38,42;
thus sup (f.:A) = Bottom
T by A2,YELLOW_0:39,def 11 .= f.sup A by A1,FUNCOP_1:13;
end;
end;
definition
let R,S be 1-sorted;
assume
A1: the carrier of S c= the carrier of R;
dom id the carrier of S = the carrier of S &
rng id the carrier of S = the carrier of S by RELAT_1:71;
then A2: id the carrier of S is Function of the carrier of S, the carrier of R
by A1,FUNCT_2:4;
func incl(S,R) -> map of S,R equals:
Def1:
id the carrier of S;
coherence by A2;
end;
definition
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:59;
the carrier of S c= the carrier of R by YELLOW_0:def 13;
then incl(S,R) = id the carrier of S by Def1;
then incl(S,R).x = a & incl(S,R).y = b by FUNCT_1:35;
hence thesis by YELLOW_0:60;
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:
Def2: (incl(subrelstr X, R))*((subrelstr X)+id);
coherence;
func X opp+id -> strict non empty NetStr over R equals:
Def3: (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;
X+id = (incl(subrelstr X, R))*((subrelstr X)+id) by Def2;
then A1: the RelStr of X+id = the RelStr of (subrelstr X)+id &
the mapping of X+id = incl(subrelstr X, R)*the mapping of (subrelstr X)+id
by WAYBEL_9:def 8;
A2: the carrier of subrelstr X = X by YELLOW_0:def 15;
hence
A3: the carrier of X+id = X by A1,WAYBEL_9:def 5;
A4: 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,A2,A4,YELLOW_0:def 13;
S is full
proof
thus the InternalRel of S = (the InternalRel of R)|_2 the carrier of S
by A1,A4,YELLOW_0:def 14;
end;
hence X+id is full SubRelStr of R;
let x be Element of X+id;
id subrelstr X = id X by A2,GRCAT_1:def 11;
then the mapping of (subrelstr X)+id = id X & dom id X = X &
incl(subrelstr X, R) = id X by A2,Def1,RELAT_1:71,WAYBEL_9:def 5;
then the mapping of X+id = id X by A1,FUNCT_1:42;
hence X+id.x = (id X).x by WAYBEL_0:def 8 .= x by A3,FUNCT_1:35;
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;
X opp+id = (incl(subrelstr X, R))*((subrelstr X)opp+id) by Def3;
then A1: the RelStr of X opp+id = the RelStr of (subrelstr X)opp+id &
the mapping of X opp+id
= incl(subrelstr X, R)*the mapping of (subrelstr X) opp+id
by WAYBEL_9:def 8;
A2: the carrier of subrelstr X = X by YELLOW_0:def 15;
A3: the carrier of (subrelstr X) opp+id = the carrier of subrelstr X &
the RelStr of (subrelstr X) opp+id = (subrelstr X) opp &
the InternalRel of (subrelstr X) opp+id = (the InternalRel of subrelstr X)~
by WAYBEL_9:11,def 6;
thus
the carrier of X opp+id = X by A1,A2,WAYBEL_9:def 6;
A4: 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 A2,YELLOW_0:def 14;
then A5: the InternalRel of (subrelstr X)opp+id = (the InternalRel of R)~|_2 X
by A3,ORDERS_2:95;
then the InternalRel of (subrelstr X)opp+id c= the InternalRel of R opp
by A4,WELLORD1:15;
then reconsider S = X opp+id as SubRelStr of R opp by A1,A2,A3,A4,YELLOW_0:
def 13;
S is full
proof
thus the InternalRel of S
= (the InternalRel of R opp)|_2 the carrier of S by A1,A3,A4,A5,
YELLOW_0:def 15;
end;
hence X opp+id is full SubRelStr of R opp;
let x be Element of X opp+id;
id subrelstr X = id X by A2,GRCAT_1:def 11;
then the mapping of (subrelstr X)opp+id = id X & dom id X = X &
incl(subrelstr X, R) = id X by A2,Def1,RELAT_1:71,WAYBEL_9:def 6;
then the mapping of X opp+id = id X by A1,FUNCT_1:42;
hence X opp+id.x = (id X).x by WAYBEL_0:def 8 .= x by A1,A2,A3,FUNCT_1:35;
end;
definition
let R be non empty reflexive RelStr;
let X be non empty Subset of R;
cluster X +id -> reflexive;
coherence
proof X+id = (incl(subrelstr X, R))*((subrelstr X)+id) by Def2;
hence thesis;
end;
cluster X opp+id -> reflexive;
coherence
proof X opp+id = (incl(subrelstr X, R))*((subrelstr X) opp+id) by Def3;
hence thesis;
end;
end;
definition
let R be non empty transitive RelStr;
let X be non empty Subset of R;
cluster X +id -> transitive;
coherence
proof X+id = (incl(subrelstr X, R))*((subrelstr X)+id) by Def2;
hence thesis;
end;
cluster X opp+id -> transitive;
coherence
proof X opp+id = (incl(subrelstr X, R))*((subrelstr X) opp+id) by Def3;
hence thesis;
end;
end;
definition
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: [#]subrelstr I = the carrier of subrelstr I by PRE_TOPC:12;
A2: the carrier of subrelstr I = I by YELLOW_0:def 15;
assume
A3: x in [#]subrelstr I & y in [#]subrelstr I;
then reconsider a = x, b = y as Element of R by A1,A2;
consider c being Element of R such that
A4: c in I & a <= c & b <= c by A2,A3,WAYBEL_0:def 1;
reconsider z = c as Element of subrelstr I by A2,A4;
take z; thus thesis by A1,A3,A4,YELLOW_0:61;
end;
end;
definition
let R be non empty reflexive RelStr;
let I be directed non empty Subset of R;
cluster I+id -> directed;
coherence
proof I+id = (incl(subrelstr I, R))*((subrelstr I)+id) by Def2;
hence thesis;
end;
end;
definition
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: [#]A = the carrier of A by PRE_TOPC:12;
A2: the carrier of subrelstr I = I by YELLOW_0:def 15;
A3: the carrier of A = the carrier of subrelstr F by WAYBEL_9:def 6;
assume
x in [#]A & y in [#]A;
then reconsider a = x, b = y as Element of R by A1,A2,A3;
A4: the RelStr of A = the RelStr of (subrelstr F) opp by WAYBEL_9:11;
consider c being Element of R such that
A5: c in I & a >= c & b >= c by A2,A3,WAYBEL_0:def 2;
reconsider a1 = x, b1 = y, c1 = c as Element of subrelstr F
by A2,A3,A5;
reconsider z = c as Element of A by A2,A3,A5;
take z;
A6: a1~ = a1 & b1~ = b1 & c1~ = c1 by LATTICE3:def 6;
a1 >= c1 & b1 >= c1 by A5,YELLOW_0:61;
then a1~ <= c1~ & b1~ <= c1~ by LATTICE3:9;
hence thesis by A1,A4,A6,YELLOW_0:1;
end;
end;
definition
let R be non empty reflexive RelStr;
let F be filtered non empty Subset of R;
cluster F opp+id -> directed;
coherence
proof F opp+id = (incl(subrelstr F, R))*((subrelstr F) opp+id) by Def3;
hence thesis;
end;
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 the carrier of T1 = {} by STRUCT_0:def 1;
then the topology of T1 c= {{}} & {} in the topology of T1
by PRE_TOPC:def 1,ZFMISC_1:1;
hence thesis by ZFMISC_1:39;
end;
theorem Th9:
for T being trivial non empty 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 trivial non empty 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;
{} in the topology of T & the carrier of T in the topology of T
by PRE_TOPC:5,def 1;
then A2: {{},the carrier of T} c= the topology of T & bool {x} = {{},{x}}
by ZFMISC_1:30,38;
hence bool the carrier of T c= the topology of T by A1;
let a be Point of T; a = x by REALSET1:def 20;
hence the carrier of T = {a} & the topology of T c= {{},{a}} &
{{},{a}} c= the topology of T by A1,A2;
end;
theorem
for T being trivial non empty TopSpace holds
{the carrier of T} is Basis of T &
{} is prebasis of T & {{}} is prebasis of T
proof let T be trivial non empty TopSpace;
set BB = {the carrier of T};
the carrier of T c= the carrier of T;
then A1: the topology of T = bool the carrier of T &
the carrier of T in bool the carrier of T by Th9;
then BB c= the topology of T by ZFMISC_1:37;
then BB is Subset-Family of T by A1,SETFAM_1:def 7;
then reconsider BB as Subset-Family of T;
consider x being Element of T;
A2: the topology of T = {{}, {x}} & the carrier of T = {x} by Th9;
A3: {} c= bool the carrier of T & {} c= BB & {}
c= the carrier of T by XBOOLE_1:2;
then {} is Subset-Family of T by SETFAM_1:def 7;
then reconsider C = {} as Subset-Family of T;
the topology of T c= UniCl BB
proof let a be set; assume a in the topology of T;
then A4: a = {x} & union {{x}} = {x} & BB c= BB & BB c= bool the carrier of
T or
a = {} by A2,TARSKI:def 2,ZFMISC_1:31;
{{x}} is Subset of bool the carrier of T by ZFMISC_1:37;
then {{x}} is Subset-Family of T by SETFAM_1:def 7;
then {{x}} is Subset-Family of T & C is Subset-Family of T;
hence thesis by A2,A3,A4,CANTOR_1:def 1,ZFMISC_1:2;
end;
hence
A5: {the carrier of T} is Basis of T by A1,CANTOR_1:def 2;
A6: {} c= the topology of T & C c= C & C is finite by XBOOLE_1:2;
BB c= FinMeetCl C
proof let x be set; assume x in BB;
then x = the carrier of T by TARSKI:def 1;
then Intersect C = x by CANTOR_1:def 3;
hence thesis by CANTOR_1:def 4;
end;
hence {} is prebasis of T by A5,A6,CANTOR_1:def 5;
{} c= the carrier of T by XBOOLE_1:2;
then {{}} is Subset of bool the carrier of T by ZFMISC_1:37;
then {{}} is Subset-Family of T by SETFAM_1:def 7;
then reconsider D = {{}} as Subset-Family of T;
A7: D c= the topology of T by A2,ZFMISC_1:12;
BB c= FinMeetCl D
proof let x be set; assume x in BB;
then x = the carrier of T & Intersect C = the carrier of T &
C c= D by CANTOR_1:def 3,TARSKI:def 1,XBOOLE_1:2;
hence thesis by CANTOR_1:def 4;
end;
hence {{}} is prebasis of T by A5,A7,CANTOR_1:def 5;
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 set; assume x in FinMeetCl A;
then consider Y being Subset-Family of X such that
A2: Y c= A & Y is finite & x = Intersect Y by CANTOR_1:def 4;
Y = {} or Y = {Z} by A1,A2,ZFMISC_1:39;
then x = X or x = meet {Z} by A2,CANTOR_1:def 3;
then x = X or x = Z by SETFAM_1:11;
hence thesis by TARSKI:def 2;
end;
reconsider E = {} as Subset of bool X by XBOOLE_1:2;
reconsider E as Subset-Family of X by SETFAM_1:def 7;
hereby let x be set; 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:11;
then x = Intersect E & E c= A or x = Intersect A & A c= A
by A1,CANTOR_1:def 3,XBOOLE_1:2;
hence x in FinMeetCl A by A1,CANTOR_1:def 4;
end;
hereby let x be set; assume x in UniCl A;
then consider Y being Subset-Family of X such that
A3: Y c= A & x = union Y by CANTOR_1:def 1;
Y = {} or Y = {Z} by A1,A3,ZFMISC_1:39;
then x = {} or x = Z by A3,ZFMISC_1:2,31;
hence x in {Z,{}} by TARSKI:def 2;
end;
let x be set; 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,XBOOLE_1:2,ZFMISC_1
:2,31
;
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 set; assume
A2: x in Intersect A;
now let y be set; assume y in B;
then y in A by A1,XBOOLE_0:def 2,def 4;
hence x in y by A2,CANTOR_1:10;
end;
hence x in Intersect B by A2,CANTOR_1:10;
end;
let x be set; 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 2,def 4;
then y in B or y = X by TARSKI:def 1;
hence x in y by A3,CANTOR_1:10;
end;
hence thesis by A3,CANTOR_1:10;
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 {X} c= FinMeetCl B & B c= FinMeetCl B & (A \ {X}) \/ {X} = A \/ {X}
by CANTOR_1:4,XBOOLE_1:39,ZFMISC_1:37;
then A c= B \/ {X} & B \/ {X} c= FinMeetCl B by A1,XBOOLE_1:7,8
;
then A c= FinMeetCl B by XBOOLE_1:1;
then FinMeetCl A c= FinMeetCl FinMeetCl B by CANTOR_1:16;
hence FinMeetCl A c= FinMeetCl B by CANTOR_1:13;
B c= A by A1,XBOOLE_1:7,36;
hence thesis by CANTOR_1:16;
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:37;
reconsider Z = {X} as finite non empty Subset of bool X by A1,ZFMISC_1:37;
reconsider Z as finite non empty Subset-Family of X by SETFAM_1:def 7;
A3: Intersect Z = meet Z by CANTOR_1:def 3 .= X by SETFAM_1:11;
let x be set;
hereby assume x in FinMeetCl A;
then consider Y being Subset-Family of X such that
A4: Y c= A & Y is finite & x = Intersect Y by CANTOR_1:def 4;
per cases; suppose Y = {};
then x = X by A4,CANTOR_1:def 3;
hence ex Y being finite non empty Subset-Family of X st
Y c= A & x = Intersect Y by A2,A3;
suppose Y <> {};
hence ex Y being finite non empty Subset-Family of X st
Y c= A & x = Intersect Y by A4;
end;
thus thesis by CANTOR_1:def 4;
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 set; assume x in UniCl UniCl A;
then consider Y being Subset-Family of X such that
A1: Y c= UniCl A & x = union Y by CANTOR_1:def 1;
set Z = {y where y is Subset of X: y in A & y c= x};
Z c= bool X
proof let a be set; assume a in Z;
then ex y being Subset of X st a = y & y in A & y c= x;
hence thesis;
end;
then reconsider Z as Subset-Family of X by SETFAM_1:def 7;
A2: x = union Z
proof
hereby let a be set; assume a in x;
then consider s being set such that
A3: a in s & s in Y by A1,TARSKI:def 4;
consider t being Subset-Family of X such that
A4: t c= A & s = union t by A1,A3,CANTOR_1:def 1;
consider u being set such that
A5: a in u & u in t by A3,A4,TARSKI:def 4;
reconsider u as Subset of X by A5;
u c= s & s c= x by A1,A3,A4,A5,ZFMISC_1:92;
then u c= x by XBOOLE_1:1;
then u in Z by A4,A5;
hence a in union Z by A5,TARSKI:def 4;
end;
let a be set; assume a in union Z;
then consider u being set such that
A6: a in u & u in Z by TARSKI:def 4;
ex y being Subset of X st u = y & y in A & y c= x by A6;
hence thesis by A6;
end;
Z c= A
proof let a be set; assume a in Z;
then ex y being Subset of X st a = y & y in A & y c= x;
hence thesis;
end;
hence x in UniCl A by A2,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 set; assume x in UniCl A;
then consider B being Subset-Family of X such that
A1: B c= A & x = union B by CANTOR_1:def 1;
B = {} by A1,XBOOLE_1:3;
hence x in {{}} by A1,TARSKI:def 1,ZFMISC_1:2;
end;
consider B being empty Subset-Family of X;
let x be set; assume x in {{}};
then x = {} & B c= A & union B = {} by TARSKI:def 1,ZFMISC_1:2;
hence thesis by 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 set; assume x in FinMeetCl A;
then consider B being Subset-Family of X such that
A1: B c= A & B is finite & x = Intersect B by CANTOR_1:def 4;
B = {} by A1,XBOOLE_1:3;
then x = X by A1,CANTOR_1:def 3;
hence x in {X} by TARSKI:def 1;
end;
consider B being empty Subset-Family of X;
let x be set; assume x in {X};
then x = X & B c= A & Intersect B = X
by CANTOR_1:def 3,TARSKI:def 1;
hence thesis by CANTOR_1:def 4;
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 set; assume a in UniCl A;
then consider y being Subset-Family of X such that
A2: y c= A & a = union y by CANTOR_1:def 1;
y = {} or y = {{}} or y = {X} or y = {{},X} by A1,A2,ZFMISC_1:42;
then a = {} or a = X or a = {} \/ X & {} \/ X = X by A2,ZFMISC_1:2,31,93;
hence a in A by A1,TARSKI:def 2;
end;
thus A c= UniCl A by CANTOR_1:1;
hereby let a be set; assume a in FinMeetCl A;
then consider y being Subset-Family of X such that
A3: y c= A & y is finite & a = Intersect y by CANTOR_1:def 4;
y = {} or y = {{}} or y = {X} or y = {{},X} by A1,A3,ZFMISC_1:42;
then a = X or a = meet {{}} or a = meet {X} or a = meet {{},X}
by A3,CANTOR_1:def 3;
then a = X or a = {} or a = {} /\ X & {} /\ X = {} by SETFAM_1:11,12;
hence a in A by A1,TARSKI:def 2;
end;
thus A c= FinMeetCl A 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 set; assume x in UniCl A;
then consider y being Subset-Family of X such that
A3: y c= A & x = union y by CANTOR_1:def 1;
A4: y c= B by A2,A3,XBOOLE_1:1;
then y is Subset of bool Y by XBOOLE_1:1;
then y is Subset-Family of Y by SETFAM_1:def 7;
then ex y being Subset-Family of Y st y c= B & x = union y by A3,A4;
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 & X c= Y 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 & X in A & X c= Y;
thus FinMeetCl B c= {Y} \/ FinMeetCl A
proof let x be set; assume x in FinMeetCl B;
then consider y being Subset-Family of Y such that
A2: y c= B & y is finite & x = Intersect y by CANTOR_1:def 4;
reconsider z = y as Subset of bool X by A1,A2,XBOOLE_1:1;
reconsider z as Subset-Family of X by SETFAM_1:def 7;
per cases;
suppose y = {}; then x = Y by A2,CANTOR_1:def 3;
then x in {Y} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 2;
suppose y <> {};
then Intersect y = meet y & Intersect z = meet y by CANTOR_1:def 3;
then x in FinMeetCl A by A1,A2,CANTOR_1:def 4;
hence thesis by XBOOLE_0:def 2;
end;
let x be set; assume
A3: x in {Y} \/ FinMeetCl A;
consider E being empty Subset-Family of Y;
per cases by A3,XBOOLE_0:def 2;
suppose x in {Y};
then x = Y & Intersect E = Y & E c= B by CANTOR_1:def 3,TARSKI:def 1,
XBOOLE_1:2;
hence thesis by CANTOR_1:def 4;
suppose x in FinMeetCl A;
then consider y being non empty finite Subset-Family of X such that
A4: y c= A & x = Intersect y by A1,Th14;
reconsider z = y as Subset of bool Y by A1,A4,XBOOLE_1:1;
reconsider z as Subset-Family of Y by SETFAM_1:def 7;
x = meet z by A4,CANTOR_1:def 3 .= Intersect z by CANTOR_1:def 3;
hence thesis by A1,A4,CANTOR_1:def 4;
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
A = {};
then FinMeetCl A = {X} & UniCl A = {{}} by Th16,Th17;
then FinMeetCl UniCl A = {{},X} & UniCl FinMeetCl A = {X,{}} by Th11;
hence thesis by Th18;
suppose A <> {}; then reconsider A as non empty Subset-Family of X;
A1: UniCl FinMeetCl UniCl A c= UniCl UniCl FinMeetCl A
proof let x be set; assume x in UniCl FinMeetCl UniCl A;
then consider Y being Subset-Family of X such that
A2: Y c= FinMeetCl UniCl A & x = union Y by CANTOR_1:def 1;
Y c= UniCl FinMeetCl A
proof let y be set; assume y in Y;
then consider Z being Subset-Family of X such that
A3: Z c= UniCl A & Z is finite & y = Intersect Z by A2,CANTOR_1:def 4;
per cases;
suppose Z = {}; then y = X by A3,CANTOR_1:def 3;
then y in
FinMeetCl A & FinMeetCl A c= UniCl FinMeetCl A by CANTOR_1:1,8;
hence thesis;
suppose
A4: Z <> {};
then A5: y = meet Z by A3,CANTOR_1:def 3;
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};
A6: G c= FinMeetCl A
proof let a be set; assume a in G;
then consider f being Element of Funcs(Z,A) such that
A7: a = meet rng f & for z being set st z in Z holds f.z c= z;
Funcs(Z,A) is FUNCTION_DOMAIN of Z,A by FRAENKEL:11;
then f is Function of Z,A by FRAENKEL:def 2;
then A8: dom f = Z & rng f c= A by FUNCT_2:def 1,RELSET_1:12;
then reconsider B = rng f as Subset of bool X by XBOOLE_1:1;
reconsider B as Subset-Family of X by SETFAM_1:def 7;
B <> {} by A4,A8,RELAT_1:65;
then Intersect B = a & B is finite
by A3,A7,A8,CANTOR_1:def 3,FINSET_1:26;
hence thesis by A8,CANTOR_1:def 4;
end;
then reconsider G as Subset of bool X by XBOOLE_1:1;
reconsider G as Subset-Family of X by SETFAM_1:def 7;
union G = y
proof
hereby let a be set; assume a in union G;
then consider b being set such that
A9: a in b & b in G by TARSKI:def 4;
consider f being Element of Funcs(Z,A) such that
A10: b = meet rng f & for z being set st z in Z holds f.z c= z by
A9;
Funcs(Z,A) is FUNCTION_DOMAIN of Z,A by FRAENKEL:11;
then f is Function of Z,A by FRAENKEL:def 2;
then A11: dom f = Z & rng f c= A by FUNCT_2:def 1,RELSET_1:12;
then reconsider B = rng f as Subset of bool X by XBOOLE_1:1;
reconsider B as Subset-Family of X by SETFAM_1:def 7;
b c= y
proof let c be set; assume
A12: c in b;
now let d be set; assume
A13: d in Z;
then f.d in B by A11,FUNCT_1:def 5;
then b c= f.d by A10,SETFAM_1:4;
then f.d c= d & c in f.d by A10,A12,A13;
hence c in d;
end;
hence c in y by A4,A5,SETFAM_1:def 1;
end;
hence a in y by A9;
end;
let a be set; assume
A14: a in y;
defpred P[set,set] means a in $2 & $2 c= $1;
A15: now let z be set; assume A16: z in Z;
then A17: a in z & z in UniCl A by A3,A5,A14,SETFAM_1:def 1;
consider C being Subset-Family of X such that
A18: C c= A & z = union C by A3,A16,CANTOR_1:def 1;
consider w being set such that
A19: a in w & w in C by A17,A18,TARSKI:def 4;
take w; thus w in A by A18,A19;
thus P[z, w] by A18,A19,ZFMISC_1:92;
end;
consider f being Function such that
A20: dom f = Z & rng f c= A and
A21: for z being set st z in Z holds P[z, f.z]
from NonUniqBoundFuncEx(A15);
reconsider f as Element of Funcs(Z,A) by A20,FUNCT_2:def 2;
for z being set st z in Z holds f.z c= z by A21;
then A22: meet rng f in G;
now thus rng f <> {} by A4,A20,RELAT_1:65;
let y be set; assume y in rng f;
then ex z being set st z in Z & y = f.z by A20,FUNCT_1:def 5;
hence a in y by A21;
end;
then a in meet rng f by SETFAM_1:def 1;
hence thesis by A22,TARSKI:def 4;
end;
hence thesis by A6,CANTOR_1:def 1;
end;
hence thesis by A2,CANTOR_1:def 1;
end;
A c= UniCl A by CANTOR_1:1;
then FinMeetCl A c= FinMeetCl UniCl A by CANTOR_1:16;
then UniCl FinMeetCl A c= UniCl FinMeetCl UniCl A &
UniCl UniCl FinMeetCl A = UniCl FinMeetCl A by Th15,CANTOR_1:9;
hence thesis by A1,XBOOLE_0:def 10;
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
proof assume the topology of T = UniCl K;
hence K c= the topology of T & the topology of T c= UniCl K
by CANTOR_1:1;
end;
assume K c= the topology of T;
then A1: UniCl K c= UniCl the topology of T by CANTOR_1:9;
assume the topology of T c= UniCl K;
hence the topology of T c= UniCl K & UniCl K c= the topology of T
by A1,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: now assume T is empty;
then the topology of T = {{}} & the carrier of T = {} by Th8,STRUCT_0:def
1;
hence the topology of T = bool the carrier of T by ZFMISC_1:1;
end;
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 CANTOR_1:def 5;
then FinMeetCl BB c= FinMeetCl the topology of T by CANTOR_1:16;
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 5;
the topology of T c= UniCl A &
UniCl A c= UniCl FinMeetCl BB by A4,CANTOR_1:9,def 2;
then the topology of T c= UniCl FinMeetCl BB by XBOOLE_1:1;
hence FinMeetCl BB is Basis of T by A3,CANTOR_1:def 2;
end;
assume
A5: FinMeetCl BB is Basis of T;
then BB c= FinMeetCl BB & FinMeetCl BB c= the topology of T
by CANTOR_1:4,def 2;
then BB c= the topology of T by XBOOLE_1:1;
hence BB is prebasis of T by A5,CANTOR_1:def 5;
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
A1: the carrier of T1 = the carrier of T2 & B is Basis of T2;
then reconsider C = B as Basis of T2;
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
A1: the carrier of T1 = the carrier of T2 & P is prebasis of T2;
then reconsider C = P as prebasis of T2;
FinMeetCl P is Basis of T1 & FinMeetCl C is Basis of T2 by Th23;
hence thesis by A1,Th25;
end;
theorem
for T being TopSpace, K being Basis of T holds K is open & K is prebasis of
T
proof let T be TopSpace, K be Basis of T;
K c= the topology of T by CANTOR_1:def 2;
hence for P be Subset of T st P in K holds
P is open by PRE_TOPC:def 5;
thus K c= the topology of T by CANTOR_1:def 2;
take K; thus K c= FinMeetCl K by CANTOR_1:4;
end;
theorem
for T being TopSpace, K being prebasis of T holds K is open
proof let T be TopSpace, K be prebasis of T;
let P be Subset of T;
A1: K c= the topology of T by CANTOR_1:def 5;
assume P in K;
hence P in the topology of T by A1;
end;
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};
the carrier of T in the topology of T by PRE_TOPC:def 1;
then A1: B c= the topology of T & {the carrier of T} c= the topology of T
by CANTOR_1:def 5,ZFMISC_1:37;
then C c= the topology of T by XBOOLE_1:8;
then C is Subset of bool the carrier of T by XBOOLE_1:1;
then C is Subset-Family of T by SETFAM_1:def 7;
then reconsider C as Subset-Family of T;
C is prebasis of T
proof thus C c= the topology of T by A1,XBOOLE_1:8;
B c= C by XBOOLE_1:7;
then FinMeetCl B c= FinMeetCl C & FinMeetCl B is Basis of T
by Th23,CANTOR_1:16;
hence thesis;
end;
hence thesis;
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};
the carrier of T in the topology of T by PRE_TOPC:def 1;
then A1: B c= the topology of T & {the carrier of T} c= the topology of T
by CANTOR_1:def 2,ZFMISC_1:37;
then C c= the topology of T by XBOOLE_1:8;
then C is Subset of bool the carrier of T by XBOOLE_1:1;
then C is Subset-Family of T by SETFAM_1:def 7;
then reconsider C as Subset-Family of T;
C is Basis of T
proof thus C c= the topology of T by A1,XBOOLE_1:8;
B c= C by XBOOLE_1:7;
then UniCl B c= UniCl C & the topology of T c= UniCl B by CANTOR_1:9,def
2;
hence thesis by XBOOLE_1:1;
end;
hence thesis;
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:
18;
let p be Point of T; assume p in A;
then consider Z being set such that
A2: p in Z & 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 A2;
hence ex a being Subset of T st a in K & p in a & a c= A by A2;
end;
assume
A3: 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 set; 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 by SETFAM_1:def 7;
reconsider F as Subset-Family of T;
A4: F is open
proof let x be Subset of T; assume x in F;
then ex G being Subset of T st x = G & G in K & G c= A;
then x in K & K c= the topology of T by CANTOR_1:def 2;
hence x in the topology of T;
end;
A = union F
proof
hereby let x be set; assume
A5: x in A;
then reconsider p = x as Point of T;
consider a being Subset of T such that
A6: a in K & p in a & a c= A by A3,A5;
a in F by A6;
hence x in union F by A6,TARSKI:def 4;
end;
F c= bool A
proof let x be set; 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:95;
hence thesis by ZFMISC_1:99;
end;
hence thesis by A4,TOPS_2:26;
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;
thus B c= the topology of T by A1;
let x be set; assume
A3: 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 set; 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 by SETFAM_1:def 7;
reconsider Y as Subset-Family of T;
A4: Y c= B
proof let y be set; assume y in Y;
then ex V being Subset of T st y = V & V in B & V c= A;
hence thesis;
end;
x = union Y
proof
hereby let p be set; assume
A5: p in x; then p in A; then reconsider q = p as Point of T;
A is open by A3,PRE_TOPC:def 5;
then consider a being Subset of T such that
A6: a in B & q in a & a c= A by A2,A5;
a in Y by A6;
hence p in union Y by A6,TARSKI:def 4;
end;
let p be set; assume p in union Y;
then consider a being set such that
A7: p in a & a in Y by TARSKI:def 4;
ex V being Subset of T st a = V & V in B & V c= A by A7;
hence thesis by A7;
end;
hence thesis by A4,CANTOR_1:def 1;
end;
theorem Th33:
for S being TopSpace, T being non empty TopSpace, K being Basis of T
for f being map 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 map of S,T;
A1: BB c= the topology of T by CANTOR_1:def 2;
hereby assume
A2: f is continuous;
let A be Subset of T; assume A in BB;
then A is open by A1,PRE_TOPC:def 5;
then A` is closed by TOPS_1:30;
hence f"A` is closed by A2,PRE_TOPC:def 12;
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:29;
then A4: A` = union {G where G is Subset of T: G in BB & G c= A`} by YELLOW_8:
18;
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 set; 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 by SETFAM_1:def 7;
reconsider F as Subset-Family of S;
F c= the topology of S
proof let a be set; assume a in F;
then consider G being Subset of T such that
A5: a = f"G & G in BB & G c= A`;
f"G` is closed & (f"G)` = f"G` by A3,A5,Th2;
then f"G is open by TOPS_1:30;
hence thesis by A5,PRE_TOPC:def 5;
end; then
A6: 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,A6,PRE_TOPC:def 5;
then (f"A)` is open by Th2;
hence f"A is closed by TOPS_1:29;
end;
theorem
for S being TopSpace,T being non empty TopSpace, K being Basis of T
for f being map 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 map 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:30;
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:30;
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 map 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 map of S,T;
A1: BB c= the topology of T by CANTOR_1:def 5;
hereby assume
A2: f is continuous;
let A be Subset of T; assume A in BB;
then A is open by A1,PRE_TOPC:def 5;
then A` is closed by TOPS_1:30;
hence f"A` is closed by A2,PRE_TOPC:def 12;
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 & Y is finite & A = Intersect Y by CANTOR_1:def 4;
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`;
A5: f"A` = f"union CY by A4,YELLOW_8:16
.= 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 set; 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 by SETFAM_1:def 7;
reconsider X as Subset-Family of S;
A6: 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 a is closed by A3,A4;
end;
A7: Y is finite by A4;
deffunc F(Subset of T) = f"$1`;
A8: {F(y) where y is Subset of T: y in Y} is finite
from FraenkelFin(A7);
X is finite by A8;
hence f"A` is closed by A5,A6,TOPS_2:28;
end;
hence thesis by Th33;
end;
theorem
for S being TopSpace,T being non empty TopSpace, K being prebasis of T
for f being map 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 map 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:30;
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:30;
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:20;
x in Int G by CONNSP_2:def 1;
then consider Z being set such that
A3: x in Z & Z in {A where A is Subset of T: A in BB & A c= G}
by A2,TARSKI:def 4;
consider A being Subset of T such that
A4: Z = A & A in BB & A c= G by A3;
A meets X by A1,A3,A4;
hence G meets X by A4,XBOOLE_1:63;
end;
hence x in Cl X by YELLOW_6:6;
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 BB' = FinMeetCl BB as Basis of T by Th23;
now let A be Subset of T; assume A in BB';
then consider Y being Subset-Family of T such that
A2: Y c= BB & Y is finite & A = Intersect Y by CANTOR_1:def 4;
reconsider Y as finite Subset-Family of T by A2;
assume x in A;
then Intersect Y meets X by A1,A2;
hence A meets X by 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: the carrier of N = [#]N & [#]N is directed by PRE_TOPC:12,WAYBEL_0:def 6;
A4: the mapping of N = netmap(N,T) by WAYBEL_0:def 7;
now let Z be finite Subset-Family of T; assume
A5: Z c= BB & x in Intersect Z;
defpred P[set,set] means
for i,j being Element of N st $2 = i & i <= j holds N.j in $1;
A6: now let a be set; assume
A7: a in Z;
then reconsider A = a as Subset of T;
A in BB & x in A by A5,A7,CANTOR_1:10;
then N is_eventually_in A by A1;
then consider i being Element of N such that
A8: for j being Element of N st i <= j holds N.j in A by WAYBEL_0:def 11;
reconsider b = i as set;
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 set st a in Z holds P[a, f.a]
from NonUniqBoundFuncEx(A6);
consider k being Element of N;
per cases by A9,RELAT_1:65;
suppose Z = {};
then A10: Intersect Z = the carrier of T by CANTOR_1:def 3;
N.k = netmap(N,T).k & the carrier of T <> {} by A4,WAYBEL_0:def 8;
then N.k in rng netmap(N,T) by FUNCT_2:6;
hence Intersect Z meets S by A2,A10,XBOOLE_0:3;
suppose rng f <> {};
then reconsider Y = rng f as finite non empty Subset of N
by A9,FINSET_1:26;
consider i being Element of N such that
A11: i in the carrier of N & 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 5;
then reconsider j = f.y as Element of N;
j <= i by A11,A13,LATTICE3:def 9;
hence N.i in y by A9,A12;
end;
then A14: N.i in Intersect Z by CANTOR_1:10;
N.i = netmap(N,T).i & the carrier of T <> {} by A4,WAYBEL_0:def 8;
then N.i in rng netmap(N,T) by FUNCT_2:6;
hence Intersect Z meets S by A2,A14,XBOOLE_0:3;
end;
hence x in Cl S 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 5;
BB c= bool the carrier of T
proof let x be set; 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 by SETFAM_1:def 7;
reconsider BB as Subset-Family of T;
A2: B1 c= the topology of T1 & B2 c= the topology of T2 by CANTOR_1:def 2;
BB is Basis of T
proof
hereby let x be set; assume x in BB;
then consider a being Subset of T1, b being Subset of T2 such that
A3: x = [:a,b:] & a in B1 & b in B2;
a is open & b is open by A2,A3,PRE_TOPC:def 5;
then [:a,b:] is open by BORSUK_1:46;
hence x in the topology of T by A3,PRE_TOPC:def 5;
end;
let x be set; assume
A4: x in the topology of T;
then reconsider X = x as Subset of T;
X is open by A4,PRE_TOPC:def 5;
then A5: X = union Base-Appr X by BORSUK_1:54;
set Y = BB /\ Base-Appr X;
A6: Y c= BB & Y c= Base-Appr X by XBOOLE_1:17;
reconsider Y as Subset-Family of T;
union Y = X
proof thus union Y c= X by A5,A6,ZFMISC_1:95;
let z be set; assume
A7: z in X;
then reconsider p = z as Point of T;
consider z1,z2 being set such that
A8: z1 in the carrier of T1 & z2 in the carrier of T2 & p = [z1,z2]
by A1,ZFMISC_1:def 2;
reconsider z1 as Point of T1 by A8;
reconsider z2 as Point of T2 by A8;
consider Z being set such that
A9: z in Z & Z in Base-Appr X by A5,A7,TARSKI:def 4;
A10: 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 6;
then consider a being Subset of T1,
b being Subset of T2 such that
A11: Z = [:a,b:] & [:a,b:] c= X & a is open & b is open by A9;
A12: z1 in a & z2 in b by A8,A9,A11,ZFMISC_1:106;
then consider a' being Subset of T1 such that
A13: a' in B1 & z1 in a' & a' c= a by A11,Th31;
consider b' being Subset of T2 such that
A14: b' in B2 & z2 in b' & b' c= b by A11,A12,Th31;
[:a',b':] c= [:a,b:] by A13,A14,ZFMISC_1:119;
then [:a',b':] c= X & a' is open & b' is open
by A2,A11,A13,A14,PRE_TOPC:def 5,XBOOLE_1:1;
then [:a',b':] in Base-Appr X & [:a',b':] in BB by A10,A13,A14;
then p in [:a',b':] & [:a',b':] in
Y by A8,A13,A14,XBOOLE_0:def 3,ZFMISC_1:106;
hence thesis by TARSKI:def 4;
end;
hence x in UniCl BB by A6,CANTOR_1:def 1;
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 & cT2 in the topology of T2 by PRE_TOPC:def 1;
A2: B1 c= the topology of T1 & B2 c= the topology of T2 by CANTOR_1:def 5;
C1 c= bool the carrier of T
proof let x be set; 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 by SETFAM_1:def 7;
reconsider C1 as Subset-Family of T;
C2 c= bool the carrier of T
proof let x be set; 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 by SETFAM_1:def 7;
reconsider C2 as Subset-Family of T;
reconsider C = C2 \/ C1 as Subset-Family of T;
C is prebasis of T
proof
hereby let x be set; assume x in C;
then x in C1 or x in C2 by XBOOLE_0:def 2;
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
A3: x = [:a,b:] & a in the topology of T1 & b in
the topology of T2 by A1,A2
;
a is open & b is open by A3,PRE_TOPC:def 5;
then [:a,b:] is open by BORSUK_1:46;
hence x in the topology of T by A3,PRE_TOPC:def 5;
end;
take D; let d be set; assume d in D;
then consider a being Subset of T1, b being Subset of T2 such that
A4: d = [:a,b:] & a in D1 & b in D2;
consider aY being Subset-Family of T1 such that
A5: aY c= B1 and
A6: aY is finite and
A7: a = Intersect aY by A4,CANTOR_1:def 4;
consider bY being Subset-Family of T2 such that
A8: bY c= B2 and
A9: bY is finite and
A10: b = Intersect bY by A4,CANTOR_1:def 4;
deffunc F(Subset of T1) = [:$1, cT2:];
A11: {F(s) where s is Subset of T1: s in aY} is finite
from FraenkelFin(A6);
deffunc G(Subset of T2) = [:cT1, $1:];
A12: {G(s) where s is Subset of T2: s in bY} is finite
from FraenkelFin(A9);
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};
A13: Y1 c= C
proof let x be set; assume x in Y1;
then consider s being Subset of T1 such that
A14: x = [:s, cT2:] & s in aY;
s in B1 & s is Subset of T1 by A5,A14;
then x in C1 by A14;
hence thesis by XBOOLE_0:def 2;
end;
A15: Y2 c= C
proof let x be set; assume x in Y2;
then consider s being Subset of T2 such that
A16: x = [:cT1, s:] & s in bY;
s in B2 & s is Subset of T2 by A8,A16;
then x in C2 by A16;
hence thesis by XBOOLE_0:def 2;
end;
set Y = Y1 \/ Y2;
A17: Y c= C by A13,A15,XBOOLE_1:8;
then Y is Subset of bool the carrier of T by XBOOLE_1:1;
then Y is Subset-Family of T by SETFAM_1:def 7;
then reconsider Y as Subset-Family of T;
A18: Y is finite by A11,A12,FINSET_1:14;
Intersect Y = d
proof
hereby let p be set; assume
A19: p in Intersect Y;
then consider p1 being Point of T1, p2 being Point of T2 such that
A20: p = [p1,p2] by BORSUK_1:50;
now let z be set; assume
A21: z in aY;
then reconsider z' = z as Subset of T1;
[:z', cT2:] in Y1 by A21;
then [:z', cT2:] in Y by XBOOLE_0:def 2;
then p in [:z', cT2:] by A19,CANTOR_1:10;
hence p1 in z by A20,ZFMISC_1:106;
end;
then A22: p1 in a by A7,CANTOR_1:10;
now let z be set; assume
A23: z in bY;
then reconsider z' = z as Subset of T2;
[:cT1, z':] in Y2 by A23;
then [:cT1, z':] in Y by XBOOLE_0:def 2;
then p in [:cT1, z':] by A19,CANTOR_1:10;
hence p2 in z by A20,ZFMISC_1:106;
end;
then p2 in b by A10,CANTOR_1:10;
hence p in d by A4,A20,A22,ZFMISC_1:106;
end;
let p be set; assume p in d;
then consider p1,p2 being set such that
A24: p1 in a & p2 in b & [p1,p2] = p by A4,ZFMISC_1:def 2;
reconsider p1 as Point of T1 by A24;
reconsider p2 as Point of T2 by A24;
now let z be set; assume
A25: z in Y;
per cases by A25,XBOOLE_0:def 2;
suppose z in Y1;
then consider s being Subset of T1 such that
A26: z = [:s, cT2:] & s in aY;
p1 in s by A7,A24,A26,CANTOR_1:10;
hence [p1,p2] in z by A26,ZFMISC_1:106;
suppose z in Y2;
then consider s being Subset of T2 such that
A27: z = [:cT1, s:] & s in bY;
p2 in s by A10,A24,A27,CANTOR_1:10;
hence [p1,p2] in z by A27,ZFMISC_1:106;
end;
hence p in Intersect Y by A24,CANTOR_1:10;
end;
hence d in FinMeetCl C by A17,A18,CANTOR_1:def 4;
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 set; assume
A2: x in Intersect A;
then consider x1,x2 being set such that
A3: x1 in X1 & x2 in X2 & [x1,x2] = x by ZFMISC_1:def 2;
consider a1 being Element of A1, a2 being 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,CANTOR_1:10;
hence x1 in a by A3,ZFMISC_1:106;
end;
then A4: x1 in Intersect A1 by A3,CANTOR_1:10;
now let a be set; assume a in A2;
then [:a1,a:] in A by A1;
then x in [:a1,a:] by A2,CANTOR_1:10;
hence x2 in a by A3,ZFMISC_1:106;
end;
then x2 in Intersect A2 by A3,CANTOR_1:10;
hence x in [:Intersect A1, Intersect A2:] by A3,A4,ZFMISC_1:106;
end;
let x be set; assume
A5: x in [:Intersect A1, Intersect A2:];
then consider x1,x2 being set such that
A6: x1 in Intersect A1 & x2 in Intersect A2 & [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
A7: c = [:a,b:] & a in A1 & b in A2 by A1;
x1 in a & x2 in b by A6,A7,CANTOR_1:10;
hence x in c by A6,A7,ZFMISC_1:106;
end;
hence x in Intersect A by A5,CANTOR_1:10;
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 & 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;
A2: FinMeetCl BB is Basis of T by Th23;
CC c= bool the carrier of [:T1,T2:]
proof let x be set; 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:]
by SETFAM_1:def 7;
reconsider CC as Subset-Family of [:T1,T2:];
CC c= the topology of T
proof let x be set; assume x in CC;
then consider a being Subset of T1, b being Subset of T2 such that
A3: x = [:a,b:] & a in B1 & b in B2;
B1 c= the topology of T1 & B2 c= the topology of T2
by CANTOR_1:def 5;
then a is open & b is open by A3,PRE_TOPC:def 5;
then [:a,b:] is open by BORSUK_1:46;
hence thesis by A3,PRE_TOPC:def 5;
end;
then UniCl CC c= UniCl the topology of T by CANTOR_1:9;
then A4: UniCl CC c= the topology of T by CANTOR_1:6;
BB c= UniCl CC
proof let x be set; assume
A5: x in BB;
per cases by A5,XBOOLE_0:def 2;
suppose x in BB1;
then consider b being Subset of T2 such that
A6: x = [:cT1,b:] & 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 set; 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 by SETFAM_1:def 7;
reconsider Y as Subset-Family of T;
A7: Y c= CC
proof let y be set; assume y in Y;
then ex a being Subset of T1 st y = [:a,b:] & a in B1;
hence thesis by A6;
end;
x = union Y
proof
hereby let z be set; assume z in x;
then consider p1, p2 being set such that
A8: p1 in cT1 & p2 in b & [p1,p2] = z by A6,ZFMISC_1:def 2;
consider a being set such that
A9: p1 in a & a in B1 by A1,A8,TARSKI:def 4;
reconsider a as Subset of T1 by A9;
[:a,b:] in Y & z in [:a,b:] by A8,A9,ZFMISC_1:def 2;
hence z in union Y by TARSKI:def 4;
end;
let z be set; assume z in union Y;
then consider y being set such that
A10: z in y & y in Y by TARSKI:def 4;
ex a being Subset of T1 st y = [:a,b:] & a in B1 by A10;
then y c= x by A6,ZFMISC_1:118;
hence thesis by A10;
end;
hence thesis by A7,CANTOR_1:def 1;
suppose x in BB2;
then consider a being Subset of T1 such that
A11: x = [:a,cT2:] & 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 set; 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 by SETFAM_1:def 7;
reconsider Y as Subset-Family of T;
A12: Y c= CC
proof let y be set; assume y in Y;
then ex b being Subset of T2 st y = [:a,b:] & b in B2;
hence thesis by A11;
end;
x = union Y
proof
hereby let z be set; assume z in x;
then consider p1, p2 being set such that
A13: p1 in a & p2 in cT2 & [p1,p2] = z by A11,ZFMISC_1:def 2;
consider b being set such that
A14: p2 in b & b in B2 by A1,A13,TARSKI:def 4;
reconsider b as Subset of T2 by A14;
[:a,b:] in Y & z in [:a,b:] by A13,A14,ZFMISC_1:def 2;
hence z in union Y by TARSKI:def 4;
end;
let z be set; assume z in union Y;
then consider y being set such that
A15: z in y & y in Y by TARSKI:def 4;
ex b being Subset of T2 st y = [:a,b:] & b in B2 by A15;
then y c= x by A11,ZFMISC_1:118;
hence thesis by A15;
end;
hence thesis by A12,CANTOR_1:def 1;
end;
then FinMeetCl BB c= FinMeetCl UniCl CC by CANTOR_1:16;
then UniCl CC is prebasis of T by A2,A4,CANTOR_1:def 5;
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 consider O being Subset-Family of R;
take TopRelStr(#the carrier of R, the InternalRel of R, O#);
thus thesis;
end;
end;
definition
let R be RelStr;
let T be TopAugmentation of R;
redefine attr T is TopSpace-like; synonym T is correct;
end;
definition
let R be RelStr;
cluster correct discrete strict TopAugmentation of R;
existence
proof reconsider BB = bool the carrier of R
as Subset-Family of R by SETFAM_1:def 7;
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;
definition
let R be non empty RelStr;
cluster -> non empty 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;
definition
let R be reflexive RelStr;
cluster -> reflexive 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_1:def 4;
end;
end;
definition
let R be transitive RelStr;
cluster -> transitive 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_1:def 5;
hence thesis by ORDERS_1:def 5;
end;
end;
definition
let R be antisymmetric RelStr;
cluster -> antisymmetric 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_1:def 6;
hence thesis by ORDERS_1:def 6;
end;
end;
definition
let R be complete (non empty RelStr);
cluster -> complete 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 D meets C 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;
the carrier of IT = the carrier of R &
sigma R = the topology of IT by WAYBEL11:def 12,YELLOW_6:def 27;
then the carrier of T in sigma R &
(for a being Subset-Family of T
st a c= the topology of T
holds union a in the topology of T) &
(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,A2,PRE_TOPC:def 1;
hence thesis by A1,PRE_TOPC:def 1;
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;
A3: sigma R = the topology of ConvergenceSpace Scott-Convergence R
by WAYBEL11:def 12;
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
proof assume S in the topology of T;
then A is inaccessible upper by A1,A3,WAYBEL11:31;
hence thesis by A2,Th47,WAYBEL_0:25;
end;
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,A3,WAYBEL11:31;
end;
hence thesis;
end;
definition
let R be complete LATTICE;
cluster Scott strict correct 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
A2: F = G & F is open;
then F is upper inaccessible by WAYBEL11:def 4;
then G is upper inaccessible by A1,A2,Th47,WAYBEL_0:25;
hence G is open 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 set; 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,PRE_TOPC:def 5;
then C is open by A1,Th50;
hence thesis by PRE_TOPC:def 5;
end;
let x be set; 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,PRE_TOPC:def 5;
then C is open by A1,Th50;
hence thesis by PRE_TOPC:def 5;
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;
consider A being 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;
definition
let R be complete LATTICE;
cluster Scott -> correct 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;
Lm2:
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:69;
now assume
A2: the carrier of S = {};
then the topology of S = {} or the topology of S = {{}} by ZFMISC_1:1,39
;
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:17;
take T;
the topology of S c= FinMeetCl the topology of S &
FinMeetCl the topology of S c= the topology of T
by CANTOR_1:1,4;
then A3: the topology of S c= the topology of T by XBOOLE_1:1;
FinMeetCl the topology of S is Basis of T by Th22;
hence thesis by A3,CANTOR_1:def 5;
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 &
the topology of T is prebasis of R by Lm2;
take R; thus thesis by A1,CANTOR_1:def 5;
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 &
the topology of S is prebasis of T by Lm2;
the topology of S c= the topology of T by A1,CANTOR_1:def 5;
then reconsider T as TopExtension of S by A1,Def5;
take T; thus thesis by A1;
end;
definition
let T be TopStruct;
cluster strict discrete TopExtension of T;
existence
proof
reconsider S = bool the carrier of T as Subset-Family of T
by SETFAM_1:def 7;
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;
c1 c= c1 \/ c2 & c2 c= c1 \/ c2 by XBOOLE_1:7;
then bool c1 c= bool (c1 \/ c2) & bool c2 c= bool (c1 \/
c2) by ZFMISC_1:79;
then t1 c= bool (c1 \/ c2) & t2 c= bool (c1 \/ c2) by XBOOLE_1:1;
then reconsider t = t1 \/ t2 as Subset of bool (c1 \/ c2) by XBOOLE_1:8;
reconsider t as Subset-Family of c1 \/ c2 by SETFAM_1:def 7;
set S = TopStruct(#c1 \/ c2, t#);
consider T being TopExtension of S such that
A1: T is strict & t is prebasis of T by Th53;
reconsider T as strict TopExtension of S by A1;
take T;
thus thesis by A1,Def5;
end;
end;
definition
let T1 be non empty TopStruct, T2 be TopStruct;
cluster -> non empty 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 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, T' being Refinement of T1,T2 holds
the TopStruct of T = the TopStruct of T'
proof let T1, T2 be TopStruct, T,T' be Refinement of T1,T2;
the carrier of T = (the carrier of T1) \/ (the carrier of T2) &
(the topology of T1) \/ (the topology of T2) is prebasis of T &
the carrier of T' = (the carrier of T1) \/ (the carrier of T2) &
(the topology of T1) \/ (the topology of T2) is prebasis of T'
by Def6;
hence thesis by 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;
the carrier of T = (the carrier of T1) \/ (the carrier of T2) &
(the topology of T1) \/ (the topology of T2) is prebasis of T
by Def6;
hence thesis by 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;
(the topology of T1) \/ the topology of T2 is prebasis of T by Def6;
then the topology of T1 c= (the topology of T1) \/ the topology of T2 &
the topology of T2 c= (the topology of T1) \/ the topology of T2 &
(the topology of T1) \/ the topology of T2 c= the topology of T
by CANTOR_1:def 5,XBOOLE_1:7;
then the topology of T1 c= the topology of T &
the topology of T2 c= the topology of T by XBOOLE_1:1;
hence thesis by A1,A2,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 & C1 c= the topology of T1 &
B2 c= the topology of T2 & C2 c= the topology of T2 &
cT1 in the topology of T1 & cT2 in the topology of T2
by CANTOR_1:def 5,PRE_TOPC:def 1;
then A2: B1 \/ B2 c= B & B c= the topology of T & cT1 in B & cT2 in B
by CANTOR_1:def 5,XBOOLE_0:def 2,XBOOLE_1:13;
then A3: B1 \/ B2 c= the topology of T & {cT1,cT2} c= the topology of T &
{cT1,cT2} c= B by XBOOLE_1:1,ZFMISC_1:38;
then B1 \/ B2 \/ {cT1,cT2} c= the topology of T by XBOOLE_1:8;
then B1 \/ B2 \/ {cT1, cT2} is Subset of bool the carrier of T by XBOOLE_1:1;
then B1 \/ B2 \/ {cT1, cT2} is Subset-Family of T by SETFAM_1:
def 7;
then reconsider BB = B1 \/ B2 \/
{cT1, cT2} as Subset-Family of T;
the topology of T1 c= B & the topology of T2 c= B by XBOOLE_1:7;
then C1 c= B & C2 c= B by A1,XBOOLE_1:1;
then reconsider D1 = C1, D2 = C2 as Subset of bool the carrier of T
by XBOOLE_1:1;
reconsider D1, D2 as Subset-Family of T
by SETFAM_1:def 7;
reconsider D1, D2 as Subset-Family of T;
A4: UniCl FinMeetCl BB = UniCl FinMeetCl FinMeetCl BB by CANTOR_1:13
.= UniCl FinMeetCl UniCl FinMeetCl BB by Th21;
FinMeetCl B is Basis of T & FinMeetCl C1 is Basis of T1 &
FinMeetCl C2 is Basis of T2 by Th23;
then A5: UniCl FinMeetCl B = the topology of T &
UniCl FinMeetCl C1 = the topology of T1 &
UniCl FinMeetCl C2 = the topology of T2 by Th22;
B1 c= B1 \/ B2 & B2 c= B1 \/ B2 & {cT1} c= {cT1,cT2} & {cT2} c= {cT1,cT2}
by XBOOLE_1:7,ZFMISC_1:12;
then D1 c= BB & D2 c= BB & BB c= B by A2,A3,XBOOLE_1:8,13;
then A6: FinMeetCl BB c= FinMeetCl B &
FinMeetCl D1 c= FinMeetCl BB & FinMeetCl D2 c= FinMeetCl BB
by CANTOR_1:16;
then A7: UniCl FinMeetCl BB c= the topology of T &
UniCl FinMeetCl D1 c= UniCl FinMeetCl BB &
UniCl FinMeetCl D2 c= UniCl FinMeetCl BB by A5,CANTOR_1:9;
cT1 in {cT1} & cT2 in {cT2} by TARSKI:def 1;
then cT1 in C1 & cT2 in C2 by XBOOLE_0:def 2;
then FinMeetCl D1 = {the carrier of T} \/ FinMeetCl C1 &
FinMeetCl D2 = {the carrier of T} \/ FinMeetCl C2 by Th20;
then FinMeetCl C1 c= FinMeetCl D1 & FinMeetCl C2 c= FinMeetCl D2
by XBOOLE_1:7;
then FinMeetCl C1 c= FinMeetCl BB & FinMeetCl C2 c= FinMeetCl BB
by A6,XBOOLE_1:1;
then the topology of T1 c= UniCl FinMeetCl BB &
the topology of T2 c= UniCl FinMeetCl BB by A5,Th19;
then B c= UniCl FinMeetCl BB by XBOOLE_1:8;
then FinMeetCl B c= FinMeetCl UniCl FinMeetCl BB by CANTOR_1:16;
then the topology of T c= UniCl FinMeetCl BB by A4,A5,CANTOR_1:9;
then the topology of T = UniCl FinMeetCl BB by A7,XBOOLE_0:def 10;
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 & B2 c= the topology of T2 &
B c= the topology of T by CANTOR_1:def 2,def 5;
the topology of T1 c= B & the topology of T2 c= B by XBOOLE_1:7;
then A4: B1 c= B & B2 c= B & B c= FinMeetCl B by A3,CANTOR_1:4,XBOOLE_1:1;
then B1 c= FinMeetCl B & B2 c= FinMeetCl B & B1 \/ B2 c= B
by A3,XBOOLE_1:1,13;
then INTERSECTION(B1,B2) c= FinMeetCl B & B1 \/ B2 c= FinMeetCl B
by A4,CANTOR_1:15,XBOOLE_1:1;
then A5: BB c= FinMeetCl B & FinMeetCl B c= the topology of T
by A1,CANTOR_1:def 2,XBOOLE_1:8;
then A6: BB c= the topology of T by XBOOLE_1:1;
BB is Subset of bool the carrier of T by A5,XBOOLE_1:1;
then BB is Subset-Family of T by SETFAM_1:def 7;
then reconsider BB as Subset-Family of T;
now let A be Subset of T such that
A7: A is open;
let p be Point of T; assume p in A;
then consider a being Subset of T such that
A8: a in FinMeetCl B & p in a & a c= A by A1,A7,Th31;
consider Y being Subset-Family of T such that
A9: Y c= B & Y is finite & a = Intersect Y by A8,CANTOR_1:def 4;
Y /\ the topology of T1 c= the topology of T1 by XBOOLE_1:17;
then Y /\ the topology of T1 is Subset of bool the carrier of T1
by XBOOLE_1:1;
then Y /\ the topology of T1 is Subset-Family of T1
by SETFAM_1:def 7;
then reconsider Y1 = Y /\ the topology of T1 as Subset-Family of T1
;
Y /\ the topology of T2 c= the topology of T2 by XBOOLE_1:17;
then Y /\ the topology of T2 is Subset of bool the carrier of T2
by XBOOLE_1:1;
then Y /\ the topology of T2 is Subset-Family of T2
by SETFAM_1:def 7;
then reconsider Y2 = Y /\ the topology of T2 as Subset-Family of T2
;
A10: Y = B /\ Y by A9,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;
cT1 in the topology of T1 & cT2 in the topology of T2
by PRE_TOPC:def 1;
then A11: cT1 is open & cT2 is open & cT1 in B & cT2 in B
by PRE_TOPC:def 5,XBOOLE_0:def 2;
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 2;
suppose
A12: Y1 \/ Y2 = {} & p in cT1;
then consider b1 being Subset of T1 such that
A13: b1 in B1 & p in b1 & b1 c= cT1 by A11,Th31;
b1 in B1 \/ B2 & b1 in B & a = the carrier of T
by A3,A9,A10,A12,A13,CANTOR_1:def 3,XBOOLE_0:def 2;
then b1 in BB & b1 is Subset of T & b1 c= A
by A8,XBOOLE_0:def 2,XBOOLE_1:1;
hence thesis by A13;
suppose
A14: Y1 \/ Y2 = {} & p in cT2;
then consider b2 being Subset of T2 such that
A15: b2 in B2 & p in b2 & b2 c= cT2 by A11,Th31;
b2 in B1 \/ B2 & b2 in B & a = the carrier of T
by A3,A9,A10,A14,A15,CANTOR_1:def 3,XBOOLE_0:def 2;
then b2 in BB & b2 is Subset of T & b2 c= A
by A8,XBOOLE_0:def 2,XBOOLE_1:1;
hence thesis by A15;
suppose
A16: Y1 = {} & Y2 <> {} & Y <> {};
then A17: a = meet Y2 by A9,A10,CANTOR_1:def 3
.= Intersect Y2 by A16,CANTOR_1:def 3;
Y2 c= Y by A10,XBOOLE_1:7;
then Y2 is finite & Y2 c= the topology of T2
by A9,FINSET_1:13,XBOOLE_1:17;
then a in FinMeetCl the topology of T2 by A17,CANTOR_1:def 4;
then a in the topology of T2 & the topology of T2 = UniCl B2
by Th22,CANTOR_1:5;
then consider Z being Subset-Family of T2 such that
A18: Z c= B2 & a = union Z by CANTOR_1:def 1;
consider z being set such that
A19: p in z & z in Z by A8,A18,TARSKI:def 4;
z in B1 \/ B2 by A18,A19,XBOOLE_0:def 2;
then A20: z in BB & z c= a by A18,A19,XBOOLE_0:def 2,ZFMISC_1:92;
then z is Subset of T & z c= A by A8,XBOOLE_1:1;
hence thesis by A19,A20;
suppose
A21: Y1 <> {} & Y2 = {} & Y <> {};
then A22: a = meet Y1 by A9,A10,CANTOR_1:def 3
.= Intersect Y1 by A21,CANTOR_1:def 3;
Y1 c= Y by A10,XBOOLE_1:7;
then Y1 is finite & Y1 c= the topology of T1
by A9,FINSET_1:13,XBOOLE_1:17;
then a in FinMeetCl the topology of T1 by A22,CANTOR_1:def 4;
then a in the topology of T1 & the topology of T1 = UniCl B1
by Th22,CANTOR_1:5;
then consider Z being Subset-Family of T1 such that
A23: Z c= B1 & a = union Z by CANTOR_1:def 1;
consider z being set such that
A24: p in z & z in Z by A8,A23,TARSKI:def 4;
z in B1 \/ B2 by A23,A24,XBOOLE_0:def 2;
then A25: z in BB & z c= a by A23,A24,XBOOLE_0:def 2,ZFMISC_1:92;
then z is Subset of T & z c= A by A8,XBOOLE_1:1;
hence thesis by A24,A25;
thus thesis;
suppose
A26: Y1 <> {} & Y2 <> {} & Y <> {};
then A27: a = meet Y by A9,CANTOR_1:def 3
.= (meet Y1)/\meet Y2 by A10,A26,SETFAM_1:10
.= (meet Y1)/\Intersect Y2 by A26,CANTOR_1:def 3
.= (Intersect Y1)/\Intersect Y2 by A26,CANTOR_1:def 3;
Y1 c= Y & Y2 c= Y by A10,XBOOLE_1:7;
then Y1 is finite & Y2 is finite &
Y1 c= the topology of T1 & Y2 c= the topology of T2
by A9,FINSET_1:13,XBOOLE_1:17;
then Intersect Y1 in FinMeetCl the topology of T1 &
Intersect Y2 in FinMeetCl the topology of T2 by CANTOR_1:def 4;
then A28: Intersect Y1 in the topology of T1 & the topology of T1 = UniCl
B1 &
Intersect Y2 in the topology of T2 & the topology of T2 = UniCl B2
by Th22,CANTOR_1:5;
then consider Z1 being Subset-Family of T1 such that
A29: Z1 c= B1 & Intersect Y1 = union Z1 by CANTOR_1:def 1;
p in Intersect Y1 by A8,A27,XBOOLE_0:def 3;
then consider z1 being set such that
A30: p in z1 & z1 in Z1 by A29,TARSKI:def 4;
consider Z2 being Subset-Family of T2 such that
A31: Z2 c= B2 & Intersect Y2 = union Z2 by A28,CANTOR_1:def 1;
p in Intersect Y2 by A8,A27,XBOOLE_0:def 3;
then consider z2 being set such that
A32: p in z2 & z2 in Z2 by A31,TARSKI:def 4;
z1 /\ z2 in INTERSECTION(B1,B2) & z1 c= union Z1 & z2 c= union Z2
by A29,A30,A31,A32,SETFAM_1:def 5,ZFMISC_1:92;
then A33: z1 /\ z2 in BB & z1 /\ z2 c= a by A27,A29,A31,XBOOLE_0:def 2,
XBOOLE_1:27;
then z1 /\ z2 is Subset of T & z1 /\ z2 c= A & p in z1 /\ z2
by A8,A30,A32,XBOOLE_0:def 3,XBOOLE_1:1;
hence thesis by A33;
end;
end;
hence thesis by A6,Th32;
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 & the carrier of T2 in B2 by PRE_TOPC:def 1;
A4: B1 c= INTERSECTION(B1,B2)
proof let a be set; assume a in B1;
then a /\ the carrier of T1 in INTERSECTION(B1,B2) &
a c= the carrier of T1 by A1,A3,SETFAM_1:def 5;
hence thesis by XBOOLE_1:28;
end;
B2 c= INTERSECTION(B1,B2)
proof let a be set; assume a in B2;
then a /\ the carrier of T2 in INTERSECTION(B1,B2) &
a c= the carrier of T2 by A1,A3,SETFAM_1:def 5;
hence thesis by XBOOLE_1:28;
end;
then B1 \/ B2 c= INTERSECTION(B1,B2) by A4,XBOOLE_1:8;
hence INTERSECTION(the topology of T1, the topology of T2) is Basis of T
by A2,XBOOLE_1: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;
the RelStr of T1 = the RelStr of L &
the RelStr of T2 = the RelStr of L by Def4;
hence thesis by Th60;
end;