:: Remarks on Special Subsets of Topological Spaces
:: by Zbigniew Karno
::
:: Received April 6, 1993
:: Copyright (c) 1993-2017 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 PRE_TOPC, SUBSET_1, XBOOLE_0, STRUCT_0, TOPS_1, TARSKI, RCOMP_1,
TOPS_3;
notations TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1,
TSEP_1;
constructors TOPS_1, BORSUK_1, TSEP_1;
registrations PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1;
requirements BOOLE, SUBSET;
definitions PRE_TOPC, XBOOLE_0;
equalities XBOOLE_0, SUBSET_1, STRUCT_0;
expansions PRE_TOPC, XBOOLE_0;
theorems PRE_TOPC, TOPS_1, TOPS_2, TSEP_1, TDLAT_3, SUBSET_1, TARSKI,
XBOOLE_0, XBOOLE_1;
begin
:: 1. Selected Properties of Subsets of a Topological Space.
reserve X for TopStruct,
A for Subset of X;
theorem Th1:
(A = {}X iff A` = [#]X) & (A = {} iff A` = the carrier of X)
proof
thus A = {}X iff A` = [#]X
proof
thus A = {}X implies A` = [#]X;
assume A` = [#]X;
then A`` = {}X by XBOOLE_1:37;
hence thesis;
end;
hence thesis;
end;
theorem Th2:
(A = [#]X iff A` = {}X) & (A = the carrier of X iff A` = {})
by XBOOLE_1:37;
theorem Th3:
for X being TopSpace, A,B being Subset of X holds Int A /\ Cl B c= Cl(A /\ B)
proof
let X be TopSpace, A,B be Subset of X;
(Int A) /\ B c= A /\ B by TOPS_1:16,XBOOLE_1:26;
then
A1: Cl((Int A) /\ B) c= Cl(A /\ B) by PRE_TOPC:19;
Int A /\ Cl B c= Cl((Int A) /\ B) by TOPS_1:13;
hence thesis by A1,XBOOLE_1:1;
end;
reserve X for TopSpace,
A,B for Subset of X;
theorem Th4:
Int(A \/ B) c= (Cl A) \/ Int B
proof
(Int A`) /\ Cl B` c= Cl(( A`) /\ B`) by Th3;
then (Cl(( A`) /\ B`))` c= ((Int A`) /\ Cl B`)` by SUBSET_1:12;
then Int((( A`) /\ B`)`) c= (((Int A`) /\ Cl B`))` by TDLAT_3:3;
then Int(( A``) \/ ( B``)) c= (((Int A`) /\ Cl B`))` by XBOOLE_1:54;
then Int(A \/ B) c= (Int A`)` \/ (Cl B`)` by XBOOLE_1:54;
then Int(A \/ B) c= Cl A \/ (Cl B`)` by TDLAT_3:1;
hence thesis by TOPS_1:def 1;
end;
theorem Th5:
for A being Subset of X st A is closed holds Int(A \/ B) c= A \/ Int B
proof
let A be Subset of X;
assume A is closed;
then Cl A = A by PRE_TOPC:22;
hence thesis by Th4;
end;
theorem Th6:
for A being Subset of X st A is closed holds Int(A \/ B) = Int(A \/ Int B)
proof
let A be Subset of X;
A \/ Int B c= A \/ B by TOPS_1:16,XBOOLE_1:9;
then
A1: Int(A \/ Int B) c= Int(A \/ B) by TOPS_1:19;
assume A is closed;
then Int Int(A \/ B) c= Int(A \/ Int B) by Th5,TOPS_1:19;
hence thesis by A1;
end;
theorem Th7:
A misses Int Cl A implies Int Cl A = {}
proof
reconsider A9 = A as Subset of X;
assume A /\ Int Cl A = {};
then A9 misses Int Cl A9;
then (Cl A) misses (Int Cl A) by TSEP_1:36;
then (Cl A) /\ (Int Cl A) = {};
hence thesis by TOPS_1:16,XBOOLE_1:28;
end;
theorem
A \/ Cl Int A = the carrier of X implies Cl Int A = the carrier of X
proof
assume A \/ Cl Int A = the carrier of X;
then (Int A) \/ (Cl Int A) = the carrier of X by TDLAT_3:4;
hence thesis by PRE_TOPC:18,XBOOLE_1:12;
end;
begin
:: 2. Special Subsets of a Topological Space.
definition
let X be TopStruct, A be Subset of X;
redefine attr A is boundary means
:Def1:
Int A = {};
compatibility by TOPS_1:48;
end;
theorem
{}X is boundary;
reserve X for non empty TopSpace,
A for Subset of X;
theorem Th10:
A is boundary implies A <> the carrier of X
proof
assume
A1: Int A = {};
assume A = the carrier of X;
then A = [#]X;
hence contradiction by A1,TOPS_1:15;
end;
reserve X for TopSpace,
A,B for Subset of X;
theorem Th11:
B is boundary & A c= B implies A is boundary
by TOPS_1:19,XBOOLE_1:3;
theorem
A is boundary iff for C being Subset of X st A` c= C & C is closed
holds C = the carrier of X
proof
thus A is boundary implies for C being Subset of X st A` c= C & C is closed
holds C = the carrier of X
proof
assume
A1: A is boundary;
let C be Subset of X;
assume A` c= C;
then
A2: C` c= A`` by SUBSET_1:12;
assume C is closed;
then C` = {}X by A1,A2,TOPS_1:50;
hence thesis by Th2;
end;
assume
A3: for C being Subset of X st A` c= C & C is closed holds C = the
carrier of X;
now
let G be Subset of X;
assume that
A4: G c= A and
A5: G is open;
A` c= G` by A4,SUBSET_1:12;
then G` = the carrier of X by A3,A5;
hence G = {} by Th1;
end;
hence thesis by TOPS_1:50;
end;
theorem
A is boundary iff for G being Subset of X st G <> {} & G is open holds
( A`) meets G
proof
thus A is boundary implies for G being Subset of X st G <> {} & G is open
holds ( A`) meets G
by SUBSET_1:24,TOPS_1:50;
assume
A1: for G being Subset of X st G <> {} & G is open holds ( A`) meets G;
assume Int A <> {};
then Int A c= A & ( A`) meets Int A by A1,TOPS_1:16;
hence contradiction by SUBSET_1:24;
end;
theorem
A is boundary iff for F being Subset of X holds F is closed implies
Int F = Int(F \/ A)
proof
thus A is boundary implies for F being Subset of X holds F is closed implies
Int F = Int(F \/ A)
proof
assume
A1: Int A = {};
let F be Subset of X;
assume F is closed;
then Int(F \/ A) = Int(F \/ Int A) by Th6;
hence thesis by A1;
end;
assume
for F being Subset of X holds F is closed implies Int F = Int(F \/ A );
then Int {}X = Int({}X \/ A);
hence thesis;
end;
theorem
A is boundary implies A /\ B is boundary by Th11,XBOOLE_1:17;
definition
let X be TopStruct, A be Subset of X;
redefine attr A is dense means
Cl A = the carrier of X;
compatibility
proof
thus A is dense implies Cl A = the carrier of X
proof
assume A is dense;
then Cl A = [#]X by TOPS_1:def 3;
hence thesis;
end;
assume Cl A = the carrier of X;
then Cl A = [#]X;
hence thesis by TOPS_1:def 3;
end;
end;
theorem
[#]X is dense;
reserve X for non empty TopSpace,
A, B for Subset of X;
theorem Th17:
A is dense implies A <> {}
proof
assume A is dense;
then
A1: Cl A = [#]X;
assume A = {};
hence contradiction by A1,PRE_TOPC:22;
end;
theorem Th18:
A is dense iff A` is boundary
proof
thus A is dense implies A` is boundary
proof
assume A is dense;
then ( A``) is dense;
hence thesis by TOPS_1:def 4;
end;
assume A` is boundary;
then ( A``) is dense by TOPS_1:def 4;
hence thesis;
end;
theorem
A is dense iff for C being Subset of X st A c= C & C is closed holds C
= the carrier of X
by TOPS_1:5,PRE_TOPC:18;
theorem
A is dense iff for G being Subset of X holds G is open implies Cl G =
Cl(G /\ A)
proof
thus A is dense implies for G being Subset of X holds G is open implies Cl G
= Cl(G /\ A)
proof
assume
A1: A is dense;
let G be Subset of X;
assume G is open;
then
A2: Cl(G /\ Cl A) = Cl(G /\ A) by TOPS_1:14;
G /\ [#]X = G by XBOOLE_1:28;
hence thesis by A1,A2;
end;
assume for G being Subset of X holds G is open implies Cl G = Cl(G /\ A);
then Cl [#]X = Cl([#]X /\ A);
then
A3: [#]X = Cl([#]X /\ A) by TOPS_1:2;
[#]X /\ A = A by XBOOLE_1:28;
hence thesis by A3;
end;
theorem
A is dense implies A \/ B is dense by TOPS_1:44,XBOOLE_1:7;
definition
let X be TopStruct, A be Subset of X;
redefine attr A is nowhere_dense means
Int(Cl A) = {};
compatibility
by Def1,TOPS_1:def 5;
end;
theorem
{}X is nowhere_dense;
theorem
A is nowhere_dense implies A <> the carrier of X by Th10;
theorem
A is nowhere_dense implies Cl A is nowhere_dense;
theorem
A is nowhere_dense implies A is not dense
proof
assume
A1: Int Cl A = {};
assume A is dense;
then Cl A = [#]X;
hence contradiction by A1,TOPS_1:15;
end;
theorem Th26:
B is nowhere_dense & A c= B implies A is nowhere_dense
proof
assume B is nowhere_dense;
then
A1: Cl B is boundary;
assume A c= B;
then Cl A is boundary by A1,Th11,PRE_TOPC:19;
hence thesis;
end;
theorem Th27:
A is nowhere_dense iff ex C being Subset of X st A c= C & C is
closed & C is boundary
proof
thus A is nowhere_dense implies ex C being Subset of X st A c= C & C is
closed & C is boundary
proof
assume
A1: A is nowhere_dense;
take Cl A;
thus thesis by A1,PRE_TOPC:18;
end;
given C being Subset of X such that
A2: A c= C & C is closed & C is boundary;
Cl A is boundary by A2,Th11,TOPS_1:5;
hence thesis;
end;
theorem Th28:
A is nowhere_dense iff for G being Subset of X st G <> {} & G is
open ex H being Subset of X st H c= G & H <> {} & H is open & A misses H
proof
thus A is nowhere_dense implies for G being Subset of X st G <> {} & G is
open ex H being Subset of X st H c= G & H <> {} & H is open & A misses H
proof
assume A is nowhere_dense;
then
A1: Cl A is boundary;
let G be Subset of X;
assume G <> {} & G is open;
then consider H being Subset of X such that
A2: H c= G & H <> {} & H is open & Cl A misses H by A1,TOPS_1:51;
take H;
thus thesis by A2,PRE_TOPC:18,XBOOLE_1:63;
end;
assume
A3: for G being Subset of X st G <> {} & G is open ex H being Subset of
X st H c= G & H <> {} & H is open & A misses H;
for G being Subset of X st G <> {} & G is open ex H being Subset of X st
H c= G & H <> {} & H is open & Cl A misses H
proof
let G be Subset of X;
assume G <> {} & G is open;
then consider H being Subset of X such that
A4: H c= G & H <> {} & H is open & A misses H by A3;
take H;
thus thesis by A4,TSEP_1:36;
end;
then Cl A is boundary by TOPS_1:51;
hence thesis;
end;
theorem
A is nowhere_dense implies A /\ B is nowhere_dense by Th26,XBOOLE_1:17;
theorem Th30:
A is nowhere_dense & B is boundary implies A \/ B is boundary
proof
assume A is nowhere_dense;
then
A1: Cl A is boundary;
assume B is boundary;
then A c= Cl A & B \/ Cl A is boundary by A1,PRE_TOPC:18,TOPS_1:49;
hence thesis by Th11,XBOOLE_1:9;
end;
definition
let X be TopStruct, A be Subset of X;
attr A is everywhere_dense means
Cl(Int A) = [#]X;
end;
definition
let X be TopStruct, A be Subset of X;
redefine attr A is everywhere_dense means
Cl(Int A) = the carrier of X;
compatibility;
end;
theorem
[#]X is everywhere_dense
proof
Int [#]X = [#]X by TOPS_1:15;
then Cl Int [#]X = [#]X by TOPS_1:2;
hence thesis;
end;
theorem
A is everywhere_dense implies Int A is everywhere_dense;
theorem Th33:
A is everywhere_dense implies A is dense
proof
assume A is everywhere_dense;
then Cl Int A = [#] X;
then [#]X c= Cl A by PRE_TOPC:19,TOPS_1:16;
then Cl A = [#]X;
hence thesis;
end;
theorem
A is everywhere_dense implies A <> {} by Th17,Th33;
theorem
A is everywhere_dense iff Int A is dense;
theorem Th36:
A is open & A is dense implies A is everywhere_dense
by TOPS_1:23;
theorem
A is everywhere_dense implies A is not boundary
by PRE_TOPC:22;
theorem Th38:
A is everywhere_dense & A c= B implies B is everywhere_dense
proof
assume A is everywhere_dense;
then
A1: Cl Int A = [#]X;
assume A c= B;
then Int A c= Int B by TOPS_1:19;
then Cl Int A c= Cl Int B by PRE_TOPC:19;
then [#]X = Cl Int B by A1;
hence thesis;
end;
theorem Th39:
A is everywhere_dense iff A` is nowhere_dense
proof
thus A is everywhere_dense implies A` is nowhere_dense
proof
assume A is everywhere_dense;
then Cl Int A = [#]X;
then (Cl Int A)` = {}X by Th2;
then Int (Int A)` = {}X by TDLAT_3:3;
then Int Cl A` = {} by TDLAT_3:2;
then Cl A` is boundary;
hence thesis;
end;
assume A` is nowhere_dense;
then Cl A` is boundary;
then Int Cl A` = {}X;
then Int (Int A)` = {}X by TDLAT_3:2;
then (Cl Int A)` = {}X by TDLAT_3:3;
then Cl Int A = [#]X by Th2;
hence thesis;
end;
theorem Th40:
A is nowhere_dense iff A` is everywhere_dense
proof
thus A is nowhere_dense implies A` is everywhere_dense
proof
assume A is nowhere_dense;
then Cl A is boundary;
then Int Cl A = {}X;
then Int (Int A`)` = {}X by TDLAT_3:1;
then (Cl Int A`)` = {}X by TDLAT_3:3;
then Cl Int A` = [#]X by Th2;
hence thesis;
end;
assume A` is everywhere_dense;
then Cl Int A` = [#]X;
then (Cl Int A`)` = {}X by Th2;
then Int (Int A`)` = {}X by TDLAT_3:3;
then Int Cl A = {} by TDLAT_3:1;
then Cl A is boundary;
hence thesis;
end;
theorem Th41:
A is everywhere_dense iff ex C being Subset of X st C c= A & C
is open & C is dense
proof
thus A is everywhere_dense implies ex C being Subset of X st C c= A & C is
open & C is dense
proof
assume
A1: A is everywhere_dense;
take Int A;
thus thesis by A1,TOPS_1:16;
end;
given C being Subset of X such that
A2: C c= A & C is open & C is dense;
Int A is dense by A2,TOPS_1:24,44;
hence thesis;
end;
theorem
A is everywhere_dense iff for F being Subset of X st F <> the carrier
of X & F is closed ex H being Subset of X st F c= H & H <> the carrier of X & H
is closed & A \/ H = the carrier of X
proof
thus A is everywhere_dense implies for F being Subset of X st F <> the
carrier of X & F is closed ex H being Subset of X st F c= H & H <> the carrier
of X & H is closed & A \/ H = the carrier of X
proof
assume A is everywhere_dense;
then
A1: A` is nowhere_dense by Th39;
let F be Subset of X;
assume F <> the carrier of X;
then
A2: [#]X \ F <> {} by PRE_TOPC:4;
assume F is closed;
then consider G being Subset of X such that
A3: G c= F` and
A4: G <> {} and
A5: G is open and
A6: ( A`) misses G by A1,A2,Th28;
take H = G`;
F`` c= H by A3,SUBSET_1:12;
hence F c= H;
H` <> {} by A4;
then [#]X \ H <> {};
hence H <> the carrier of X by PRE_TOPC:4;
thus H is closed by A5;
( A`) /\ H` = {} by A6;
then (A \/ H)` = {}X by XBOOLE_1:53;
hence thesis by Th2;
end;
assume
A7: for F being Subset of X st F <> the carrier of X & F is closed ex H
being Subset of X st F c= H & H <> the carrier of X & H is closed & A \/ H =
the carrier of X;
for G being Subset of X st G <> {} & G is open ex H being Subset of X
st H c= G & H <> {} & H is open & ( A`) misses H
proof
let G be Subset of X;
assume G <> {};
then G`` <> {};
then
A8: G` <> [#]X by PRE_TOPC:4;
assume G is open;
then consider F being Subset of X such that
A9: G` c= F and
A10: F <> the carrier of X and
A11: F is closed and
A12: A \/ F = the carrier of X by A7,A8;
take H = F`;
H c= G`` by A9,SUBSET_1:12;
hence H c= G;
F <> [#]X by A10;
hence H <> {} by PRE_TOPC:4;
thus H is open by A11;
(A \/ F)` = {}X by A12,Th2;
hence ( A`) /\ H = {} by XBOOLE_1:53;
end;
then A` is nowhere_dense by Th28;
hence thesis by Th39;
end;
theorem
A is everywhere_dense implies A \/ B is everywhere_dense by Th38,XBOOLE_1:7;
theorem Th44:
A is everywhere_dense & B is everywhere_dense implies A /\ B is
everywhere_dense
proof
assume A is everywhere_dense & B is everywhere_dense;
then A` is nowhere_dense & B` is nowhere_dense by Th39;
then A` \/ B` = (A /\ B)` & A` \/ B` is nowhere_dense by TOPS_1:53
,XBOOLE_1:54;
hence thesis by Th39;
end;
theorem Th45:
A is everywhere_dense & B is dense implies A /\ B is dense
proof
assume A is everywhere_dense;
then
A1: A` is nowhere_dense by Th39;
assume B is dense;
then B` is boundary by Th18;
then A` \/ B` = (A /\ B)` & A` \/ B` is boundary by A1,Th30,XBOOLE_1:54;
hence thesis by Th18;
end;
theorem
A is dense & B is nowhere_dense implies A \ B is dense
proof
assume
A1: A is dense;
A2: A \ B = B` /\ A by SUBSET_1:13;
assume B is nowhere_dense;
then B` is everywhere_dense by Th40;
hence thesis by A1,A2,Th45;
end;
theorem
A is everywhere_dense & B is boundary implies A \ B is dense
proof
assume
A1: A is everywhere_dense;
A2: A \ B = A /\ B` by SUBSET_1:13;
assume B is boundary;
then B` is dense by TOPS_1:def 4;
hence thesis by A1,A2,Th45;
end;
theorem
A is everywhere_dense & B is nowhere_dense implies A \ B is everywhere_dense
proof
assume
A1: A is everywhere_dense;
A2: A \ B = A /\ B` by SUBSET_1:13;
assume B is nowhere_dense;
then B` is everywhere_dense by Th40;
hence thesis by A1,A2,Th44;
end;
reserve D for Subset of X;
theorem
D is everywhere_dense implies ex C,B being Subset of X st C is open &
C is dense & B is nowhere_dense & C \/ B = D & C misses B
proof
assume D is everywhere_dense;
then consider C being Subset of X such that
A1: C c= D and
A2: C is open & C is dense by Th41;
take C;
take B = D \ C;
thus C is open & C is dense by A2;
C is everywhere_dense by A2,Th36;
then C` is nowhere_dense by Th39;
hence B is nowhere_dense by Th26,XBOOLE_1:33;
thus thesis by A1,XBOOLE_1:45,79;
end;
theorem
D is everywhere_dense implies ex C,B being Subset of X st C is open &
C is dense & B is closed & B is boundary & C \/ (D /\ B) = D & C misses B & C
\/ B = the carrier of X
proof
assume D is everywhere_dense;
then consider C being Subset of X such that
A1: C c= D and
A2: C is open & C is dense by Th41;
take C;
take B = C`;
thus C is open & C is dense & B is closed & B is boundary by A2,Th18;
thus C \/ (D /\ B) = (C \/ D) /\ (C \/ C`) by XBOOLE_1:24
.= (C \/ D) /\ [#]X by PRE_TOPC:2
.= C \/ D by XBOOLE_1:28
.= D by A1,XBOOLE_1:12;
C misses B by XBOOLE_1:79;
hence C /\ B = {};
C \/ B = [#]X by PRE_TOPC:2;
hence thesis;
end;
theorem
D is nowhere_dense implies ex C,B being Subset of X st C is closed & C
is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X
proof
assume D is nowhere_dense;
then consider C being Subset of X such that
A1: D c= C and
A2: C is closed & C is boundary by Th27;
take C;
take B = D \/ C`;
thus C is closed & C is boundary by A2;
C` is everywhere_dense by A2,Th40;
hence B is everywhere_dense by Th38,XBOOLE_1:7;
A3: C misses C` by XBOOLE_1:79;
thus C /\ B = (C /\ D) \/ (C /\ C`) by XBOOLE_1:23
.= (C /\ D) \/ {}X by A3
.= D by A1,XBOOLE_1:28;
thus C \/ B = D \/ (C \/ C`) by XBOOLE_1:4
.= D \/ [#]X by PRE_TOPC:2
.= the carrier of X by XBOOLE_1:12;
end;
theorem
D is nowhere_dense implies ex C,B being Subset of X st C is closed & C
is boundary & B is open & B is dense & C /\ (D \/ B) = D & C misses B & C \/ B
= the carrier of X
proof
assume D is nowhere_dense;
then consider C being Subset of X such that
A1: D c= C and
A2: C is closed & C is boundary by Th27;
take C;
take B = C`;
thus C is closed & C is boundary & B is open & B is dense by A2;
A3: C misses C` by XBOOLE_1:79;
thus C /\ (D \/ B) = (C /\ D) \/ (C /\ C`) by XBOOLE_1:23
.= (C /\ D) \/ {}X by A3
.= D by A1,XBOOLE_1:28;
C misses B by XBOOLE_1:79;
hence C /\ B = {};
C \/ B = [#]X by PRE_TOPC:2;
hence thesis;
end;
begin
:: 3. Properties of Subsets in Subspaces.
reserve Y0 for SubSpace of X;
theorem Th53:
for A being Subset of X, B being Subset of Y0 st B c= A holds Cl B c= Cl A
proof
let A be Subset of X, B be Subset of Y0;
assume
A1: B c= A;
then reconsider D = B as Subset of X by XBOOLE_1:1;
Cl B = (Cl D) /\ [#]Y0 by PRE_TOPC:17;
then
A2: Cl B c= Cl D by XBOOLE_1:17;
Cl D c= Cl A by A1,PRE_TOPC:19;
hence thesis by A2,XBOOLE_1:1;
end;
theorem Th54:
for C, A being Subset of X, B being Subset of Y0 st C is closed
& C c= the carrier of Y0 & A c= C & A = B holds Cl A = Cl B
proof
let C, A be Subset of X, B be Subset of Y0;
assume
A1: C is closed;
assume
A2: C c= the carrier of Y0;
assume A c= C;
then Cl A c= Cl C by PRE_TOPC:19;
then Cl A c= C by A1,PRE_TOPC:22;
then
A3: Cl A = (Cl A) /\ [#]Y0 by A2,XBOOLE_1:1,28;
assume A = B;
hence thesis by A3,PRE_TOPC:17;
end;
theorem
for Y0 being closed non empty SubSpace of X for A being Subset of X, B
being Subset of Y0 st A = B holds Cl A = Cl B
proof
let Y0 be closed non empty SubSpace of X;
reconsider C = the carrier of Y0 as Subset of X by TSEP_1:1;
let A be Subset of X, B be Subset of Y0;
A1: C is closed by TSEP_1:11;
assume A = B;
hence thesis by A1,Th54;
end;
theorem Th56:
for A being Subset of X, B being Subset of Y0 st A c= B holds Int A c= Int B
proof
let A be Subset of X, B be Subset of Y0;
A1: Int A c= A by TOPS_1:16;
assume A c= B;
then
A2: Int A c= B by A1,XBOOLE_1:1;
then reconsider C = Int A as Subset of Y0 by XBOOLE_1:1;
C is open by TOPS_2:25;
hence thesis by A2,TOPS_1:24;
end;
theorem Th57:
for Y0 being non empty SubSpace of X, C, A being Subset of X, B
being Subset of Y0 st C is open & C c= the carrier of Y0 & A c= C & A = B holds
Int A = Int B
proof
let Y0 be non empty SubSpace of X, C, A be Subset of X, B be Subset of Y0;
assume
A1: C is open;
assume
A2: C c= the carrier of Y0;
assume
A3: A c= C;
assume
A4: A = B;
A5: Int B c= B by TOPS_1:16;
then reconsider D = Int B as Subset of X by A4,XBOOLE_1:1;
Int B c= C by A3,A4,A5,XBOOLE_1:1;
then D is open by A1,A2,TSEP_1:9;
then
A6: D c= Int A by A4,TOPS_1:16,24;
Int A c= Int B by A4,Th56;
hence thesis by A6;
end;
theorem
for Y0 being open non empty SubSpace of X for A being Subset of X, B
being Subset of Y0 st A = B holds Int A = Int B
proof
let Y0 be open non empty SubSpace of X;
reconsider C = the carrier of Y0 as Subset of X by TSEP_1:1;
let A be Subset of X, B be Subset of Y0;
A1: C is open by TSEP_1:16;
assume A = B;
hence thesis by A1,Th57;
end;
reserve X0 for SubSpace of X;
theorem Th59:
for A being Subset of X, B being Subset of X0 st A c= B holds A
is dense implies B is dense
proof
let A be Subset of X, B be Subset of X0;
A1: [#]X0 c= [#]X by PRE_TOPC:def 4;
assume
A2: A c= B;
then reconsider C = A as Subset of X0 by XBOOLE_1:1;
assume A is dense;
then Cl A = [#]X;
then [#]X0 = (Cl A) /\ [#]X0 by A1,XBOOLE_1:28;
then Cl C = [#]X0 by PRE_TOPC:17;
then C is dense;
hence thesis by A2,TOPS_1:44;
end;
theorem Th60:
for C, A being Subset of X, B being Subset of X0 st C c= the
carrier of X0 & A c= C & A = B holds C is dense & B is dense iff A is dense
proof
let C, A be Subset of X, B be Subset of X0;
assume
A1: C c= the carrier of X0;
reconsider P = the carrier of X0 as Subset of X by TSEP_1:1;
assume
A2: A c= C;
assume
A3: A = B;
thus C is dense & B is dense implies A is dense
proof
assume C is dense;
then Cl C = [#]X;
then
A4: [#]X c= Cl P by A1,PRE_TOPC:19;
assume B is dense;
then Cl B = [#]X0;
then P = (Cl A) /\ [#]X0 by A3,PRE_TOPC:17;
then Cl P c= Cl Cl A by PRE_TOPC:19,XBOOLE_1:17;
then [#]X c= Cl A by A4,XBOOLE_1:1;
then Cl A = [#]X;
hence thesis;
end;
thus thesis by A2,A3,Th59,TOPS_1:44;
end;
reserve X0 for non empty SubSpace of X;
theorem Th61:
for A being Subset of X, B being Subset of X0 st A c= B holds A
is everywhere_dense implies B is everywhere_dense
proof
let A be Subset of X, B be Subset of X0;
assume
A1: A c= B;
then reconsider C = A as Subset of X0 by XBOOLE_1:1;
assume A is everywhere_dense;
then Int A is dense;
then Int C is dense by Th56,Th59;
then Int B is dense by A1,TOPS_1:19,44;
hence thesis;
end;
theorem Th62:
for C, A being Subset of X, B being Subset of X0 st C is open &
C c= the carrier of X0 & A c= C & A = B holds C is dense & B is
everywhere_dense iff A is everywhere_dense
proof
let C, A be Subset of X, B be Subset of X0;
assume
A1: C is open;
assume C c= the carrier of X0;
then reconsider E = C as Subset of X0;
A2: E is open by A1,TOPS_2:25;
assume
A3: A c= C;
assume
A4: A = B;
A5: Int B c= B by TOPS_1:16;
then reconsider D = Int B as Subset of X by A4,XBOOLE_1:1;
Int B c= Int E by A3,A4,TOPS_1:19;
then
A6: Int B c= E by A2,TOPS_1:23;
then
A7: D is open by A1,TSEP_1:9;
thus C is dense & B is everywhere_dense implies A is everywhere_dense
proof
assume
A8: C is dense;
assume B is everywhere_dense;
then Int B is dense;
then D is dense by A6,A8,Th60;
then Int A is dense by A4,A5,A7,TOPS_1:24,44;
hence thesis;
end;
thus A is everywhere_dense implies C is dense & B is everywhere_dense
by A3,Th33,Th38,A4,Th61;
end;
theorem
for X0 being open non empty SubSpace of X for A,C being Subset of X, B
being Subset of X0 st C = the carrier of X0 & A = B holds C is dense & B is
everywhere_dense iff A is everywhere_dense
proof
let X0 be open non empty SubSpace of X;
let A,C be Subset of X, B be Subset of X0;
assume
A1: C = the carrier of X0;
assume
A2: A = B;
C is open by A1,TSEP_1:def 1;
hence thesis by A1,A2,Th62;
end;
theorem
for C, A being Subset of X, B being Subset of X0 st C c= the carrier
of X0 & A c= C & A = B holds C is everywhere_dense & B is everywhere_dense iff
A is everywhere_dense
proof
let C, A be Subset of X, B be Subset of X0;
assume
A1: C c= the carrier of X0;
assume
A2: A c= C;
assume
A3: A = B;
thus C is everywhere_dense & B is everywhere_dense implies A is
everywhere_dense
proof
Int C c= C by TOPS_1:16;
then reconsider D = Int C as Subset of X0 by A1,XBOOLE_1:1;
A4: D /\ B c= Int C by XBOOLE_1:17;
then reconsider E = D /\ B as Subset of X by XBOOLE_1:1;
assume
A5: C is everywhere_dense;
then Int C is everywhere_dense;
then
A6: D is everywhere_dense by Th61;
assume B is everywhere_dense;
then
A7: D /\ B is everywhere_dense by A6,Th44;
Int C is dense by A5;
then E is everywhere_dense by A7,A4,Th62;
hence thesis by A3,Th38,XBOOLE_1:17;
end;
thus thesis by A2,A3,Th38,Th61;
end;
theorem Th65:
for A being Subset of X, B being Subset of X0 st A c= B holds B
is boundary implies A is boundary
by XBOOLE_1:3,Th56;
theorem Th66:
for C, A being Subset of X, B being Subset of X0 st C is open &
C c= the carrier of X0 & A c= C & A = B holds A is boundary implies B is
boundary
by Th57;
theorem
for X0 being open non empty SubSpace of X for A being Subset of X, B
being Subset of X0 st A = B holds A is boundary iff B is boundary
proof
let X0 be open non empty SubSpace of X;
let A be Subset of X, B be Subset of X0;
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
A1: C is open by TSEP_1:def 1;
assume A = B;
hence thesis by A1,Th65,Th66;
end;
theorem Th68:
for A being Subset of X, B being Subset of X0 st A c= B holds B
is nowhere_dense implies A is nowhere_dense
proof
let A be Subset of X, B be Subset of X0;
reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;
reconsider G = (Int Cl A) /\ [#]X0 as Subset of X0;
assume
A1: A c= B;
then reconsider C = A as Subset of X0 by XBOOLE_1:1;
assume B is nowhere_dense;
then C is nowhere_dense by A1,Th26;
then
A2: G is open & Int Cl C = {} by TOPS_2:24;
(Int Cl A) /\ [#]X0 c= (Cl A) /\ [#]X0 by TOPS_1:16,XBOOLE_1:26;
then
A3: (Int Cl A) /\ [#]X0 c= Cl C by PRE_TOPC:17;
now
assume Int Cl A <> {};
then A meets Int Cl A by Th7;
then
A4: A /\ Int Cl A <> {};
C c= D;
then (Int Cl A) /\ D <> {} by A4,XBOOLE_1:3,26;
hence contradiction by A3,A2,TOPS_1:24,XBOOLE_1:3;
end;
hence thesis;
end;
Lm1: for C, A being Subset of X, B being Subset of X0 st C is open & C = the
carrier of X0 & A = B holds A is nowhere_dense implies B is nowhere_dense
proof
let C, A be Subset of X, B be Subset of X0;
assume
A1: C is open;
assume
A2: C = the carrier of X0;
assume A = B;
then
A3: Cl B c= Cl A by Th53;
then reconsider D = Cl B as Subset of X by XBOOLE_1:1;
assume A is nowhere_dense;
then
A4: Int Cl A = {};
Int D = Int Cl B by A1,A2,Th57;
then Int Cl B = {} by A3,A4,TOPS_1:19,XBOOLE_1:3;
hence thesis;
end;
theorem Th69:
for C, A being Subset of X, B being Subset of X0 st C is open &
C c= the carrier of X0 & A c= C & A = B holds A is nowhere_dense implies B is
nowhere_dense
proof
let C, A be Subset of X, B be Subset of X0;
assume
A1: C is open;
assume
A2: C c= the carrier of X0;
assume that
A3: A c= C and
A4: A = B;
assume
A5: A is nowhere_dense;
A6: now
assume C <> {};
then consider X1 being strict non empty SubSpace of X such that
A7: C = the carrier of X1 by TSEP_1:10;
reconsider E = B as Subset of X1 by A3,A4,A7;
E is nowhere_dense & X1 is SubSpace of X0 by A1,A2,A4,A5,A7,Lm1,TSEP_1:4;
hence thesis by Th68;
end;
now
assume C = {};
then B = {}X0 by A3,A4,XBOOLE_1:3;
hence thesis;
end;
hence thesis by A6;
end;
theorem
for X0 being open non empty SubSpace of X for A being Subset of X, B
being Subset of X0 st A = B holds A is nowhere_dense iff B is nowhere_dense
proof
let X0 be open non empty SubSpace of X;
let A be Subset of X, B be Subset of X0;
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
A1: C is open by TSEP_1:def 1;
assume A = B;
hence thesis by A1,Th68,Th69;
end;
begin
:: 4. Subsets in Topological Spaces with the same Topological Structures.
theorem
for X1, X2 being 1-sorted holds the carrier of X1 = the carrier of X2
implies for C1 being Subset of X1, C2 being Subset of X2 holds C1 = C2 iff C1`
= C2`
proof
let X1, X2 be 1-sorted;
assume
A1: the carrier of X1 = the carrier of X2;
let C1 be Subset of X1, C2 be Subset of X2;
thus C1 = C2 implies C1` = C2` by A1;
thus C1` = C2` implies C1 = C2
proof
assume C1` = C2`;
hence C1 = [#]X2 \ C2` by A1,PRE_TOPC:3
.= C2 by PRE_TOPC:3;
end;
end;
reserve X1,X2 for TopStruct;
theorem Th72:
the carrier of X1 = the carrier of X2 & (for C1 being Subset of
X1, C2 being Subset of X2 st C1 = C2 holds (C1 is open iff C2 is open)) implies
the TopStruct of X1 = the TopStruct of X2
proof
assume
A1: the carrier of X1 = the carrier of X2;
assume
A2: for C1 being Subset of X1, C2 being Subset of X2 st C1 = C2 holds (
C1 is open iff C2 is open);
now
let D be object;
assume
A3: D in the topology of X2;
then reconsider C2 = D as Subset of X2;
reconsider C1 = C2 as Subset of X1 by A1;
C2 is open by A3;
then C1 is open by A2;
hence D in the topology of X1;
end;
then
A4: the topology of X2 c= the topology of X1 by TARSKI:def 3;
now
let D be object;
assume
A5: D in the topology of X1;
then reconsider C1 = D as Subset of X1;
reconsider C2 = C1 as Subset of X2 by A1;
C1 is open by A5;
then C2 is open by A2;
hence D in the topology of X2;
end;
then the topology of X1 c= the topology of X2 by TARSKI:def 3;
hence thesis by A1,A4,XBOOLE_0:def 10;
end;
theorem Th73:
the carrier of X1 = the carrier of X2 & (for C1 being Subset of
X1, C2 being Subset of X2 st C1 = C2 holds (C1 is closed iff C2 is closed))
implies the TopStruct of X1 = the TopStruct of X2
proof
assume
A1: the carrier of X1 = the carrier of X2;
assume
A2: for C1 being Subset of X1, C2 being Subset of X2 st C1 = C2 holds (
C1 is closed iff C2 is closed);
now
let C1 be Subset of X1, C2 be Subset of X2;
assume
A3: C1 = C2;
thus C1 is open implies C2 is open
proof
assume C1 is open;
then C1` is closed by TOPS_1:4;
then C2` is closed by A1,A2,A3;
hence thesis by TOPS_1:4;
end;
thus C2 is open implies C1 is open
proof
assume C2 is open;
then C2` is closed by TOPS_1:4;
then C1` is closed by A1,A2,A3;
hence thesis by TOPS_1:4;
end;
end;
hence thesis by A1,Th72;
end;
reserve X1,X2 for TopSpace;
theorem
the carrier of X1 = the carrier of X2 & (for C1 being Subset of X1, C2
being Subset of X2 st C1 = C2 holds Int C1 = Int C2) implies the TopStruct of
X1 = the TopStruct of X2
proof
assume
A1: the carrier of X1 = the carrier of X2;
assume
A2: for C1 being Subset of X1, C2 being Subset of X2 st C1 = C2 holds
Int C1 = Int C2;
now
let C1 be Subset of X1, C2 be Subset of X2;
assume
A3: C1 = C2;
thus C1 is open implies C2 is open
proof
assume C1 is open;
then C1 = Int C1 by TOPS_1:23;
then C2 = Int C2 by A2,A3;
hence thesis;
end;
thus C2 is open implies C1 is open
proof
assume C2 is open;
then C2 = Int C2 by TOPS_1:23;
then C1 = Int C1 by A2,A3;
hence thesis;
end;
end;
hence thesis by A1,Th72;
end;
theorem
the carrier of X1 = the carrier of X2 & (for C1 being Subset of X1, C2
being Subset of X2 st C1 = C2 holds Cl C1 = Cl C2) implies the TopStruct of X1
= the TopStruct of X2
proof
assume
A1: the carrier of X1 = the carrier of X2;
assume
A2: for C1 being Subset of X1, C2 being Subset of X2 st C1 = C2 holds Cl
C1 = Cl C2;
now
let C1 be Subset of X1, C2 be Subset of X2;
assume
A3: C1 = C2;
thus C1 is closed implies C2 is closed
proof
assume C1 is closed;
then C1 = Cl C1 by PRE_TOPC:22;
then C2 = Cl C2 by A2,A3;
hence thesis;
end;
thus C2 is closed implies C1 is closed
proof
assume C2 is closed;
then C2 = Cl C2 by PRE_TOPC:22;
then C1 = Cl C1 by A2,A3;
hence thesis;
end;
end;
hence thesis by A1,Th73;
end;
reserve D1 for Subset of X1,
D2 for Subset of X2;
theorem Th76:
D1 = D2 & the TopStruct of X1 = the TopStruct of X2 implies (D1
is open implies D2 is open);
theorem Th77:
D1 = D2 & the TopStruct of X1 = the TopStruct of X2 implies Int D1 = Int D2
proof
assume
A1: D1 = D2;
A2: Int D1 c= D1 by TOPS_1:16;
then reconsider C2 = Int D1 as Subset of X2 by A1,XBOOLE_1:1;
assume
A3: the TopStruct of X1 = the TopStruct of X2;
then
A4: C2 c= Int D2 by A1,A2,Th76,TOPS_1:24;
A5: Int D2 c= D2 by TOPS_1:16;
then reconsider C1 = Int D2 as Subset of X1 by A1,XBOOLE_1:1;
C1 c= Int D1 by A1,A3,A5,Th76,TOPS_1:24;
hence thesis by A4;
end;
theorem Th78:
D1 c= D2 & the TopStruct of X1 = the TopStruct of X2 implies Int D1 c= Int D2
proof
assume
A1: D1 c= D2;
then reconsider C2 = D1 as Subset of X2 by XBOOLE_1:1;
assume the TopStruct of X1 = the TopStruct of X2;
then Int D1 = Int C2 by Th77;
hence thesis by A1,TOPS_1:19;
end;
theorem Th79:
D1 = D2 & the TopStruct of X1 = the TopStruct of X2 implies (D1
is closed implies D2 is closed)
by Th76;
theorem Th80:
D1 = D2 & the TopStruct of X1 = the TopStruct of X2 implies Cl D1 = Cl D2
proof
assume
A1: D1 = D2;
assume
A2: the TopStruct of X1 = the TopStruct of X2;
then reconsider C2 = Cl D1 as Subset of X2;
D1 c= Cl D1 by PRE_TOPC:18;
then
A3: Cl D2 c= C2 by A1,A2,Th79,TOPS_1:5;
reconsider C1 = Cl D2 as Subset of X1 by A2;
D2 c= Cl D2 by PRE_TOPC:18;
then Cl D1 c= C1 by A1,A2,Th79,TOPS_1:5;
hence thesis by A3;
end;
theorem Th81:
D1 c= D2 & the TopStruct of X1 = the TopStruct of X2 implies Cl D1 c= Cl D2
proof
assume
A1: D1 c= D2;
assume
A2: the TopStruct of X1 = the TopStruct of X2;
then reconsider C2 = D1 as Subset of X2;
Cl D1 = Cl C2 by A2,Th80;
hence thesis by A1,PRE_TOPC:19;
end;
theorem Th82:
D2 c= D1 & the TopStruct of X1 = the TopStruct of X2 implies (D1
is boundary implies D2 is boundary)
proof
assume
A1: D2 c= D1;
then reconsider C1 = D2 as Subset of X1 by XBOOLE_1:1;
assume
A2: the TopStruct of X1 = the TopStruct of X2;
assume D1 is boundary;
then C1 is boundary by A1,Th11;
then
A3: Int C1 = {};
Int C1 = Int D2 by A2,Th77;
hence thesis by A3;
end;
theorem Th83:
D1 c= D2 & the TopStruct of X1 = the TopStruct of X2 implies (D1
is dense implies D2 is dense)
proof
assume
A1: D1 c= D2;
then reconsider C2 = D1 as Subset of X2 by XBOOLE_1:1;
assume
A2: the TopStruct of X1 = the TopStruct of X2;
assume D1 is dense;
then
A3: Cl D1 = the carrier of X1;
Cl D1 = Cl C2 by A2,Th80;
then C2 is dense by A2,A3;
hence thesis by A1,TOPS_1:44;
end;
theorem
D2 c= D1 & the TopStruct of X1 = the TopStruct of X2 implies (D1 is
nowhere_dense implies D2 is nowhere_dense)
proof
assume
A1: D2 c= D1;
assume
A2: the TopStruct of X1 = the TopStruct of X2;
assume D1 is nowhere_dense;
then Cl D1 is boundary;
then Cl D2 is boundary by A1,A2,Th81,Th82;
hence thesis;
end;
reserve X1,X2 for non empty TopSpace;
reserve D1 for Subset of X1,
D2 for Subset of X2;
theorem
D1 c= D2 & the TopStruct of X1 = the TopStruct of X2 implies (D1 is
everywhere_dense implies D2 is everywhere_dense)
proof
assume
A1: D1 c= D2;
assume
A2: the TopStruct of X1 = the TopStruct of X2;
assume D1 is everywhere_dense;
then Int D1 is dense;
then Int D2 is dense by A1,A2,Th78,Th83;
hence thesis;
end;