:: On the Boundary and Derivative of a Set :: by Adam Grabowski :: :: Received November 8, 2004 :: Copyright (c) 2004-2021 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;