:: Families of Subsets, Subspaces and Mappings in Topological Spaces
:: by Agata Darmochwa{\l}
::
:: Received June 21, 1989
:: Copyright (c) 1990-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 SUBSET_1, PRE_TOPC, SETFAM_1, STRUCT_0, TARSKI, FUNCT_2,
ZFMISC_1, XBOOLE_0, FINSET_1, FUNCT_1, RELAT_1, RCOMP_1, FINSEQ_1, NAT_1,
XXREAL_0, ARYTM_3, CARD_1, ORDINAL2, VALUED_1, RELAT_2, CONNSP_1, TOPS_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0,
RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, XCMPLX_0, NAT_1,
FINSEQ_1, FINSET_1, SETFAM_1, STRUCT_0, PRE_TOPC, CONNSP_1;
constructors SETFAM_1, PARTFUN1, FUNCT_3, XXREAL_0, XREAL_0, NAT_1, MEMBERED,
FINSEQ_1, CONNSP_1, RELSET_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, PRE_TOPC,
XREAL_0, FINSEQ_1, RELAT_1, FUNCT_1, ORDINAL1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, PRE_TOPC;
equalities SUBSET_1, STRUCT_0, RELAT_1;
expansions TARSKI, PRE_TOPC;
theorems TARSKI, FINSET_1, SETFAM_1, FUNCT_1, FUNCT_2, FUNCT_3, NAT_1,
FINSEQ_1, ZFMISC_1, PRE_TOPC, TOPS_1, RELAT_1, XBOOLE_0, XBOOLE_1,
XREAL_1, CONNSP_1;
schemes CLASSES1, NAT_1, SUBSET_1;
begin
reserve x, y for set,
T for TopStruct,
GX for TopSpace,
P, Q, M, N for Subset of T,
F, G for Subset-Family of T,
W, Z for Subset-Family of GX,
A for SubSpace of T;
::
:: A FAMILY OF SETS IN TOPOLOGICAL SPACES
::
theorem
for T being 1-sorted, F being Subset-Family of T holds F c= bool [#]T;
theorem Th2:
for T being 1-sorted, F being Subset-Family of T, X being set st
X c= F holds X is Subset-Family of T
proof
let T be 1-sorted, F be Subset-Family of T, X be set;
assume
A1: X c= F;
X c= bool the carrier of T
proof
let y be object;
assume y in X;
then y in F by A1;
hence thesis;
end;
hence thesis;
end;
theorem
for T being non empty 1-sorted, F being Subset-Family of T st F is
Cover of T holds F <> {}
proof
let T be non empty 1-sorted, F be Subset-Family of T;
set x = the Element of union F;
assume F is Cover of T;
then union F = the carrier of T by SETFAM_1:45;
then ex A being set st x in A & A in F by TARSKI:def 4;
hence thesis;
end;
theorem
for T being 1-sorted, F, G being Subset-Family of T holds union F \
union G c= union(F \ G)
proof
let T be 1-sorted, F, G be Subset-Family of T;
let x be object;
assume
A1: x in union F \ union G;
then x in union F by XBOOLE_0:def 5;
then consider A being set such that
A2: x in A and
A3: A in F by TARSKI:def 4;
not x in union G by A1,XBOOLE_0:def 5;
then not A in G by A2,TARSKI:def 4;
then A in F \ G by A3,XBOOLE_0:def 5;
hence thesis by A2,TARSKI:def 4;
end;
theorem
for T being set, F being Subset-Family of T holds F <> {} iff
COMPLEMENT(F) <> {}
proof
let T be set, F be Subset-Family of T;
thus F <> {} implies COMPLEMENT(F) <> {} by SETFAM_1:32;
assume COMPLEMENT(F) <> {};
then COMPLEMENT(COMPLEMENT(F)) <> {} by SETFAM_1:32;
hence thesis;
end;
theorem Th6:
for T being set, F being Subset-Family of T holds F <> {}
implies meet COMPLEMENT(F) = (union F)`
proof
let T be set, F be Subset-Family of T;
assume F <> {};
then meet COMPLEMENT(F) = [#]T \ union F by SETFAM_1:33;
hence thesis;
end;
theorem Th7:
for T being set, F being Subset-Family of T holds F <> {}
implies union COMPLEMENT(F) = (meet F)`
proof
let T be set, F be Subset-Family of T;
assume F <> {};
then union COMPLEMENT(F) = [#]T \ meet F by SETFAM_1:34
.= T \ meet F;
hence thesis;
end;
Lm1: for T being 1-sorted, F being Subset-Family of T st COMPLEMENT(F) is
finite holds F is finite
proof
let T be 1-sorted, F be Subset-Family of T;
defpred X[object,object] means
for X being Subset of T st X = $1 holds $2 = X`;
A1: for x being object st x in COMPLEMENT(F)
ex y being object st X[x,y]
proof
let x be object;
assume x in COMPLEMENT(F);
then reconsider X=x as Subset of T;
reconsider y=X` as object;
take y;
thus thesis;
end;
consider f being Function such that
A2: dom f = COMPLEMENT(F) and
A3: for x being object st x in COMPLEMENT(F) holds X[x,f.x]
from CLASSES1:sch 1(A1);
for x being object holds x in rng f iff x in F
proof let x be object;
hereby
assume x in rng f;
then consider y being object such that
A4: y in dom f and
A5: x=f.y by FUNCT_1:def 3;
reconsider Y=y as Subset of T by A2,A4;
Y` in F by A2,A4,SETFAM_1:def 7;
hence x in F by A2,A3,A4,A5;
end;
assume
A6: x in F;
then reconsider X=x as Subset of T;
A7: X`` = X;
then X` in COMPLEMENT(F) by A6,SETFAM_1:def 7;
then
A8: f.(X`) = X`` by A3;
X` in dom f by A2,A6,A7,SETFAM_1:def 7;
hence thesis by A8,FUNCT_1:def 3;
end;
then rng f = F by TARSKI:2;
then
A9: f.:(COMPLEMENT(F)) = F by A2,RELAT_1:113;
assume COMPLEMENT(F) is finite;
hence thesis by A9,FINSET_1:5;
end;
theorem Th8:
for T being 1-sorted, F being Subset-Family of T holds
COMPLEMENT(F) is finite iff F is finite
proof
let T be 1-sorted, F be Subset-Family of T;
thus COMPLEMENT(F) is finite implies F is finite by Lm1;
assume F is finite;
then COMPLEMENT COMPLEMENT F is finite;
hence thesis by Lm1;
end;
::
:: CLOSED AND OPEN FAMILIES
::
definition
let T be TopStruct, F be Subset-Family of T;
attr F is open means
for P being Subset of T holds P in F implies P is open;
attr F is closed means
for P being Subset of T holds P in F implies P is closed;
end;
theorem Th9:
F is closed iff COMPLEMENT(F) is open
proof
thus F is closed implies COMPLEMENT(F) is open
proof
assume
A1: F is closed;
let P;
assume P in COMPLEMENT(F);
then P` in F by SETFAM_1:def 7;
then P` is closed by A1;
hence thesis by TOPS_1:4;
end;
assume
A2: COMPLEMENT(F) is open;
let P such that
A3: P in F;
P``=P;
then P` in COMPLEMENT(F) by A3,SETFAM_1:def 7;
then P` is open by A2;
hence thesis;
end;
theorem
F is open iff COMPLEMENT(F) is closed
proof
F = COMPLEMENT COMPLEMENT F;
hence thesis by Th9;
end;
theorem
F c= G & G is open implies F is open;
theorem
F c= G & G is closed implies F is closed;
theorem
F is open & G is open implies F \/ G is open
proof
assume
A1: F is open & G is open;
let P;
assume P in F \/ G;
then P in F or P in G by XBOOLE_0:def 3;
hence thesis by A1;
end;
theorem
F is open implies F /\ G is open
proof
assume
A1: F is open;
let P;
assume P in F /\ G;
then P in F by XBOOLE_0:def 4;
hence thesis by A1;
end;
theorem
F is open implies F \ G is open
proof
assume
A1: F is open;
let P;
assume P in F \ G;
then P in F by XBOOLE_0:def 5;
hence thesis by A1;
end;
theorem
F is closed & G is closed implies F \/ G is closed
proof
assume
A1: F is closed & G is closed;
let P;
assume P in F \/ G;
then P in F or P in G by XBOOLE_0:def 3;
hence thesis by A1;
end;
theorem
F is closed implies F /\ G is closed
proof
assume
A1: F is closed;
let P;
assume P in F /\ G;
then P in F by XBOOLE_0:def 4;
hence thesis by A1;
end;
theorem
F is closed implies F \ G is closed
proof
assume
A1: F is closed;
let P;
assume P in F \ G;
then P in F by XBOOLE_0:def 5;
hence thesis by A1;
end;
theorem Th19:
W is open implies union W is open
proof
assume
A1: W is open;
W c= the topology of GX
proof
let x be object;
assume
A2: x in W;
then reconsider X=x as Subset of GX;
X is open by A1,A2;
hence thesis;
end;
then union W in the topology of GX by PRE_TOPC:def 1;
hence thesis;
end;
theorem Th20:
W is open & W is finite implies meet W is open
proof
assume that
A1: W is open and
A2: W is finite;
consider p being FinSequence such that
A3: rng p = W by A2,FINSEQ_1:52;
consider n being Nat such that
A4: dom p = Seg n by FINSEQ_1:def 2;
defpred X[Nat] means for Z st Z = p.:(Seg $1) & $1 <= n & 1 <= n holds meet
Z is open;
A5: for k be Nat holds X[k] implies X[k+1]
proof
let k be Nat;
assume
A6: for Z st Z = p.:(Seg k) & k <= n & 1 <= n holds meet Z is open;
let Z such that
A7: Z = p.:(Seg(k+1));
assume that
A8: k+1 <= n and
A9: 1 <= n;
A10: now
reconsider G2 = Im(p,k+1) as Subset-Family of GX by A3,Th2,RELAT_1:111;
reconsider G1 = p.:(Seg k) as Subset-Family of GX by A3,Th2,RELAT_1:111;
assume
A11: 0 < k;
k+1 <= n+1 by A8,NAT_1:12;
then k <= n by XREAL_1:6;
then Seg k c= dom p by A4,FINSEQ_1:5;
then
A12: G1 <> {} by A11,RELAT_1:119;
k+1 <= n+1 by A8,NAT_1:12;
then k <= n by XREAL_1:6;
then
A13: meet G1 is open by A6,A9;
0 <= k & 0+1 = 1 by NAT_1:2;
then 1 <= k+1 by XREAL_1:7;
then
A14: k+1 in dom p by A4,A8,FINSEQ_1:1;
then G2 = {p.(k+1)} by FUNCT_1:59;
then
A15: meet G2 = p.(k+1) by SETFAM_1:10;
{k+1} c= dom p by A14,ZFMISC_1:31;
then
A16: G2 <> {} by RELAT_1:119;
p.(k+1) in W by A3,A14,FUNCT_1:def 3;
then
A17: meet G2 is open by A1,A15;
p.:(Seg(k+1)) = p.:(Seg k \/ {k+1}) by FINSEQ_1:9
.= p.:(Seg k) \/ p.:{k+1} by RELAT_1:120;
then meet Z = meet G1 /\ meet G2 by A7,A12,A16,SETFAM_1:9;
hence thesis by A13,A17,TOPS_1:11;
end;
now
assume
A18: k=0;
then
A19: 1 in dom p by A4,A8,FINSEQ_1:1;
then Im(p,1) = {p.1} by FUNCT_1:59;
then meet Z = p.1 by A7,A18,FINSEQ_1:2,SETFAM_1:10;
then meet Z in W by A3,A19,FUNCT_1:def 3;
hence thesis by A1;
end;
hence thesis by A10,NAT_1:3;
end;
A20: X[0]
proof
let Z;
assume that
A21: Z = p.:(Seg 0) and
0 <= n;
A22: {} in the topology of GX by PRE_TOPC:1;
meet Z = {} by A21,SETFAM_1:1;
hence thesis by A22;
end;
A23: for k be Nat holds X[k] from NAT_1:sch 2(A20,A5);
A24: now
assume
A25: 1 <= n;
W = p.:(Seg n) by A3,A4,RELAT_1:113;
hence thesis by A23,A25;
end;
A26: now
assume n = 0;
then Seg n = {};
then W = p.:{} by A3,A4,RELAT_1:113;
then
A27: meet W = {} by SETFAM_1:1;
{} in the topology of GX by PRE_TOPC:1;
hence thesis by A27;
end;
now
assume n <> 0;
then
A28: 0 < n by NAT_1:3;
1 = 0+1;
hence 1 <= n by A28,NAT_1:13;
end;
hence thesis by A24,A26;
end;
theorem
W is closed & W is finite implies union W is closed
proof
reconsider C = COMPLEMENT(W) as Subset-Family of GX;
assume W is closed & W is finite;
then COMPLEMENT(W) is open & COMPLEMENT(W) is finite by Th8,Th9;
then
A1: meet C is open by Th20;
now
assume W <> {};
then meet COMPLEMENT(W) = (union W)` by Th6;
hence thesis by A1;
end;
hence thesis by ZFMISC_1:2;
end;
theorem
W is closed implies meet W is closed
proof
reconsider C = COMPLEMENT(W) as Subset-Family of GX;
assume W is closed;
then COMPLEMENT(W) is open by Th9;
then
A1: union C is open by Th19;
A2: now
assume W <> {};
then union COMPLEMENT(W) = (meet W)` by Th7;
hence thesis by A1;
end;
now
assume W = {};
then meet W = {}GX by SETFAM_1:def 1;
hence thesis;
end;
hence thesis by A2;
end;
::
:: SUBSPACES OF A TOPOLOGICAL SPACE
::
theorem
for F being Subset-Family of A holds F is Subset-Family of T
proof
let F be Subset-Family of A;
[#] A c= [#]T by PRE_TOPC:def 4;
then bool the carrier of A c= bool the carrier of T by ZFMISC_1:67;
hence thesis by XBOOLE_1:1;
end;
theorem Th24:
for B being Subset of A holds B is open iff ex C being Subset of
T st C is open & C /\ [#](A) = B
proof
let B be Subset of A;
hereby
assume B is open;
then B in the topology of A;
then consider C being Subset of T such that
A1: C in the topology of T & C /\ [#](A) = B by PRE_TOPC:def 4;
reconsider C as Subset of T;
take C;
thus C is open & C /\ [#] A = B by A1;
end;
given C being Subset of T such that
A2: C is open and
A3: C /\ [#](A) = B;
C in the topology of T by A2;
then B in the topology of A by A3,PRE_TOPC:def 4;
hence thesis;
end;
theorem Th25:
Q is open implies for P being Subset of A st P=Q holds P is open
proof
assume
A1: Q is open;
let P be Subset of A;
assume P=Q;
then Q /\ [#] A = P by XBOOLE_1:28;
hence thesis by A1,Th24;
end;
theorem Th26:
Q is closed implies for P being Subset of A st P=Q holds P is closed
proof
assume
A1: Q is closed;
let P be Subset of A;
assume P=Q;
then Q /\ [#] A = P by XBOOLE_1:28;
hence thesis by A1,PRE_TOPC:13;
end;
theorem
F is open implies for G being Subset-Family of A st G=F holds G is open
by Th25;
theorem
F is closed implies for G being Subset-Family of A st G=F holds G is closed
by Th26;
theorem Th29:
M /\ N is Subset of T|N
proof
M /\ N c= N by XBOOLE_1:17;
then M /\ N c= [#](T|N) by PRE_TOPC:def 5;
hence thesis;
end;
::
:: RESTRICTION OF A FAMILY
::
definition
let T be TopStruct, P be Subset of T, F be Subset-Family of T;
func F|P -> Subset-Family of T|P means
:Def3:
for Q being Subset of T|P
holds Q in it iff ex R being Subset of T st R in F & R /\ P = Q;
existence
proof
thus ex G being Subset-Family of T|P st for Q being Subset of T|P holds Q
in G iff ex R being Subset of T st R in F & R /\ P = Q
proof
defpred X[Subset of T|P] means ex R being Subset of T st R in F & R /\ P
= $1;
ex G being Subset-Family of T|P st for Q being Subset of T|P holds Q
in G iff X[Q] from SUBSET_1:sch 3;
hence thesis;
end;
end;
uniqueness
proof
thus for G,H being Subset-Family of T|P st (for Q being Subset of T|P
holds Q in G iff ex R being Subset of T st R in F & R /\ P = Q) & (for Q being
Subset of T|P holds Q in H iff ex R being Subset of T st R in F & R /\ P = Q)
holds G = H
proof
let G,H be Subset-Family of T|P such that
A1: for Q being Subset of T|P holds Q in G iff ex R being Subset of
T st R in F & R /\ P = Q and
A2: for Q being Subset of T|P holds Q in H iff ex R being Subset of
T st R in F & R /\ P = Q;
for x being object holds x in G iff x in H
proof let x be object;
hereby
assume
A3: x in G;
then reconsider X=x as Subset of T|P;
ex R being Subset of T st R in F & R /\ P = X by A1,A3;
hence x in H by A2;
end;
assume
A4: x in H;
then reconsider X=x as Subset of T|P;
ex R being Subset of T st R in F & R /\ P = X by A2,A4;
hence thesis by A1;
end;
hence thesis by TARSKI:2;
end;
end;
end;
theorem
F c= G implies F|M c= G|M
proof
assume
A1: F c= G;
let x be object;
assume
A2: x in F|M;
then reconsider X=x as Subset of T|M;
ex R being Subset of T st R in F & R /\ M = X by A2,Def3;
hence thesis by A1,Def3;
end;
theorem Th31:
Q in F implies Q /\ M in F|M
proof
reconsider QQ = Q /\ M as Subset of T|M by Th29;
A1: Q /\ M = QQ;
assume Q in F;
hence thesis by A1,Def3;
end;
theorem
Q c= union F implies Q /\ M c= union(F|M)
proof
assume
A1: Q c= union F;
now
assume M <> {};
thus Q /\ M c= union(F|M)
proof
let x be object;
assume
A2: x in Q /\ M;
then x in Q by XBOOLE_0:def 4;
then consider Z being set such that
A3: x in Z and
A4: Z in F by A1,TARSKI:def 4;
reconsider ZZ=Z as Subset of T by A4;
ZZ /\ M in F|M by A4,Th31;
then reconsider ZP = ZZ /\ M as Subset of T|M;
A5: ZP in F|M by A4,Th31;
x in M by A2,XBOOLE_0:def 4;
then x in ZP by A3,XBOOLE_0:def 4;
hence thesis by A5,TARSKI:def 4;
end;
end;
hence thesis;
end;
theorem
M c= union F implies M = union (F|M)
proof
assume
A1: M c= union F;
for x being object holds x in M iff x in union(F|M)
proof let x be object;
hereby
assume
A2: x in M;
then consider A being set such that
A3: x in A and
A4: A in F by A1,TARSKI:def 4;
reconsider A9=A as Subset of T by A4;
A /\ M c= M by XBOOLE_1:17;
then A /\ M c= [#](T|M) by PRE_TOPC:def 5;
then reconsider B=A9 /\ M as Subset of T|M;
A5: B in F|M by A4,Def3;
x in A /\ M by A2,A3,XBOOLE_0:def 4;
hence x in union(F|M) by A5,TARSKI:def 4;
end;
assume x in union(F|M);
then consider A being set such that
A6: x in A and
A7: A in F|M by TARSKI:def 4;
reconsider B = A as Subset of T|M by A7;
ex R being Subset of T st R in F & R /\ M = B by A7,Def3;
hence thesis by A6,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:2;
end;
theorem Th34:
union(F|M) c= union F
proof
let x be object;
assume x in union(F|M);
then consider A being set such that
A1: x in A and
A2: A in F|M by TARSKI:def 4;
reconsider Q = A as Subset of T|M by A2;
consider R being Subset of T such that
A3: R in F and
A4: R /\ M = Q by A2,Def3;
x in R by A1,A4,XBOOLE_0:def 4;
hence thesis by A3,TARSKI:def 4;
end;
theorem
M c= union (F|M) implies M c= union F
proof
assume
A1: M c= union(F|M);
union(F|M) c= union F by Th34;
hence thesis by A1;
end;
theorem
F is finite implies F|M is finite
proof
defpred X[object,object] means
for X being Subset of T st X = $1 holds $2 = X /\ M;
A1: for x being object st x in F ex y being object st X[x,y]
proof
let x be object;
assume x in F;
then reconsider X=x as Subset of T;
reconsider y=X /\ M as set;
take y;
thus thesis;
end;
consider f being Function such that
A2: dom f = F and
A3: for x being object st x in F holds X[x,f.x] from CLASSES1:sch 1(A1);
for x being object holds x in rng f iff x in F|M
proof let x be object;
hereby
assume x in rng f;
then consider y being object such that
A4: y in dom f and
A5: x=f.y by FUNCT_1:def 3;
reconsider Y=y as Subset of T by A2,A4;
Y /\ M c= M by XBOOLE_1:17;
then Y /\ M c= [#](T|M) by PRE_TOPC:def 5;
then reconsider X=f.y as Subset of T|M by A2,A3,A4;
f.y = Y /\ M by A2,A3,A4;
then X in F|M by A2,A4,Def3;
hence x in F|M by A5;
end;
assume
A6: x in F|M;
then reconsider X=x as Subset of T|M;
consider R being Subset of T such that
A7: R in F and
A8: R /\ M = X by A6,Def3;
f.R = R /\ M by A3,A7;
hence thesis by A2,A7,A8,FUNCT_1:def 3;
end;
then rng f = F|M by TARSKI:2;
then
A9: f.:(F) = F|M by A2,RELAT_1:113;
assume F is finite;
hence thesis by A9,FINSET_1:5;
end;
theorem
F is open implies F|M is open
proof
assume
A1: F is open;
let Q be Subset of T|M;
assume Q in F|M;
then consider R being Subset of T such that
A2: R in F and
A3: R /\ M = Q by Def3;
reconsider R as Subset of T;
A4: Q = R /\ [#](T|M) by A3,PRE_TOPC:def 5;
R is open by A1,A2;
hence thesis by A4,Th24;
end;
theorem
F is closed implies F|M is closed
proof
assume
A1: F is closed;
let Q be Subset of T|M;
assume Q in F|M;
then consider R being Subset of T such that
A2: R in F and
A3: R /\ M = Q by Def3;
reconsider R as Subset of T;
A4: Q = R /\ [#](T|M) by A3,PRE_TOPC:def 5;
R is closed by A1,A2;
hence thesis by A4,PRE_TOPC:13;
end;
theorem
for F being Subset-Family of A st F is open ex G being Subset-Family
of T st G is open & for AA being Subset of T st AA = [#] A holds F = G|AA
proof
let F be Subset-Family of A;
assume
A1: F is open;
[#] A c= [#]T by PRE_TOPC:def 4;
then reconsider At = [#] A as Subset of T;
defpred X[Subset of T] means ex X1 being Subset of T st X1 = $1 & X1 is open
& $1 /\ At in F;
consider G being Subset-Family of T such that
A2: for X being Subset of T holds X in G iff X[X] from SUBSET_1:sch 3;
take G;
thus G is open
proof
let H be Subset of T;
assume H in G;
then ex X1 being Subset of T st X1 = H & X1 is open & H /\ At in F by A2;
hence thesis;
end;
let AA be Subset of T;
assume
A3: AA = [#] A;
then F c= bool AA;
then F c= bool [#](T|AA) by PRE_TOPC:def 5;
then reconsider FF = F as Subset-Family of T|AA;
for X being Subset of T|AA holds X in FF iff ex X9 being Subset of T st
X9 in G & X9 /\ AA=X
proof
let X be Subset of T|AA;
thus X in FF implies ex X9 being Subset of T st X9 in G & X9 /\ AA=X
proof
assume
A4: X in FF;
then reconsider XX=X as Subset of A;
XX is open by A1,A4;
then consider Y being Subset of T such that
A5: Y is open & Y /\ [#] A = XX by Th24;
take Y;
thus thesis by A2,A3,A4,A5;
end;
given X9 being Subset of T such that
A6: X9 in G and
A7: X9 /\ AA=X;
ex X1 being Subset of T st X1 = X9 & X1 is open & X9 /\ At in F by A2,A6;
hence thesis by A3,A7;
end;
hence thesis by Def3;
end;
theorem
ex f being Function st dom f = F & rng f = F|P & for x st x in F for Q
st Q = x holds f.x = Q /\ P
proof
defpred X[object,object] means for Q st Q=$1 holds $2=Q /\ P;
A1: for x being object st x in F ex y being object st X[x,y]
proof
let x be object;
assume x in F;
then reconsider Q=x as Subset of T;
reconsider y=Q /\ P as set;
take y;
thus thesis;
end;
consider f being Function such that
A2: dom f = F and
A3: for x being object st x in F holds X[x,f.x] from CLASSES1:sch 1(A1);
take f;
thus dom f = F by A2;
for x being object holds x in rng f iff x in F|P
proof let x be object;
hereby
assume x in rng f;
then consider y being object such that
A4: y in dom f and
A5: f.y=x by FUNCT_1:def 3;
reconsider Y=y as Subset of T by A2,A4;
Y /\ P c= P by XBOOLE_1:17;
then Y /\ P c= [#](T|P) by PRE_TOPC:def 5;
then reconsider X=x as Subset of T|P by A2,A3,A4,A5;
X = Y /\ P by A2,A3,A4,A5;
hence x in F|P by A2,A4,Def3;
end;
assume
A6: x in F|P;
then reconsider X=x as Subset of T|P;
consider Q be Subset of T such that
A7: Q in F and
A8: Q /\ P = X by A6,Def3;
reconsider p=Q as set;
f.p = x by A3,A7,A8;
hence thesis by A2,A7,FUNCT_1:def 3;
end;
hence rng f = F|P by TARSKI:2;
thus thesis by A3;
end;
theorem Th41:
for X,Y being 1-sorted, f being Function of X, Y st [#]Y = {}
implies [#]X = {} holds f"([#]Y) = [#]X
proof
let X,Y be 1-sorted, f be Function of X, Y such that
A1: [#]Y={} implies [#]X={};
f"(rng f) = dom f by RELAT_1:134
.= [#]X by A1,FUNCT_2:def 1;
then [#]X c= f"([#]Y) by RELAT_1:143;
hence thesis by XBOOLE_0:def 10;
end;
theorem
for T being 1-sorted, S being non empty 1-sorted, f being Function of
T, S, H being Subset-Family of S holds ("f).:H is Subset-Family of T
proof
let T be 1-sorted, S be non empty 1-sorted, f be Function of T, S, H be
Subset-Family of S;
("f).:H c= rng "f & rng "f c= bool dom f by FUNCT_3:22,RELAT_1:111;
then ("f).:H c= bool dom f;
hence thesis by FUNCT_2:def 1;
end;
::
:: CONTINUOUS MAPPING
::
reserve S for non empty TopStruct,
f for Function of T, S,
H for Subset-Family of S;
theorem Th43:
for X,Y being TopStruct, f being Function of X,Y st [#]Y = {}
implies [#]X = {} holds f is continuous iff for P being Subset of Y st P is
open holds f"P is open
proof
let X,Y be TopStruct, f be Function of X,Y;
assume
A1: [#]Y={} implies [#]X={};
hereby
assume
A2: f is continuous;
let P1 be Subset of Y;
assume P1 is open;
then P1` is closed by TOPS_1:4;
then
A3: f"(P1`) is closed by A2;
f"(P1`) = f"([#]Y) \ f"P1 by FUNCT_1:69
.= [#]X \ f"P1 by A1,Th41
.= (f"P1)`;
hence f"P1 is open by A3,TOPS_1:4;
end;
assume
A4: for P1 being Subset of Y st P1 is open holds f"P1 is open;
let P1 be Subset of Y;
assume P1 is closed;
then P1` is open;
then
A5: f"(P1`) is open by A4;
f"(P1`) = f"([#]Y) \ f"P1 by FUNCT_1:69
.= [#]X \ f"P1 by A1,Th41
.= (f"P1)`;
hence thesis by A5;
end;
theorem Th44:
for T being TopSpace, S being TopSpace, f being Function of T, S
holds f is continuous iff for P1 being Subset of S holds Cl(f"P1) c= f"(Cl P1)
proof
let T be TopSpace, S be TopSpace, f be Function of T, S;
hereby
assume
A1: f is continuous;
let P1 be Subset of S;
Cl(Cl P1) = Cl P1;
then Cl P1 is closed by PRE_TOPC:22;
then
A2: f"(Cl P1) is closed by A1;
f"P1 c= f"(Cl P1) by PRE_TOPC:18,RELAT_1:143;
then Cl(f"P1) c= Cl(f"(Cl P1)) by PRE_TOPC:19;
hence Cl(f"P1) c= f"(Cl P1) by A2,PRE_TOPC:22;
end;
assume
A3: for P1 being Subset of S holds Cl(f"P1) c= f"(Cl P1);
let P1 be Subset of S;
assume P1 is closed;
then Cl P1 = P1 by PRE_TOPC:22;
then f"P1 c= Cl(f"P1) & Cl(f"P1) c= f"P1 by A3,PRE_TOPC:18;
then f"P1 = Cl(f"P1) by XBOOLE_0:def 10;
hence thesis by PRE_TOPC:22;
end;
theorem Th45:
for T being TopSpace, S being non empty TopSpace, f being
Function of T, S holds f is continuous iff for P being Subset of T holds f.:(Cl
P) c= Cl(f.:P)
proof
let T be TopSpace, S be non empty TopSpace, f be Function of T, S;
hereby
assume
A1: f is continuous;
let P be Subset of T;
P c= [#]T;
then P c= dom f by FUNCT_2:def 1;
then
A2: Cl P c= Cl(f"(f.:P)) by FUNCT_1:76,PRE_TOPC:19;
Cl(f"(f.:P)) c= f"(Cl(f.:P)) by A1,Th44;
then Cl P c= f"(Cl(f.:P)) by A2;
then
A3: f.:(Cl P) c= f.:(f"(Cl(f.:P))) by RELAT_1:123;
f.:(f"(Cl(f.:P))) c= Cl(f.:P) by FUNCT_1:75;
hence f.:(Cl P) c= Cl(f.:P) by A3;
end;
assume
A4: for P being Subset of T holds f.:(Cl P) c= Cl(f.:P);
now
let P1 be Subset of S;
Cl(f"P1) c= [#]T;
then Cl(f"P1) c= dom f by FUNCT_2:def 1;
then
A5: Cl(f"P1) c= f"(f.:Cl(f"P1)) by FUNCT_1:76;
f.:(Cl(f"P1)) c= Cl(f.:(f"P1)) & Cl(f.:(f"P1)) c= Cl P1 by A4,FUNCT_1:75
,PRE_TOPC:19;
then f.:(Cl(f"P1)) c= Cl P1;
then f"(f.:(Cl(f"P1))) c= f"(Cl P1) by RELAT_1:143;
hence Cl(f"P1) c= f"(Cl P1) by A5;
end;
hence thesis by Th44;
end;
theorem Th46:
for T,V being TopStruct,S being non empty TopStruct, f being
Function of T,S, g being Function of S,V holds f is continuous & g is
continuous implies g*f is continuous
proof
let T,V be TopStruct,S be non empty TopStruct;
let f be Function of T,S, g be Function of S,V;
assume that
A1: f is continuous and
A2: g is continuous;
let P be Subset of V;
assume P is closed;
then (g*f)"P = f"(g"P) & g"P is closed by A2,RELAT_1:146;
hence thesis by A1;
end;
theorem
f is continuous & H is open implies for F st F=("f).:H holds F is open
proof
assume that
A1: f is continuous and
A2: H is open;
let F such that
A3: F=("f).:H;
let X be Subset of T;
assume X in F;
then consider y being object such that
A4: y in dom "f and
A5: y in H and
A6: X=("f).y by A3,FUNCT_1:def 6;
reconsider Y=y as Subset of S by A5;
A7: X = f"Y by A4,A6,FUNCT_3:21;
A8: [#]S={} implies [#]T={};
Y is open by A2,A5;
hence thesis by A1,A8,A7,Th43;
end;
theorem
for T, S being TopStruct, f being Function of T, S, H being
Subset-Family of S st f is continuous & H is closed holds for F being
Subset-Family of T st F=("f).:H holds F is closed
proof
let T, S be TopStruct, f be Function of T, S, H be Subset-Family of S;
assume that
A1: f is continuous and
A2: H is closed;
let F be Subset-Family of T such that
A3: F=("f).:H;
let X be Subset of T;
assume X in F;
then consider y being object such that
A4: y in dom "f and
A5: y in H and
A6: X=("f).y by A3,FUNCT_1:def 6;
reconsider Y=y as Subset of S by A5;
A7: X = f"Y by A4,A6,FUNCT_3:21;
Y is closed by A2,A5;
hence thesis by A1,A7;
end;
definition
let S, T be set, f be Function of S,T;
assume
A1: f is bijective;
func f/" -> Function of T,S equals
:Def4:
f";
coherence
proof
rng f = [#]T by A1,FUNCT_2:def 3;
hence thesis by A1,FUNCT_2:25;
end;
end;
notation
let S, T be set, f be Function of S,T;
synonym f" for f/";
end;
theorem Th49:
for T being 1-sorted, S being non empty 1-sorted, f being Function of T,S
st rng f = [#]S & f is one-to-one holds dom(f") = [#]S & rng(f") = [#]T
proof
let T be 1-sorted, S be non empty 1-sorted, f be Function of T,S;
assume that
A1: rng f = [#]S and
A2: f is one-to-one;
A3: f is onto by A1,FUNCT_2:def 3;
hence dom(f") = dom((f qua Function)") by A2,Def4
.= [#]S by A1,A2,FUNCT_1:32;
thus rng(f") = rng((f qua Function)") by A2,A3,Def4
.= dom f by A2,FUNCT_1:33
.= [#]T by FUNCT_2:def 1;
end;
theorem Th50:
for T, S being 1-sorted, f being Function of T,S st rng f = [#]S
& f is one-to-one holds f" is one-to-one
proof
let T, S be 1-sorted, f be Function of T,S;
assume that
A1: rng f = [#]S and
A2: f is one-to-one;
A3: f is onto by A1,FUNCT_2:def 3;
(f qua Function)" is one-to-one by A2;
hence thesis by A2,A3,Def4;
end;
theorem Th51:
for T being 1-sorted, S being non empty 1-sorted, f being
Function of T,S st rng f = [#]S & f is one-to-one holds (f")" = f
proof
let T be 1-sorted, S be non empty 1-sorted, f be Function of T,S;
assume that
A1: rng f = [#]S and
A2: f is one-to-one;
A3: f is onto by A1,FUNCT_2:def 3;
f = ((f qua Function)")" by A2,FUNCT_1:43;
then
A4: f = (f" qua Function)" by A3,A2,Def4;
A5: f" is one-to-one by A1,A2,Th50;
rng(f") = [#]T by A1,A2,Th49;
then f" is onto by FUNCT_2:def 3;
hence thesis by A4,A5,Def4;
end;
theorem
for T, S being 1-sorted, f being Function of T,S st rng f = [#]S & f
is one-to-one holds f"*f = id dom f & f*f" = id rng f
proof
let T, S be 1-sorted, f be Function of T,S;
assume that
A1: rng f = [#]S and
A2: f is one-to-one;
A3: f is onto by A1,FUNCT_2:def 3;
(f qua Function)"*f = id dom f & f*(f qua Function)" = id rng f by A2,
FUNCT_1:39;
hence thesis by A2,A3,Def4;
end;
theorem Th53:
for T being 1-sorted, S, V being non empty 1-sorted, f being
Function of T,S, g being Function of S,V st rng f = [#]S & f is one-to-one &
dom g = [#]S & rng g = [#]V & g is one-to-one holds (g*f)" = f"*g"
proof
let T be 1-sorted, S, V be non empty 1-sorted;
let f be Function of T,S;
let g be Function of S,V;
assume that
A1: rng f = [#]S and
A2: f is one-to-one;
assume that
A3: dom g = [#]S and
A4: rng g = [#] V and
A5: g is one-to-one;
A6: f is onto & g is onto by A1,A4,FUNCT_2:def 3;
rng(g*f) = [#] V by A1,A3,A4,RELAT_1:28;
then g*f is onto by FUNCT_2:def 3;
then
A7: (g*f)" = ((g*f) qua Function)" by A2,A5,Def4;
A8: f" = (f qua Function)" by A2,A6,Def4;
g" = (g qua Function)" by A5,A6,Def4;
hence thesis by A2,A5,A8,A7,FUNCT_1:44;
end;
theorem Th54:
for T, S being 1-sorted, f being Function of T, S, P being
Subset of T st rng f = [#]S & f is one-to-one holds f.:P = (f")"P
proof
let T, S be 1-sorted, f be Function of T, S, P be Subset of T;
assume that
A1: rng f = [#]S and
A2: f is one-to-one;
A3: f is onto by A1,FUNCT_2:def 3;
f.:P = ((f qua Function)")"P by A2,FUNCT_1:84;
hence thesis by A2,A3,Def4;
end;
theorem Th55:
for T, S being 1-sorted, f being Function of T,S, P1 being
Subset of S st rng f = [#]S & f is one-to-one holds f"P1 = (f").:P1
proof
let T, S be 1-sorted, f be Function of T, S, P1 be Subset of S;
assume rng f = [#]S;
then
A1: f is onto by FUNCT_2:def 3;
assume
A2: f is one-to-one;
f"P1 = ((f qua Function)").:P1 by A2,FUNCT_1:85;
hence thesis by A1,A2,Def4;
end;
::
:: HOMEOMORPHISM
::
definition
let S, T be TopStruct, f be Function of S, T;
attr f is being_homeomorphism means
dom f = [#]S & rng f = [#]T & f
is one-to-one & f is continuous & f" is continuous;
end;
theorem
f is being_homeomorphism implies f" is being_homeomorphism
by Th49,Th50,Th51;
theorem
for T, S, V being non empty TopStruct, f being Function of T,S, g
being Function of S,V st f is being_homeomorphism & g is being_homeomorphism
holds g*f is being_homeomorphism
proof
let T, S, V be non empty TopStruct;
let f be Function of T,S;
let g be Function of S,V;
assume that
A1: f is being_homeomorphism and
A2: g is being_homeomorphism;
A3: rng f = [#](S) & dom g = [#]S by A1,A2;
A4: rng g = [#](V) by A2;
dom f = [#]T by A1;
hence dom(g*f) = [#]T & rng(g*f) = [#] V by A3,A4,RELAT_1:27,28;
A5: f is one-to-one & g is one-to-one by A1,A2;
hence g*f is one-to-one;
f is continuous & g is continuous by A1,A2;
hence g*f is continuous by Th46;
f" is continuous & g" is continuous by A1,A2;
then f"*g" is continuous by Th46;
hence thesis by A3,A4,A5,Th53;
end;
theorem
f is being_homeomorphism iff dom f = [#]T & rng f = [#]S & f is
one-to-one & for P holds P is closed iff f.:P is closed
proof
hereby
assume
A1: f is being_homeomorphism;
hence
A2: dom f = [#]T & rng f = [#]S & f is one-to-one;
let P;
A3: f" is continuous by A1;
hereby
assume
A4: P is closed;
f is onto by A2,FUNCT_2:def 3;
then (f")"P = ((f qua Function)")"P by A2,Def4
.= f.:P by A2,FUNCT_1:84;
hence f.:P is closed by A3,A4;
end;
assume
A5: f.:P is closed;
f is continuous by A1;
then
A6: f"(f.:P) is closed by A5;
dom f = [#]T by FUNCT_2:def 1;
then
A7: P c= f"(f.:P) by FUNCT_1:76;
f"(f.:P) c= P by A2,FUNCT_1:82;
hence P is closed by A6,A7,XBOOLE_0:def 10;
end;
assume that
A8: dom f = [#]T and
A9: rng f = [#]S and
A10: f is one-to-one;
assume
A11: for P being Subset of T holds P is closed iff f.:P is closed;
A12: f is continuous
proof
let B be Subset of S such that
A13: B is closed;
set D = f"B;
B = f.:D by A9,FUNCT_1:77;
hence thesis by A11,A13;
end;
f" is continuous
proof
let B be Subset of T such that
A14: B is closed;
f is onto by A9,FUNCT_2:def 3;
then (f")"B = ((f qua Function)")"B by A10,Def4
.= f.:B by A10,FUNCT_1:84;
hence thesis by A11,A14;
end;
hence thesis by A8,A9,A10,A12;
end;
reserve T for non empty TopSpace,
S for TopSpace,
P1 for Subset of S,
f for Function of T, S;
theorem
f is being_homeomorphism iff dom f = [#]T & rng f = [#]S & f is
one-to-one & for P1 holds f"(Cl P1) = Cl(f"P1)
proof
hereby
assume
A1: f is being_homeomorphism;
hence
A2: dom f = [#]T & rng f = [#]S & f is one-to-one;
let P1;
f is continuous by A1;
then
A3: Cl(f"P1) c= f"(Cl P1) by Th44;
f" is continuous by A1;
then
A4: (f").:(Cl P1) c= Cl((f").:P1) by Th45;
f"(Cl P1) = (f").:(Cl P1) & f"P1 = (f").:P1 by A2,Th55;
hence f"(Cl P1) = Cl(f"P1) by A3,A4,XBOOLE_0:def 10;
end;
assume that
A5: dom f = [#]T and
A6: rng f = [#]S & f is one-to-one;
assume
A7: for P1 holds f"(Cl P1) = Cl(f"P1);
thus dom f = [#]T & rng f = [#]S & f is one-to-one by A5,A6;
for P1 holds Cl(f"P1) c= f"(Cl P1) by A7;
hence f is continuous by Th44;
now
let P1;
(f").:(Cl P1) = f"(Cl P1) & (f").:P1 = f"P1 by A6,Th55;
hence (f").:(Cl P1) c= Cl((f").:P1) by A7;
end;
hence thesis by Th45;
end;
reserve T for TopSpace,
S for non empty TopSpace,
P for Subset of T,
f for Function of T, S;
theorem
f is being_homeomorphism iff dom f = [#]T & rng f = [#]S & f is
one-to-one & for P holds f.:(Cl P) = Cl(f.:P)
proof
hereby
assume
A1: f is being_homeomorphism;
hence
A2: dom f = [#]T & rng f = [#]S & f is one-to-one;
let P;
f is continuous by A1;
then
A3: f.:(Cl P) c= Cl(f.:P) by Th45;
f" is continuous by A1;
then
A4: Cl((f")"P) c= (f")"(Cl P) by Th44;
(f")"P = f.:P & (f")"(Cl P) = f.:(Cl P) by A2,Th54;
hence f.:(Cl P) = Cl(f.:P) by A3,A4,XBOOLE_0:def 10;
end;
assume that
A5: dom f = [#]T and
A6: rng f = [#]S & f is one-to-one;
assume
A7: for P holds f.:(Cl P) = Cl(f.:P);
thus dom f = [#]T & rng f = [#]S & f is one-to-one by A5,A6;
for P holds f.:(Cl P) c= Cl(f.:P) by A7;
hence f is continuous by Th45;
now
let P;
(f")"P = f.:P & (f")"(Cl P) = f.:(Cl P) by A6,Th54;
hence Cl((f")"P) c= (f")"(Cl P) by A7;
end;
hence thesis by Th44;
end;
theorem Th61: :: TOPREAL5:5, AK, 21.02.2006
for X,Y being non empty TopSpace for f being Function of X,Y, A
being Subset of X st f is continuous & A is connected holds f.:A is connected
proof
let X,Y be non empty TopSpace;
let f be Function of X,Y, A be Subset of X;
assume
A1: f is continuous;
assume
A2: A is connected;
assume not f.:A is connected;
then consider P,Q being Subset of Y such that
A3: f.:A = P \/ Q and
A4: P,Q are_separated and
A5: P <> {}(Y) and
A6: Q <> {}(Y) by CONNSP_1:15;
reconsider P1=f"P,Q1=f"Q as Subset of X;
set P2=P1/\A,Q2=Q1/\A;
set y = the Element of P;
y in f.:A by A3,A5,XBOOLE_0:def 3;
then consider x being object such that
A7: x in dom f and
A8: x in A and
A9: y=f.x by FUNCT_1:def 6;
x in f"P by A5,A7,A9,FUNCT_1:def 7;
then
A10: P2<>{} by A8,XBOOLE_0:def 4;
A11: the carrier of X=dom f by FUNCT_2:def 1;
P misses Cl Q by A4,CONNSP_1:def 1;
then
A12: f"(P) /\ f"(Cl Q) = f"(P /\ Cl Q) & f"(P /\ Cl Q)=f"({}Y) by FUNCT_1:68
,XBOOLE_0:def 7;
Cl Q1 c=f"(Cl Q) by A1,Th44;
then P1 /\ Cl Q1 = {} by A12,XBOOLE_1:3,26;
then
A13: P1 misses Cl Q1 by XBOOLE_0:def 7;
Cl P misses Q by A4,CONNSP_1:def 1;
then
A14: f"(Cl P) /\ f"Q = f"(Cl P /\ Q) & f"(Cl P /\ Q)=f"({}Y) by FUNCT_1:68
,XBOOLE_0:def 7;
Cl P1 c=f"(Cl P) by A1,Th44;
then Cl P1 /\ Q1 = {}X by A14,XBOOLE_1:3,26;
then Cl P1 misses Q1 by XBOOLE_0:def 7;
then
A15: P1,Q1 are_separated by A13,CONNSP_1:def 1;
set z = the Element of Q;
z in P \/ Q by A6,XBOOLE_0:def 3;
then consider x1 being object such that
A16: x1 in dom f and
A17: x1 in A and
A18: z=f.x1 by A3,FUNCT_1:def 6;
x1 in f"Q by A6,A16,A18,FUNCT_1:def 7;
then
A19: Q2<>{} by A17,XBOOLE_0:def 4;
f"(f.:A)=f"P \/ f"Q by A3,RELAT_1:140;
then
A20: A=(P1 \/ Q1)/\A by A11,FUNCT_1:76,XBOOLE_1:28
.=P2 \/ Q2 by XBOOLE_1:23;
P2 c=P1 & Q2 c=Q1 by XBOOLE_1:17;
then ex P3,Q3 being Subset of X st A = P3 \/ Q3 & P3,Q3 are_separated & P3
<> {}(X) & Q3 <> {}(X) by A15,A20,A10,A19,CONNSP_1:7;
hence contradiction by A2,CONNSP_1:15;
end;
theorem :: JORDAN18:2, AK, 21.02.2006
for S,T being non empty TopSpace, f being Function of S,T, A being
Subset of T st f is being_homeomorphism & A is connected holds f"A is connected
proof
let S,T be non empty TopSpace, f be Function of S,T, A be Subset of T such
that
A1: f is being_homeomorphism and
A2: A is connected;
f" is continuous by A1;
then
A3: f".:A is connected by A2,Th61;
rng f = [#]T & f is one-to-one by A1;
hence thesis by A3,Th55;
end;
begin :: Addenda
:: from JORDAN1, 2008.07.07, A.T.
reserve GX,GY for non empty TopSpace;
theorem
for GX being non empty TopSpace st (for x,y being Point of GX ex GY st
(GY is connected & ex f being Function of GY,GX st f is continuous & x in rng(f
)& y in rng(f))) holds GX is connected
proof
let GX;
assume
A1: for x,y being Point of GX ex GY st (GY is connected & ex f being
Function of GY,GX st f is continuous & x in rng f & y in rng f);
for A,B being Subset of GX st [#](GX) = A \/ B & A <> {}(GX) & B <> {}(
GX) & A is open & B is open holds A meets B
proof
let A,B be Subset of GX;
assume that
A2: [#](GX) = A \/ B and
A3: A <> {}(GX) and
A4: B <> {}(GX) and
A5: A is open & B is open;
set v = the Element of B;
set u = the Element of A;
reconsider y=v as Point of GX by A2,A4,XBOOLE_0:def 3;
reconsider x=u as Point of GX by A2,A3,XBOOLE_0:def 3;
consider GY such that
A6: GY is connected and
A7: ex f being Function of GY,GX st f is continuous & x in rng f & y
in rng f by A1;
consider f being Function of GY,GX such that
A8: f is continuous and
A9: x in rng f and
A10: y in rng f by A7;
f"([#] GX)=[#] GY by Th41;
then
A11: f"A \/ f"B = [#] GY by A2,RELAT_1:140;
rng f /\ B <> {} by A4,A10,XBOOLE_0:def 4;
then rng f meets B by XBOOLE_0:def 7;
then
A12: f"B <> {}(GY) by RELAT_1:138;
rng f /\ A <> {} by A3,A9,XBOOLE_0:def 4;
then rng f meets A by XBOOLE_0:def 7;
then
A13: f"A <> {}(GY) by RELAT_1:138;
[#]GX <> {};
then f"A is open & f"B is open by A5,A8,Th43;
then f"A meets f"B by A6,A11,A13,A12,CONNSP_1:11;
then f"A /\ f"B <> {} by XBOOLE_0:def 7;
then f"(A /\ B) <> {} by FUNCT_1:68;
then rng f meets (A /\ B) by RELAT_1:138;
then ex u1 being object st u1 in rng f & u1 in A /\ B by XBOOLE_0:3;
hence thesis by XBOOLE_0:4;
end;
hence thesis by CONNSP_1:11;
end;
:: Added by AK, 2009.09.20
theorem Th64:
for X being TopStruct, F being Subset-Family of X holds
F is open iff F c= the topology of X
proof
let X be TopStruct, F be Subset-Family of X;
thus F is open implies F c= the topology of X
proof
assume
A1: F is open;
let A be object;
assume
A2: A in F;
then reconsider A as Subset of X;
A is open by A1,A2;
hence thesis;
end;
assume
A3: F c= the topology of X;
let A be Subset of X;
thus thesis by A3;
end;
theorem
for X being TopStruct, F being Subset-Family of X holds
F is closed iff F c= COMPLEMENT the topology of X
proof
let X be TopStruct, F be Subset-Family of X;
thus F is closed implies F c= COMPLEMENT the topology of X
proof
assume
A1: F is closed;
let A be object;
assume
A2: A in F;
then reconsider A as Subset of X;
A is closed by A1,A2;
then A` is open;
then A` in the topology of X;
hence thesis by SETFAM_1:def 7;
end;
assume
A3: F c= COMPLEMENT the topology of X;
let A be Subset of X;
assume A in F;
then A` in the topology of X by A3,SETFAM_1:def 7;
then A` is open;
hence thesis;
end;
registration
let X be TopStruct;
cluster the topology of X -> open;
coherence by Th64;
cluster open for Subset-Family of X;
existence
proof
take the topology of X;
thus thesis;
end;
end;