:: On the Boundary and Derivative of a Set
:: by Adam Grabowski
::
:: Received November 8, 2004
:: Copyright (c) 2004-2016 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;
begin :: Preliminaries
theorem :: TOPGEN_1:1
for T being 1-sorted, A, B being Subset of T holds A meets B` iff A \ B <> {}
;
theorem :: TOPGEN_1:2
for T being 1-sorted holds T is countable iff card [#]T c= omega;
registration
let T be finite 1-sorted;
cluster [#]T -> finite;
end;
registration
cluster finite -> countable for 1-sorted;
end;
registration
cluster countable non empty for 1-sorted;
cluster countable non empty for TopSpace;
end;
registration
let T be countable 1-sorted;
cluster [#]T -> countable;
end;
registration
cluster T_1 non empty for TopSpace;
end;
begin
theorem :: TOPGEN_1:3
for T being TopSpace, A being Subset of T holds Int A = (Cl A`)`;
:: Collective Boundary
definition
let T be TopSpace, F be Subset-Family of T;
func Fr F -> Subset-Family of T means
:: TOPGEN_1:def 1
for A being Subset of T holds A
in it iff ex B being Subset of T st A = Fr B & B in F;
end;
theorem :: TOPGEN_1:4
for T being TopSpace, F being Subset-Family of T st F = {} holds Fr F = {};
theorem :: TOPGEN_1:5
for T being TopSpace, F being Subset-Family of T, A being Subset of T
st F = { A } holds Fr F = { Fr A };
theorem :: TOPGEN_1:6
for T being TopSpace, F, G being Subset-Family of T st F c= G
holds Fr F c= Fr G;
theorem :: TOPGEN_1:7
for T being TopSpace, F, G being Subset-Family of T holds Fr (F \/ G)
= Fr F \/ Fr G;
theorem :: TOPGEN_1:8 :: 1.3.0.
for T being TopStruct, A being Subset of T holds Fr A = Cl A \ Int A;
theorem :: TOPGEN_1:9 :: 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 <> {};
theorem :: TOPGEN_1:10
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 <> {};
theorem :: TOPGEN_1:11
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 <> {};
theorem :: TOPGEN_1:12 :: 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);
theorem :: TOPGEN_1:13 :: 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`;
theorem :: TOPGEN_1:14 :: Theorem 1.3.2. (k)
for T being TopSpace, A being Subset of T holds A is open closed
iff Fr A = {};
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
:: TOPGEN_1:def 2
x in Cl (A \ {x});
end;
theorem :: TOPGEN_1:15
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
:: TOPGEN_1:def 3
for x being set st x in the carrier
of T holds x in it iff x is_an_accumulation_point_of A;
end;
:: 1.3.3. Characterizations of a Derivative
theorem :: TOPGEN_1:16
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;
theorem :: TOPGEN_1:17
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;
theorem :: TOPGEN_1:18
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;
theorem :: TOPGEN_1:19
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;
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
:: TOPGEN_1:def 4
x in A & not x is_an_accumulation_point_of A;
end;
theorem :: TOPGEN_1:20
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;
theorem :: TOPGEN_1:21
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;
theorem :: TOPGEN_1:22
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};
definition
let T be TopSpace, p be Point of T;
attr p is isolated means
:: TOPGEN_1:def 5
p is_isolated_in [#]T;
end;
theorem :: TOPGEN_1:23
for T being non empty TopSpace, p being Point of T holds p is isolated
iff {p} is open;
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
:: TOPGEN_1:def 6
for A being Subset of T holds
A in it iff ex B being Subset of T st A = Der B & B in F;
end;
reserve T for non empty TopSpace,
A, B for Subset of T,
F, G for Subset-Family of T,
x for set;
theorem :: TOPGEN_1:24
F = {} implies Der F = {};
theorem :: TOPGEN_1:25
F = { A } implies Der F = { Der A };
theorem :: TOPGEN_1:26
F c= G implies Der F c= Der G;
theorem :: TOPGEN_1:27
Der (F \/ G) = Der F \/ Der G;
:: 1.3.4. Properties of a Derivative of a Set
theorem :: TOPGEN_1:28
for T being non empty TopSpace, A being Subset of T holds Der A c= Cl A;
theorem :: TOPGEN_1:29 :: Theorem 1.3.4. (a)
for T being TopSpace, A being Subset of T holds Cl A = A \/ Der A;
theorem :: TOPGEN_1:30 :: 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;
theorem :: TOPGEN_1:31 :: 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;
theorem :: TOPGEN_1:32
for T being non empty TopSpace, A being Subset of T st T is T_1
holds Der Der A c= Der A;
theorem :: TOPGEN_1:33
for T being TopSpace, A being Subset of T st T is T_1 holds Cl Der A = Der A;
registration
let T be T_1 non empty TopSpace, A be Subset of T;
cluster Der A -> closed;
end;
theorem :: TOPGEN_1:34 :: 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;
theorem :: TOPGEN_1:35
A c= B & x is_an_accumulation_point_of A implies x
is_an_accumulation_point_of B;
begin :: 1.3.4. Density-in-itself
definition
let T be TopSpace, A be Subset of T;
attr A is dense-in-itself means
:: TOPGEN_1:def 7
A c= Der A;
end;
definition
let T be non empty TopSpace;
attr T is dense-in-itself means
:: TOPGEN_1:def 8
[#]T is dense-in-itself;
end;
theorem :: TOPGEN_1:36
T is T_1 & A is dense-in-itself implies Cl A is dense-in-itself;
definition
let T be TopSpace, F be Subset-Family of T;
attr F is dense-in-itself means
:: TOPGEN_1:def 9
for A being Subset of T st A in F holds A is dense-in-itself;
end;
theorem :: TOPGEN_1:37
for F being Subset-Family of T st F is dense-in-itself holds
union F c= union Der F;
theorem :: TOPGEN_1:38
F is dense-in-itself implies union F is dense-in-itself;
theorem :: TOPGEN_1:39
Fr {}T = {};
registration
let T be TopSpace, A be open closed Subset of T;
cluster Fr A -> empty;
end;
registration
let T be non empty non discrete TopSpace;
cluster non open for Subset of T;
cluster non closed for Subset of T;
end;
registration
let T be non empty non discrete TopSpace, A be non open Subset of T;
cluster Fr A -> non empty;
end;
registration
let T be non empty non discrete TopSpace, A be non closed Subset of T;
cluster Fr A -> non empty;
end;
begin :: Perfect Sets
definition
let T be TopSpace, A be Subset of T;
attr A is perfect means
:: TOPGEN_1:def 10
A is closed dense-in-itself;
end;
registration
let T be TopSpace;
cluster perfect -> closed dense-in-itself for Subset of T;
cluster closed dense-in-itself -> perfect for Subset of T;
end;
theorem :: TOPGEN_1:40
for T being TopSpace holds Der {}T = {}T;
theorem :: TOPGEN_1:41
for T being TopSpace, A being Subset of T holds A is perfect iff Der A = A;
theorem :: TOPGEN_1:42
for T being TopSpace holds {}T is perfect;
registration
let T be TopSpace;
cluster empty -> perfect for Subset of T;
end;
registration
let T be TopSpace;
cluster perfect for Subset of T;
end;
begin :: Scattered Subsets
definition
let T be TopSpace, A be Subset of T;
attr A is scattered means
:: TOPGEN_1:def 11
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;
cluster dense-in-itself non empty -> non scattered for Subset of T;
end;
theorem :: TOPGEN_1:43
for T being TopSpace holds {}T is scattered;
registration
let T be TopSpace;
cluster empty -> scattered for Subset of T;
end;
theorem :: TOPGEN_1:44
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;
registration
let T be discrete TopSpace, A be Subset of T;
cluster Fr A -> empty;
end;
registration
let T be discrete TopSpace;
cluster -> closed open for Subset of T;
end;
theorem :: TOPGEN_1:45
for T being discrete TopSpace, A being Subset of T holds Der A = {};
registration
let T be discrete non empty TopSpace, A be Subset of T;
cluster Der A -> empty;
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
:: TOPGEN_1:def 12
(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;
end;
:: Separable Spaces
definition
let T be TopSpace;
attr T is separable means
:: TOPGEN_1:def 13
density T c= omega;
end;
theorem :: TOPGEN_1:46
for T being countable TopSpace holds T is separable;
registration
cluster countable -> separable for TopSpace;
end;
begin :: Exercise 1.3.E.
theorem :: TOPGEN_1:47
for A being Subset of R^1 st A = RAT holds A` = IRRAT;
theorem :: TOPGEN_1:48
for A being Subset of R^1 st A = IRRAT holds A` = RAT;
theorem :: TOPGEN_1:49
for A being Subset of R^1 st A = RAT holds Int A = {};
theorem :: TOPGEN_1:50
for A being Subset of R^1 st A = IRRAT holds Int A = {};
theorem :: TOPGEN_1:51
RAT is dense Subset of R^1;
theorem :: TOPGEN_1:52
IRRAT is dense Subset of R^1;
theorem :: TOPGEN_1:53
RAT is boundary Subset of R^1;
theorem :: TOPGEN_1:54
IRRAT is boundary Subset of R^1;
theorem :: TOPGEN_1:55
REAL is non boundary Subset of R^1;
theorem :: TOPGEN_1:56
ex A, B being Subset of R^1 st A is boundary & B is boundary &
A \/ B is non boundary;