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