:: On the Boundary and Derivative of a Set
:: by Adam Grabowski
::
:: Received November 8, 2004
:: Copyright (c) 2004-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, PRE_TOPC, SUBSET_1, STRUCT_0, CARD_3, CARD_1, TARSKI,
ORDINAL1, FINSET_1, NATTRA_1, TOPS_1, SETFAM_1, RCOMP_1, RLVECT_3,
GLIB_000, TOPMETR, NUMBERS, BORSUK_5, TOPGEN_1;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, CARD_1, ORDINAL1, NUMBERS,
CARD_3, FINSET_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, TDLAT_3,
YELLOW_8, TOPMETR, BORSUK_5, ORDERS_4;
constructors CARD_3, TOPS_1, TDLAT_3, TOPMETR, YELLOW_8, BORSUK_5, ORDERS_4,
TOPS_2;
registrations SUBSET_1, CARD_1, STRUCT_0, TOPS_1, TEX_1, TEX_4, YELLOW13,
TOPMETR;
requirements BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, SUBSET_1, STRUCT_0;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, ZFMISC_1, PRE_TOPC, TOPS_1, XBOOLE_0, XBOOLE_1, SUBSET_1,
TOPS_3, TDLAT_3, YELLOW_8, FRECHET, BORSUK_5, TOPMETR, NUMBERS, CARD_4,
ORDERS_4, CARD_3;
schemes ORDINAL1, SUBSET_1;
begin :: Preliminaries
theorem Th1:
for T being 1-sorted, A, B being Subset of T holds A meets B` iff A \ B <> {}
by SUBSET_1:13;
theorem
for T being 1-sorted holds T is countable iff card [#]T c= omega
by CARD_3:def 14,ORDERS_4:def 2;
registration
let T be finite 1-sorted;
cluster [#]T -> finite;
coherence;
end;
registration
cluster finite -> countable for 1-sorted;
coherence
proof
let T be 1-sorted;
assume T is finite;
then the carrier of T is countable by CARD_4:1;
hence thesis by ORDERS_4:def 2;
end;
end;
registration
cluster countable non empty for 1-sorted;
existence
proof
set T = the finite non empty 1-sorted;
take T;
thus thesis;
end;
cluster countable non empty for TopSpace;
existence
proof
set T = the finite non empty TopSpace;
take T;
thus thesis;
end;
end;
registration
let T be countable 1-sorted;
cluster [#]T -> countable;
coherence by ORDERS_4:def 2;
end;
registration
cluster T_1 non empty for TopSpace;
existence
proof
set T = the discrete non empty TopSpace;
take T;
thus thesis;
end;
end;
begin
theorem Th3:
for T being TopSpace, A being Subset of T holds Int A = (Cl A`)`
proof
let T be TopSpace, A be Subset of T;
Int A = (Cl A```)` by TDLAT_3:3
.= (Cl A`)`;
hence thesis;
end;
:: Collective Boundary
definition
let T be TopSpace, F be Subset-Family of T;
func Fr F -> Subset-Family of T means
:Def1:
for A being Subset of T holds A
in it iff ex B being Subset of T st A = Fr B & B in F;
existence
proof
defpred P[set] means ex W being Subset of T st $1 = Fr W & W in F;
thus ex S be Subset-Family of T st for Z being Subset of T holds Z in S
iff P[Z] from SUBSET_1:sch 3;
end;
uniqueness
proof
defpred P[object] means ex W being Subset of T st $1 = Fr W & W in F;
let H, G be Subset-Family of T;
assume that
A1: for Z being Subset of T holds Z in H iff P[Z] and
A2: for X being Subset of T holds X in G iff P[X];
now
let X be object;
assume
A3: X in G;
then reconsider X9=X as Subset of T;
P[X9] by A2,A3;
hence X in H by A1;
end;
then
A4: G c= H;
now
let Z be object;
assume Z in H;
then P[Z] by A1;
hence Z in G by A2;
end;
then H c= G;
hence thesis by A4;
end;
end;
theorem
for T being TopSpace, F being Subset-Family of T st F = {} holds Fr F = {}
proof
let T be TopSpace, F be Subset-Family of T;
assume
A1: F = {};
assume Fr F <> {};
then consider x being object such that
A2: x in Fr F by XBOOLE_0:def 1;
ex B being Subset of T st x = Fr B & B in F by A2,Def1;
hence thesis by A1;
end;
theorem
for T being TopSpace, F being Subset-Family of T, A being Subset of T
st F = { A } holds Fr F = { Fr A }
proof
let T be TopSpace, F be Subset-Family of T, A be Subset of T;
assume
A1: F = { A };
thus Fr F c= { Fr A }
proof
let x be object;
assume
A2: x in Fr F;
then reconsider B = x as Subset of T;
consider C being Subset of T such that
A3: B = Fr C and
A4: C in F by A2,Def1;
C = A by A1,A4,TARSKI:def 1;
hence thesis by A3,TARSKI:def 1;
end;
let x be object;
assume x in { Fr A };
then
A5: x = Fr A by TARSKI:def 1;
A in F by A1,TARSKI:def 1;
hence thesis by A5,Def1;
end;
theorem Th6:
for T being TopSpace, F, G being Subset-Family of T st F c= G
holds Fr F c= Fr G
proof
let T be TopSpace, F, G be Subset-Family of T;
assume
A1: F c= G;
Fr F c= Fr G
proof
let x be object;
assume
A2: x in Fr F;
then reconsider A = x as Subset of T;
ex B being Subset of T st A = Fr B & B in F by A2,Def1;
hence thesis by A1,Def1;
end;
hence thesis;
end;
theorem
for T being TopSpace, F, G being Subset-Family of T holds Fr (F \/ G)
= Fr F \/ Fr G
proof
let T be TopSpace, F, G be Subset-Family of T;
thus Fr (F \/ G) c= Fr F \/ Fr G
proof
let x be object;
assume
A1: x in Fr (F \/ G);
then reconsider A = x as Subset of T;
consider B being Subset of T such that
A2: A = Fr B and
A3: B in F \/ G by A1,Def1;
per cases by A3,XBOOLE_0:def 3;
suppose
B in F;
then A in Fr F by A2,Def1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
B in G;
then A in Fr G by A2,Def1;
hence thesis by XBOOLE_0:def 3;
end;
end;
Fr F c= Fr (F \/ G) & Fr G c= Fr (F \/ G) by Th6,XBOOLE_1:7;
hence thesis by XBOOLE_1:8;
end;
theorem Th8: :: 1.3.0.
for T being TopStruct, A being Subset of T holds Fr A = Cl A \ Int A
proof
let T be TopStruct, A be Subset of T;
Fr A = Cl A /\ (Cl A`)`` by TOPS_1:def 2
.= Cl A \ (Cl A`)` by SUBSET_1:13
.= Cl A \ Int A by TOPS_1:def 1;
hence thesis;
end;
theorem Th9: :: 1.3.1. Characterization of Fr via basis
for T being non empty TopSpace, A being Subset of T, p being
Point of T holds p in Fr A iff for U being Subset of T st U is open & p in U
holds A meets U & U \ A <> {}
proof
let T be non empty TopSpace, A be Subset of T, p be Point of T;
hereby
assume
A1: p in Fr A;
let U be Subset of T;
assume
A2: U is open & p in U;
then U meets A` by A1,TOPS_1:28;
hence A meets U & U \ A <> {} by A1,A2,Th1,TOPS_1:28;
end;
assume
A3: for U being Subset of T st U is open & p in U holds A meets U & U \
A <> {};
for U being Subset of T st U is open & p in U holds A meets U & U meets A`
proof
let U be Subset of T;
assume
A4: U is open & p in U;
then U \ A <> {} by A3;
hence thesis by A3,A4,Th1;
end;
hence thesis by TOPS_1:28;
end;
theorem
for T being non empty TopSpace, A being Subset of T, p being Point of
T holds p in Fr A iff for B being Basis of p, U being Subset of T st U in B
holds A meets U & U \ A <> {}
proof
let T be non empty TopSpace, A be Subset of T, p be Point of T;
hereby
assume
A1: p in Fr A;
let B be Basis of p, U be Subset of T;
assume U in B;
then U is open & p in U by YELLOW_8:12;
hence A meets U & U \ A <> {} by A1,Th9;
end;
assume
A2: for B being Basis of p, U being Subset of T st U in B holds A meets
U & U \ A <> {};
for U being Subset of T st U is open & p in U holds A meets U & U meets A`
proof
set B = the Basis of p;
let U be Subset of T;
assume U is open & p in U;
then consider V being Subset of T such that
A3: V in B and
A4: V c= U by YELLOW_8:def 1;
V \ A <> {} by A2,A3;
then
A5: U \ A <> {} by A4,XBOOLE_1:3,33;
A meets V by A2,A3;
hence thesis by A4,A5,Th1,XBOOLE_1:63;
end;
hence thesis by TOPS_1:28;
end;
theorem
for T being non empty TopSpace, A being Subset of T, p being Point of
T holds p in Fr A iff ex B being Basis of p st for U being Subset of T st U in
B holds A meets U & U \ A <> {}
proof
let T be non empty TopSpace, A be Subset of T, p be Point of T;
hereby
set B = the Basis of p;
assume
A1: p in Fr A;
take B;
let U be Subset of T;
assume U in B;
then U is open & p in U by YELLOW_8:12;
hence A meets U & U \ A <> {} by A1,Th9;
end;
given B being Basis of p such that
A2: for U being Subset of T st U in B holds A meets U & U \ A <> {};
for U being Subset of T st U is open & p in U holds A meets U & U meets A`
proof
let U be Subset of T;
assume U is open & p in U;
then consider V being Subset of T such that
A3: V in B and
A4: V c= U by YELLOW_8:def 1;
V \ A <> {} by A2,A3;
then
A5: U \ A <> {} by A4,XBOOLE_1:3,33;
A meets V by A2,A3;
hence thesis by A4,A5,Th1,XBOOLE_1:63;
end;
hence thesis by TOPS_1:28;
end;
theorem :: Theorem 1.3.2. (d)
for T being TopSpace, A, B being Subset of T holds Fr (A /\ B) c= (Cl
A /\ Fr B) \/ (Fr A /\ Cl B)
proof
let T be TopSpace, A, B be Subset of T;
A1: Cl A /\ Cl B /\ ((Cl A`) \/ Cl B`) = (Cl A /\ Cl B /\ (Cl A`)) \/ (Cl A
/\ Cl B /\ Cl B`) by XBOOLE_1:23
.= (Cl A /\ Cl A` /\ Cl B) \/ (Cl A /\ Cl B /\ Cl B`) by XBOOLE_1:16
.= (Fr A /\ Cl B) \/ (Cl A /\ Cl B /\ Cl B`) by TOPS_1:def 2
.= (Fr A /\ Cl B) \/ (Cl A /\ (Cl B /\ Cl B`)) by XBOOLE_1:16
.= (Fr A /\ Cl B) \/ (Cl A /\ Fr B) by TOPS_1:def 2;
Fr (A /\ B) = Cl (A /\ B) /\ Cl (A /\ B)` by TOPS_1:def 2
.= Cl (A /\ B) /\ Cl (A` \/ B`) by XBOOLE_1:54
.= Cl (A /\ B) /\ ((Cl A`) \/ Cl B`) by PRE_TOPC:20;
hence thesis by A1,PRE_TOPC:21,XBOOLE_1:26;
end;
theorem :: Theorem 1.3.2. (f)
for T being TopSpace, A being Subset of T holds the carrier of T = Int
A \/ Fr A \/ Int A`
proof
let T be TopSpace, A be Subset of T;
Int A \/ Fr A \/ Int A` = Int A \/ Int A` \/ Fr A by XBOOLE_1:4
.= Int A \/ Int A` \/ (Cl A /\ Cl A`) by TOPS_1:def 2
.= (Int A \/ Int A` \/ Cl A) /\ (Int A \/ Int A` \/ Cl A`) by XBOOLE_1:24
.= (Int A \/ (Cl A)` \/ Cl A) /\ (Int A \/ Int A` \/ Cl A`) by TDLAT_3:3
.= (Int A \/ ((Cl A)` \/ Cl A)) /\ (Int A \/ Int A` \/ Cl A`) by XBOOLE_1:4
.= (Int A \/ [#]T) /\ (Int A \/ Int A` \/ Cl A`) by PRE_TOPC:2
.= (Int A \/ [#]T) /\ (Int A \/ Int A` \/ (Int A)`) by TDLAT_3:2
.= (Int A \/ [#]T) /\ (Int A \/ (Int A)` \/ Int A`) by XBOOLE_1:4
.= (Int A \/ [#]T) /\ ([#]T \/ Int A`) by PRE_TOPC:2
.= [#]T /\ ([#]T \/ Int A`) by XBOOLE_1:12
.= [#]T /\ [#]T by XBOOLE_1:12
.= [#]T;
hence thesis;
end;
theorem Th14: :: Theorem 1.3.2. (k)
for T being TopSpace, A being Subset of T holds A is open closed
iff Fr A = {}
proof
let T be TopSpace, A be Subset of T;
hereby
assume
A1: A is open closed;
then
A2: Int A = A by TOPS_1:23;
Fr A = A \ Int A by A1,TOPS_1:43
.= {} by A2,XBOOLE_1:37;
hence Fr A = {};
end;
assume
A3: Fr A = {};
Fr A = Cl A \ Int A by Th8;
then
A4: Cl A c= Int A by A3,XBOOLE_1:37;
A5: Int A c= A by TOPS_1:16;
then A c= Cl A & Cl A c= A by A4,PRE_TOPC:18;
then Cl A = A;
hence thesis by A4,A5,XBOOLE_0:def 10;
end;
begin :: Accumulation Points and Derivative of a Set
:: 1.3.2. Accumulation Points
definition
let T be TopStruct, A be Subset of T, x be object;
pred x is_an_accumulation_point_of A means
x in Cl (A \ {x});
end;
theorem
for T being TopSpace, A being Subset of T, x being object st x
is_an_accumulation_point_of A holds x is Point of T;
:: Derivative of a Set
definition
let T be TopStruct, A be Subset of T;
func Der A -> Subset of T means
:Def3:
for x being set st x in the carrier
of T holds x in it iff x is_an_accumulation_point_of A;
existence
proof
defpred P[set] means $1 is_an_accumulation_point_of A;
consider D being Subset of T such that
A1: for x being set holds x in D iff x in the carrier of T & P[x] from
SUBSET_1:sch 1;
take D;
thus thesis by A1;
end;
uniqueness
proof
defpred P[object] means $1 is_an_accumulation_point_of A;
let A1, A2 be Subset of T;
assume that
A2: for x being set st x in the carrier of T holds x in A1 iff P[x] and
A3: for x being set st x in the carrier of T holds x in A2 iff P[x];
A4: A2 c= A1
proof
let x be object;
assume
A5: x in A2;
then P[x] by A3;
hence thesis by A2,A5;
end;
A1 c= A2
proof
let x be object;
assume
A6: x in A1;
then P[x] by A2;
hence thesis by A3,A6;
end;
hence thesis by A4;
end;
end;
:: 1.3.3. Characterizations of a Derivative
theorem Th16:
for T being non empty TopSpace, A being Subset of T, x being object
holds x in Der A iff x is_an_accumulation_point_of A
by Def3;
theorem Th17:
for T being non empty TopSpace, A being Subset of T, x being
Point of T holds x in Der A iff for U being open Subset of T st x in U ex y
being Point of T st y in A /\ U & x <> y
proof
let T be non empty TopSpace, A be Subset of T, x be Point of T;
hereby
assume x in Der A;
then x is_an_accumulation_point_of A by Th16;
then
A1: x in Cl (A \ {x});
let U be open Subset of T;
assume x in U;
then A \ {x} meets U by A1,PRE_TOPC:24;
then consider y being object such that
A2: y in A \ {x} and
A3: y in U by XBOOLE_0:3;
reconsider y as Point of T by A2;
take y;
y in A by A2,ZFMISC_1:56;
hence y in A /\ U & x <> y by A2,A3,XBOOLE_0:def 4,ZFMISC_1:56;
end;
assume
A4: for U being open Subset of T st x in U ex y being Point of T st y in
A /\ U & x <> y;
for G being Subset of T st G is open holds x in G implies A \ {x} meets G
proof
let G be Subset of T;
assume
A5: G is open;
assume x in G;
then consider y being Point of T such that
A6: y in A /\ G and
A7: x <> y by A4,A5;
y in A by A6,XBOOLE_0:def 4;
then
A8: y in A \ {x} by A7,ZFMISC_1:56;
y in G by A6,XBOOLE_0:def 4;
hence thesis by A8,XBOOLE_0:3;
end;
then x in Cl (A \ {x}) by PRE_TOPC:24;
then x is_an_accumulation_point_of A;
hence thesis by Th16;
end;
theorem
for T being non empty TopSpace, A being Subset of T, x being Point of
T holds x in Der A iff for B being Basis of x, U being Subset of T st U in B ex
y being Point of T st y in A /\ U & x <> y
proof
let T be non empty TopSpace, A be Subset of T, x be Point of T;
hereby
assume x in Der A;
then x is_an_accumulation_point_of A by Th16;
then
A1: x in Cl (A \ {x});
let B be Basis of x, U be Subset of T;
assume U in B;
then U is open & x in U by YELLOW_8:12;
then A \ {x} meets U by A1,PRE_TOPC:24;
then consider y being object such that
A2: y in A \ {x} and
A3: y in U by XBOOLE_0:3;
reconsider y as Point of T by A2;
take y;
y in A by A2,ZFMISC_1:56;
hence y in A /\ U & x <> y by A2,A3,XBOOLE_0:def 4,ZFMISC_1:56;
end;
assume
A4: for B being Basis of x, U being Subset of T st U in B ex y being
Point of T st y in A /\ U & x <> y;
for G being Subset of T st G is open holds x in G implies A \ {x} meets G
proof
set B = the Basis of x;
let G be Subset of T;
assume
A5: G is open;
assume x in G;
then consider V being Subset of T such that
A6: V in B & V c= G by A5,YELLOW_8:13;
(ex y being Point of T st y in A /\ V & x <> y )& A /\ V c= A /\ G by A4,A6
,XBOOLE_1:26;
then consider y being Point of T such that
A7: y in A /\ G and
A8: x <> y;
y in A by A7,XBOOLE_0:def 4;
then
A9: y in A \ {x} by A8,ZFMISC_1:56;
y in G by A7,XBOOLE_0:def 4;
hence thesis by A9,XBOOLE_0:3;
end;
then x in Cl (A \ {x}) by PRE_TOPC:24;
then x is_an_accumulation_point_of A;
hence thesis by Th16;
end;
theorem
for T being non empty TopSpace, A being Subset of T, x being Point of
T holds x in Der A iff ex B being Basis of x st for U being Subset of T st U in
B ex y being Point of T st y in A /\ U & x <> y
proof
let T be non empty TopSpace, A be Subset of T, x be Point of T;
hereby
set B = the Basis of x;
assume x in Der A;
then x is_an_accumulation_point_of A by Th16;
then
A1: x in Cl (A \ {x});
take B;
let U be Subset of T;
assume U in B;
then U is open & x in U by YELLOW_8:12;
then A \ {x} meets U by A1,PRE_TOPC:24;
then consider y being object such that
A2: y in A \ {x} and
A3: y in U by XBOOLE_0:3;
reconsider y as Point of T by A2;
take y;
y in A by A2,ZFMISC_1:56;
hence y in A /\ U & x <> y by A2,A3,XBOOLE_0:def 4,ZFMISC_1:56;
end;
given B being Basis of x such that
A4: for U being Subset of T st U in B ex y being Point of T st y in A
/\ U & x <> y;
for G being Subset of T st G is open holds x in G implies A \ {x} meets G
proof
let G be Subset of T;
assume
A5: G is open;
assume x in G;
then consider V being Subset of T such that
A6: V in B & V c= G by A5,YELLOW_8:13;
(ex y being Point of T st y in A /\ V & x <> y )& A /\ V c= A /\ G by A4,A6
,XBOOLE_1:26;
then consider y being Point of T such that
A7: y in A /\ G and
A8: x <> y;
y in A by A7,XBOOLE_0:def 4;
then
A9: y in A \ {x} by A8,ZFMISC_1:56;
y in G by A7,XBOOLE_0:def 4;
hence thesis by A9,XBOOLE_0:3;
end;
then x in Cl (A \ {x}) by PRE_TOPC:24;
then x is_an_accumulation_point_of A;
hence thesis by Th16;
end;
begin :: 1.3.3. Isolated Points
definition
let T be TopSpace, A be Subset of T, x be set;
pred x is_isolated_in A means
x in A & not x is_an_accumulation_point_of A;
end;
theorem
for T being non empty TopSpace, A being Subset of T, p being set holds
p in A \ Der A iff p is_isolated_in A
proof
let T be non empty TopSpace, A be Subset of T, p be set;
hereby
assume
A1: p in A \ Der A;
then not p in Der A by XBOOLE_0:def 5;
then
A2: not p is_an_accumulation_point_of A by Th16;
p in A by A1,XBOOLE_0:def 5;
hence p is_isolated_in A by A2;
end;
assume
A3: p is_isolated_in A;
then not p is_an_accumulation_point_of A;
then
A4: not p in Der A by Th16;
p in A by A3;
hence thesis by A4,XBOOLE_0:def 5;
end;
theorem Th21:
for T being non empty TopSpace, A being Subset of T, p being
Point of T holds p is_an_accumulation_point_of A iff for U being open Subset of
T st p in U ex q being Point of T st q <> p & q in A & q in U
proof
let T be non empty TopSpace, A be Subset of T, p be Point of T;
hereby
assume p is_an_accumulation_point_of A;
then
A1: p in Der A by Th16;
let U be open Subset of T;
assume p in U;
then consider q being Point of T such that
A2: q in A /\ U & p <> q by A1,Th17;
take q;
thus q <> p & q in A & q in U by A2,XBOOLE_0:def 4;
end;
assume
A3: for U being open Subset of T st p in U ex q being Point of T st q <>
p & q in A & q in U;
for U being open Subset of T st p in U ex y being Point of T st y in A
/\ U & p <> y
proof
let U be open Subset of T;
assume p in U;
then consider q being Point of T such that
A4: q <> p & q in A & q in U by A3;
take q;
thus thesis by A4,XBOOLE_0:def 4;
end;
then p in Der A by Th17;
hence thesis by Th16;
end;
theorem Th22:
for T being non empty TopSpace, A being Subset of T, p being
Point of T holds p is_isolated_in A iff ex G being open Subset of T st G /\ A =
{p}
proof
let T be non empty TopSpace, A be Subset of T, p be Point of T;
hereby
assume
A1: p is_isolated_in A;
then not p is_an_accumulation_point_of A;
then consider U being open Subset of T such that
A2: p in U and
A3: not ex q being Point of T st q <> p & q in A & q in U by Th21;
take U;
A4: p in A by A1;
U /\ A = {p}
proof
thus U /\ A c= {p}
proof
let x be object;
assume x in U /\ A;
then x in U & x in A by XBOOLE_0:def 4;
then x = p by A3;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {p};
then x = p by TARSKI:def 1;
hence thesis by A4,A2,XBOOLE_0:def 4;
end;
hence U /\ A = {p};
end;
given G being open Subset of T such that
A5: G /\ A = {p};
A6: p in G /\ A by A5,TARSKI:def 1;
ex U being open Subset of T st p in U & not ex q being Point of T st q
<> p & q in A & q in U
proof
take G;
for q being Point of T holds q = p or not q in A or not q in G
proof
given q being Point of T such that
A7: q <> p and
A8: q in A & q in G;
q in A /\ G by A8,XBOOLE_0:def 4;
hence thesis by A5,A7,TARSKI:def 1;
end;
hence thesis by A6,XBOOLE_0:def 4;
end;
then
A9: not p is_an_accumulation_point_of A by Th21;
p in A by A6,XBOOLE_0:def 4;
hence thesis by A9;
end;
definition
let T be TopSpace, p be Point of T;
attr p is isolated means
p is_isolated_in [#]T;
end;
theorem
for T being non empty TopSpace, p being Point of T holds p is isolated
iff {p} is open
proof
let T be non empty TopSpace, p be Point of T;
A1: {p} /\ [#]T = {p} by XBOOLE_1:28;
hereby
assume p is isolated;
then p is_isolated_in [#]T;
then ex G being open Subset of T st G /\ [#]T = {p} by Th22;
hence {p} is open;
end;
assume {p} is open;
then p is_isolated_in [#]T by A1,Th22;
hence thesis;
end;
begin :: Derivative of a Subset-Family
definition
let T be TopSpace, F be Subset-Family of T;
func Der F -> Subset-Family of T means
:Def6:
for A being Subset of T holds
A in it iff ex B being Subset of T st A = Der B & B in F;
existence
proof
defpred P[object] means ex W being Subset of T st $1 = Der W & W in F;
thus ex S be Subset-Family of T st for Z being Subset of T holds Z in S
iff P[Z] from SUBSET_1:sch 3;
end;
uniqueness
proof
defpred P[object] means ex W being Subset of T st $1 = Der W & W in F;
let H, G be Subset-Family of T;
assume that
A1: for Z being Subset of T holds Z in H iff P[Z] and
A2: for X being Subset of T holds X in G iff P[X];
now
let X be object;
assume
A3: X in G;
then reconsider X9 = X as Subset of T;
P[X9] by A2,A3;
hence X in H by A1;
end;
then
A4: G c= H;
now
let Z be object;
assume Z in H;
then P[Z] by A1;
hence Z in G by A2;
end;
then H c= G;
hence thesis by A4;
end;
end;
reserve T for non empty TopSpace,
A, B for Subset of T,
F, G for Subset-Family of T,
x for set;
theorem
F = {} implies Der F = {}
proof
assume
A1: F = {};
assume Der F <> {};
then consider x being object such that
A2: x in Der F by XBOOLE_0:def 1;
ex B being Subset of T st x = Der B & B in F by A2,Def6;
hence thesis by A1;
end;
theorem
F = { A } implies Der F = { Der A }
proof
assume
A1: F = { A };
thus Der F c= { Der A }
proof
let x be object;
assume
A2: x in Der F;
then reconsider B = x as Subset of T;
consider C being Subset of T such that
A3: B = Der C and
A4: C in F by A2,Def6;
C = A by A1,A4,TARSKI:def 1;
hence thesis by A3,TARSKI:def 1;
end;
let x be object;
assume x in { Der A };
then
A5: x = Der A by TARSKI:def 1;
A in F by A1,TARSKI:def 1;
hence thesis by A5,Def6;
end;
theorem Th26:
F c= G implies Der F c= Der G
proof
assume
A1: F c= G;
Der F c= Der G
proof
let x be object;
assume
A2: x in Der F;
then reconsider A = x as Subset of T;
ex B being Subset of T st A = Der B & B in F by A2,Def6;
hence thesis by A1,Def6;
end;
hence thesis;
end;
theorem
Der (F \/ G) = Der F \/ Der G
proof
thus Der (F \/ G) c= Der F \/ Der G
proof
let x be object;
assume
A1: x in Der (F \/ G);
then reconsider A = x as Subset of T;
consider B being Subset of T such that
A2: A = Der B and
A3: B in F \/ G by A1,Def6;
per cases by A3,XBOOLE_0:def 3;
suppose
B in F;
then A in Der F by A2,Def6;
hence thesis by XBOOLE_0:def 3;
end;
suppose
B in G;
then A in Der G by A2,Def6;
hence thesis by XBOOLE_0:def 3;
end;
end;
Der F c= Der (F \/ G) & Der G c= Der (F \/ G) by Th26,XBOOLE_1:7;
hence thesis by XBOOLE_1:8;
end;
:: 1.3.4. Properties of a Derivative of a Set
theorem Th28:
for T being non empty TopSpace, A being Subset of T holds Der A c= Cl A
proof
let T be non empty TopSpace, A be Subset of T;
let x be object;
assume
A1: x in Der A;
then reconsider x9 = x as Point of T;
for G being Subset of T st G is open holds x9 in G implies A meets G
proof
let G be Subset of T;
assume
A2: G is open;
assume x9 in G;
then ex y being Point of T st y in A /\ G & x <> y by A1,A2,Th17;
hence thesis;
end;
hence thesis by PRE_TOPC:24;
end;
theorem Th29: :: Theorem 1.3.4. (a)
for T being TopSpace, A being Subset of T holds Cl A = A \/ Der A
proof
let T be TopSpace, A be Subset of T;
per cases;
suppose
A1: T is non empty;
then
A2: Der A c= Cl A by Th28;
thus Cl A c= A \/ Der A
proof
let x be object;
assume
A3: x in Cl A;
then reconsider x9 = x as Point of T;
per cases;
suppose
x in A;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A4: not x in A;
for U being open Subset of T st x9 in U ex y being Point of T st y
in A /\ U & x9 <> y
proof
let U be open Subset of T;
assume x9 in U;
then A meets U by A3,PRE_TOPC:24;
then consider y being object such that
A5: y in A and
A6: y in U by XBOOLE_0:3;
reconsider y as Point of T by A5;
take y;
thus thesis by A4,A5,A6,XBOOLE_0:def 4;
end;
then x9 in Der A by A1,Th17;
hence thesis by XBOOLE_0:def 3;
end;
end;
let x be object;
assume
A7: x in A \/ Der A;
per cases by A7,XBOOLE_0:def 3;
suppose
A8: x in A;
A c= Cl A by PRE_TOPC:18;
hence thesis by A8;
end;
suppose
x in Der A;
hence thesis by A2;
end;
end;
suppose
A9: T is empty;
then the carrier of T is empty;
then Cl A = {} \/ {} .= A \/ Der A by A9;
hence thesis;
end;
end;
theorem Th30: :: Theorem 1.3.4. (b)
for T being non empty TopSpace, A, B being Subset of T st A c= B
holds Der A c= Der B
proof
let T be non empty TopSpace, A, B be Subset of T;
assume
A1: A c= B;
let x be object;
assume
A2: x in Der A;
then reconsider x9 = x as Point of T;
for U being open Subset of T st x9 in U ex y being Point of T st y in B
/\ U & x9 <> y
proof
let U be open Subset of T;
assume x9 in U;
then
A3: ex y being Point of T st y in A /\ U & x9 <> y by A2,Th17;
A /\ U c= B /\ U by A1,XBOOLE_1:26;
hence thesis by A3;
end;
hence thesis by Th17;
end;
theorem Th31: :: Theorem 1.3.4. (c)
for T being non empty TopSpace, A, B being Subset of T holds Der
(A \/ B) = Der A \/ Der B
proof
let T be non empty TopSpace, A, B be Subset of T;
thus Der (A \/ B) c= Der A \/ Der B
proof
let x be object;
assume x in Der (A \/ B);
then x is_an_accumulation_point_of A \/ B by Th16;
then
A1: x in Cl ((A \/ B) \ {x});
(A \/ B) \ {x} = (A \ {x}) \/ (B \ {x}) by XBOOLE_1:42;
then Cl ((A \/ B) \ {x}) = Cl (A \ {x}) \/ Cl (B \ {x}) by PRE_TOPC:20;
then x in Cl (A \ {x}) or x in Cl (B \ {x}) by A1,XBOOLE_0:def 3;
then
x is_an_accumulation_point_of A or x is_an_accumulation_point_of B;
then x in Der A or x in Der B by Th16;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume x in Der A \/ Der B;
then x in Der A or x in Der B by XBOOLE_0:def 3;
then
A2: x is_an_accumulation_point_of A or x is_an_accumulation_point_of B by Th16;
x in Cl ((A \/ B) \ {x})
proof
B \ {x} c= (A \/ B) \ {x} by XBOOLE_1:7,33;
then
A3: Cl (B \ {x}) c= Cl ((A \/ B) \ {x}) by PRE_TOPC:19;
A \ {x} c= (A \/ B) \ {x} by XBOOLE_1:7,33;
then
A4: Cl (A \ {x}) c= Cl ((A \/ B) \ {x}) by PRE_TOPC:19;
per cases by A2;
suppose
x in Cl (A \ {x});
hence thesis by A4;
end;
suppose
x in Cl (B \ {x});
hence thesis by A3;
end;
end;
then x is_an_accumulation_point_of A \/ B;
hence thesis by Th16;
end;
theorem Th32:
for T being non empty TopSpace, A being Subset of T st T is T_1
holds Der Der A c= Der A
proof
let T be non empty TopSpace, A be Subset of T;
assume
A1: T is T_1;
let x be object;
assume
A2: x in Der Der A;
then reconsider x9 = x as Point of T;
assume not x in Der A;
then consider G being open Subset of T such that
A3: x9 in G and
A4: not ex y being Point of T st y in A /\ G & x9 <> y by Th17;
Cl {x9} = {x9} by A1,YELLOW_8:26;
then
A5: G \ {x9} is open by FRECHET:4;
consider y being Point of T such that
A6: y in Der A /\ G and
A7: x <> y by A2,A3,Th17;
y in Der A by A6,XBOOLE_0:def 4;
then
A8: y in Der A \ {x} by A7,ZFMISC_1:56;
y in G by A6,XBOOLE_0:def 4;
then consider q being set such that
A9: q in G and
A10: q in Der A \ {x} by A8;
reconsider q as Point of T by A9;
not q in {x} by A10,XBOOLE_0:def 5;
then
A11: q in G \ {x} by A9,XBOOLE_0:def 5;
set U = G \ {x9};
A12: G misses A \ {x}
proof
assume G meets A \ {x};
then consider g being object such that
A13: g in G and
A14: g in A \ {x} by XBOOLE_0:3;
g in A by A14,XBOOLE_0:def 5;
then g in A /\ G by A13,XBOOLE_0:def 4;
then x9 = g by A4;
hence thesis by A14,ZFMISC_1:56;
end;
q in Der A by A10,XBOOLE_0:def 5;
then consider y being Point of T such that
A15: y in A /\ U and
A16: q <> y by A11,A5,Th17;
y in A by A15,XBOOLE_0:def 4;
then
A17: y in A \ {q} by A16,ZFMISC_1:56;
y in U by A15,XBOOLE_0:def 4;
then consider f being set such that
A18: f in G \ {x9} and
A19: f in A \ {q} by A17;
f <> x9 & f in A by A18,A19,ZFMISC_1:56;
then
A20: f in A \ {x9} by ZFMISC_1:56;
f in G by A18,ZFMISC_1:56;
hence thesis by A12,A20,XBOOLE_0:3;
end;
theorem Th33:
for T being TopSpace, A being Subset of T st T is T_1 holds Cl Der A = Der A
proof
let T be TopSpace, A be Subset of T;
assume
A1: T is T_1;
per cases;
suppose
A2: T is non empty;
Cl Der A = Der A \/ Der Der A by Th29;
then
A3: Cl Der A c= Der A \/ Der A by A1,A2,Th32,XBOOLE_1:9;
Der A c= Cl Der A by PRE_TOPC:18;
hence thesis by A3;
end;
suppose
A4: T is empty;
then Cl Der A = {};
hence thesis by A4;
end;
end;
registration
let T be T_1 non empty TopSpace, A be Subset of T;
cluster Der A -> closed;
coherence
proof
Der A = Cl Der A by Th33;
hence thesis;
end;
end;
theorem Th34: :: Theorem 1.3.4. d)
for T being non empty TopSpace, F being Subset-Family of T holds
union Der F c= Der union F
proof
let T be non empty TopSpace, F be Subset-Family of T;
let x be object;
assume x in union Der F;
then consider Y being set such that
A1: x in Y and
A2: Y in Der F by TARSKI:def 4;
reconsider Y as Subset of T by A2;
consider B being Subset of T such that
A3: Y = Der B and
A4: B in F by A2,Def6;
Der B c= Der union F by A4,Th30,ZFMISC_1:74;
hence thesis by A1,A3;
end;
theorem
A c= B & x is_an_accumulation_point_of A implies x
is_an_accumulation_point_of B
proof
assume A c= B;
then
A1: Der A c= Der B by Th30;
assume x is_an_accumulation_point_of A;
then x in Der A by Th16;
hence thesis by A1,Th16;
end;
begin :: 1.3.4. Density-in-itself
definition
let T be TopSpace, A be Subset of T;
attr A is dense-in-itself means
A c= Der A;
end;
definition
let T be non empty TopSpace;
attr T is dense-in-itself means
[#]T is dense-in-itself;
end;
theorem Th36:
T is T_1 & A is dense-in-itself implies Cl A is dense-in-itself
proof
assume
A1: T is T_1;
assume A is dense-in-itself;
then A c= Der A;
then
A2: Der A = A \/ Der A by XBOOLE_1:12
.= Cl A by Th29;
Der Cl A = Der (A \/ Der A) by Th29
.= Der A \/ Der Der A by Th31
.= Cl A by A1,A2,Th32,XBOOLE_1:12;
hence thesis;
end;
definition
let T be TopSpace, F be Subset-Family of T;
attr F is dense-in-itself means
for A being Subset of T st A in F holds A is dense-in-itself;
end;
theorem Th37:
for F being Subset-Family of T st F is dense-in-itself holds
union F c= union Der F
proof
let F be Subset-Family of T;
assume
A1: F is dense-in-itself;
thus union F c= union Der F
proof
let x be object;
assume x in union F;
then consider A being set such that
A2: x in A and
A3: A in F by TARSKI:def 4;
reconsider A as Subset of T by A3;
A is dense-in-itself by A1,A3;
then
A4: A c= Der A;
Der A in Der F by A3,Def6;
hence thesis by A2,A4,TARSKI:def 4;
end;
end;
theorem Th38:
F is dense-in-itself implies union F is dense-in-itself
proof
assume F is dense-in-itself;
then
A1: union F c= union Der F by Th37;
union Der F c= Der union F by Th34;
then union F c= Der union F by A1;
hence thesis;
end;
theorem
Fr {}T = {}
proof
Fr {}T = Cl {}T /\ Cl ({}T)` by TOPS_1:def 2
.= {} /\ Cl ({}T)`;
hence thesis;
end;
registration
let T be TopSpace, A be open closed Subset of T;
cluster Fr A -> empty;
coherence by Th14;
end;
registration
let T be non empty non discrete TopSpace;
cluster non open for Subset of T;
existence by TDLAT_3:15;
cluster non closed for Subset of T;
existence by TDLAT_3:16;
end;
registration
let T be non empty non discrete TopSpace, A be non open Subset of T;
cluster Fr A -> non empty;
coherence by Th14;
end;
registration
let T be non empty non discrete TopSpace, A be non closed Subset of T;
cluster Fr A -> non empty;
coherence by Th14;
end;
begin :: Perfect Sets
definition
let T be TopSpace, A be Subset of T;
attr A is perfect means
A is closed dense-in-itself;
end;
registration
let T be TopSpace;
cluster perfect -> closed dense-in-itself for Subset of T;
coherence;
cluster closed dense-in-itself -> perfect for Subset of T;
coherence;
end;
theorem Th40:
for T being TopSpace holds Der {}T = {}T
proof
let T be TopSpace;
Cl {}T is empty;
then {} = {}T \/ Der {}T by Th29
.= Der {}T;
hence thesis;
end;
Lm1: for T being TopSpace, A being Subset of T st A is closed dense-in-itself
holds Der A = A
proof
let T be TopSpace, A be Subset of T;
assume
A1: A is closed dense-in-itself;
then A = Cl A by PRE_TOPC:22
.= Der A \/ A by Th29;
hence Der A c= A by XBOOLE_1:7;
thus thesis by A1;
end;
theorem Th41:
for T being TopSpace, A being Subset of T holds A is perfect iff Der A = A
proof
let T be TopSpace, A be Subset of T;
thus A is perfect implies Der A = A by Lm1;
assume
A1: Der A = A;
A2: Cl A = Der A \/ A by Th29
.= A by A1;
A is dense-in-itself by A1;
hence thesis by A2;
end;
theorem Th42:
for T being TopSpace holds {}T is perfect
proof
let T be TopSpace;
Der {}T = {}T by Th40;
hence thesis by Th41;
end;
registration
let T be TopSpace;
cluster empty -> perfect for Subset of T;
coherence
proof
let A be Subset of T;
assume A is empty;
then A = {}T;
hence thesis by Th42;
end;
end;
registration
let T be TopSpace;
cluster perfect for Subset of T;
existence
proof
take {}T;
thus thesis;
end;
end;
begin :: Scattered Subsets
definition
let T be TopSpace, A be Subset of T;
attr A is scattered means
not ex B being Subset of T st B is non empty & B c= A & B is dense-in-itself;
end;
registration
let T be non empty TopSpace;
cluster non empty scattered -> non dense-in-itself for Subset of T;
coherence;
cluster dense-in-itself non empty -> non scattered for Subset of T;
coherence;
end;
theorem
for T being TopSpace holds {}T is scattered;
registration
let T be TopSpace;
cluster empty -> scattered for Subset of T;
coherence;
end;
theorem
for T being non empty TopSpace st T is T_1 holds ex A, B being Subset
of T st A \/ B = [#]T & A misses B & A is perfect & B is scattered
proof
let T be non empty TopSpace;
defpred P[Subset of T] means $1 is dense-in-itself;
consider CC being Subset-Family of T such that
A1: for A being Subset of T holds A in CC iff P[A] from SUBSET_1:sch 3;
set C = union CC;
A2: [#]T = C \/ C` & C misses C` by PRE_TOPC:2,XBOOLE_1:79;
A3: CC is dense-in-itself by A1;
assume T is T_1;
then Cl C is dense-in-itself by A3,Th36,Th38;
then Cl C in CC by A1;
then
A4: Cl C c= C by ZFMISC_1:74;
C c= Cl C by PRE_TOPC:18;
then
A5: Cl C = C by A4;
not ex B being Subset of T st B is non empty & B c= C` & B is dense-in-itself
proof
given B being Subset of T such that
A6: B is non empty and
A7: B c= C` & B is dense-in-itself;
B misses union CC & B in CC by A1,A7,SUBSET_1:23;
hence thesis by A6,XBOOLE_1:69,ZFMISC_1:74;
end;
then
A8: C` is scattered;
C is dense-in-itself by A3,Th38;
hence thesis by A5,A8,A2;
end;
registration
let T be discrete TopSpace, A be Subset of T;
cluster Fr A -> empty;
coherence
proof
A is open closed by TDLAT_3:15,16;
hence thesis;
end;
end;
registration
let T be discrete TopSpace;
cluster -> closed open for Subset of T;
coherence by TDLAT_3:15,16;
end;
theorem Th45:
for T being discrete TopSpace, A being Subset of T holds Der A = {}
proof
let T be discrete TopSpace, A be Subset of T;
per cases;
suppose
A1: T is non empty;
assume Der A <> {};
then consider x being object such that
A2: x in Der A by XBOOLE_0:def 1;
x is_an_accumulation_point_of A by A1,A2,Th16;
then x in Cl (A \ {x});
then x in A \ {x} by PRE_TOPC:22;
hence thesis by ZFMISC_1:56;
end;
suppose
T is empty;
then the carrier of T is empty;
hence thesis;
end;
end;
registration
let T be discrete non empty TopSpace, A be Subset of T;
cluster Der A -> empty;
coherence by Th45;
end;
begin :: Density of a Topological Space and Separable Spaces
:: 1.3.6. Density of a Topological Space
definition
let T be TopSpace;
func density T -> cardinal number means
:Def12:
(ex A being Subset of T st A
is dense & it = card A) & for B being Subset of T st B is dense holds it c=
card B;
existence
proof
set B0 = [#]T;
defpred P[Ordinal] means ex A being Subset of T st A is dense & $1
= card A;
card B0 is ordinal;
then
A1: ex A being Ordinal st P[A];
consider A being Ordinal such that
A2: P[A] and
A3: for B being Ordinal st P[B] holds A c= B from ORDINAL1:sch
1(A1 );
consider B1 being Subset of T such that
A4: B1 is dense & A = card B1 by A2;
take card B1;
thus thesis by A3,A4;
end;
uniqueness;
end;
:: Separable Spaces
definition
let T be TopSpace;
attr T is separable means
density T c= omega;
end;
theorem Th46:
for T being countable TopSpace holds T is separable
proof
let T be countable TopSpace;
card [#]T c= omega & density T c= card [#]T by Def12,CARD_3:def 14;
then density T c= omega;
hence thesis;
end;
registration
cluster countable -> separable for TopSpace;
coherence by Th46;
end;
begin :: Exercise 1.3.E.
theorem
for A being Subset of R^1 st A = RAT holds A` = IRRAT by BORSUK_5:def 1
,TOPMETR:17;
Lm2: RAT = REAL \ IRRAT
proof
REAL \ IRRAT = REAL /\ RAT by BORSUK_5:def 1,XBOOLE_1:48;
hence thesis by NUMBERS:12,XBOOLE_1:28;
end;
theorem
for A being Subset of R^1 st A = IRRAT holds A` = RAT by Lm2,TOPMETR:17;
theorem
for A being Subset of R^1 st A = RAT holds Int A = {}
proof
let A be Subset of R^1;
assume A = RAT;
then Cl A` = [#]R^1 by BORSUK_5:28,def 1,TOPMETR:17;
then (Cl A`)` = {}R^1 by XBOOLE_1:37;
hence thesis by Th3;
end;
theorem
for A being Subset of R^1 st A = IRRAT holds Int A = {}
proof
let A be Subset of R^1;
assume A = IRRAT;
then Cl A` = [#]R^1 by Lm2,BORSUK_5:15,TOPMETR:17;
then (Cl A`)` = {}R^1 by XBOOLE_1:37;
hence thesis by Th3;
end;
reconsider B = RAT as Subset of R^1 by NUMBERS:12,TOPMETR:17;
theorem Th51:
RAT is dense Subset of R^1
proof
Cl B = the carrier of R^1 by BORSUK_5:15;
hence thesis by TOPS_3:def 2;
end;
reconsider A = IRRAT as Subset of R^1 by TOPMETR:17;
theorem Th52:
IRRAT is dense Subset of R^1
proof
Cl A = the carrier of R^1 by BORSUK_5:28;
hence thesis by TOPS_3:def 2;
end;
theorem Th53:
RAT is boundary Subset of R^1
proof
B` is dense by Th52,BORSUK_5:def 1,TOPMETR:17;
hence thesis by TOPS_1:def 4;
end;
theorem Th54:
IRRAT is boundary Subset of R^1
proof
A` is dense by Lm2,Th51,TOPMETR:17;
hence thesis by TOPS_1:def 4;
end;
theorem Th55:
REAL is non boundary Subset of R^1
proof
reconsider A = [#]REAL as Subset of R^1 by TOPMETR:17;
[#]R^1 = REAL by TOPMETR:17;
hence thesis;
end;
theorem
ex A, B being Subset of R^1 st A is boundary & B is boundary &
A \/ B is non boundary
proof
reconsider B = IRRAT as Subset of R^1 by TOPMETR:17;
reconsider A = RAT as Subset of R^1 by NUMBERS:12,TOPMETR:17;
take A,B;
A \/ B = RAT \/ REAL by BORSUK_5:def 1,XBOOLE_1:39
.= REAL by NUMBERS:12,XBOOLE_1:12;
hence thesis by Th53,Th54,Th55;
end;