:: The Properties of Supercondensed Sets, Subcondensed Sets and Condensed Sets :: by Magdalena Jastrz\c{e}bska and Adam Grabowski :: :: Received March 31, 2005 :: Copyright (c) 2005-2012 Association of Mizar Users begin registration let D be non trivial set ; cluster ADTS D -> non trivial ; coherence not ADTS D is trivial proofend; end; registration cluster non trivial strict TopSpace-like anti-discrete for TopStruct ; existence ex b1 being TopSpace st ( b1 is anti-discrete & not b1 is trivial & b1 is strict ) proofend; end; theorem Th1: :: ISOMICHI:1 for T being TopSpace for A, B being Subset of T holds (Int (Cl (Int A))) /\ (Int (Cl (Int B))) = Int (Cl (Int (A /\ B))) proofend; theorem Th2: :: ISOMICHI:2 for T being TopSpace for A, B being Subset of T holds Cl (Int (Cl (A \/ B))) = (Cl (Int (Cl A))) \/ (Cl (Int (Cl B))) proofend; begin definition let T be TopStruct ; let A be Subset of T; attrA is supercondensed means :Def1: :: ISOMICHI:def 1 Int (Cl A) = Int A; attrA is subcondensed means :Def2: :: ISOMICHI:def 2 Cl (Int A) = Cl A; end; :: deftheorem Def1 defines supercondensed ISOMICHI:def_1_:_ for T being TopStruct for A being Subset of T holds ( A is supercondensed iff Int (Cl A) = Int A ); :: deftheorem Def2 defines subcondensed ISOMICHI:def_2_:_ for T being TopStruct for A being Subset of T holds ( A is subcondensed iff Cl (Int A) = Cl A ); registration let T be TopSpace; cluster closed -> supercondensed for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is closed holds b1 is supercondensed proofend; end; theorem :: ISOMICHI:3 for T being TopSpace for A being Subset of T st A is closed holds A is supercondensed ; theorem Th4: :: ISOMICHI:4 for T being TopSpace for A being Subset of T st A is open holds A is subcondensed proofend; definition let T be TopSpace; let A be Subset of T; redefine attr A is condensed means :Def3: :: ISOMICHI:def 3 ( Cl (Int A) = Cl A & Int (Cl A) = Int A ); compatibility ( A is condensed iff ( Cl (Int A) = Cl A & Int (Cl A) = Int A ) ) proofend; end; :: deftheorem Def3 defines condensed ISOMICHI:def_3_:_ for T being TopSpace for A being Subset of T holds ( A is condensed iff ( Cl (Int A) = Cl A & Int (Cl A) = Int A ) ); theorem Th5: :: ISOMICHI:5 for T being TopSpace for A being Subset of T holds ( A is condensed iff ( A is subcondensed & A is supercondensed ) ) proofend; registration let T be TopSpace; cluster condensed -> supercondensed subcondensed for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is condensed holds ( b1 is subcondensed & b1 is supercondensed ) by Th5; cluster supercondensed subcondensed -> condensed for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is subcondensed & b1 is supercondensed holds b1 is condensed by Th5; end; registration let T be TopSpace; cluster condensed supercondensed subcondensed for Element of bool the carrier of T; existence ex b1 being Subset of T st ( b1 is condensed & b1 is subcondensed & b1 is supercondensed ) proofend; end; theorem :: ISOMICHI:6 for T being TopSpace for A being Subset of T st A is supercondensed holds A ` is subcondensed proofend; theorem :: ISOMICHI:7 for T being TopSpace for A being Subset of T st A is subcondensed holds A ` is supercondensed proofend; :: Corollary to Theorem 1 :: A is condensed implies A` is condensed = TDLAT_1:16; theorem Th8: :: ISOMICHI:8 for T being TopSpace for A being Subset of T holds ( A is supercondensed iff Int (Cl A) c= A ) proofend; theorem Th9: :: ISOMICHI:9 for T being TopSpace for A being Subset of T holds ( A is subcondensed iff A c= Cl (Int A) ) proofend; registration let T be TopSpace; cluster subcondensed -> semi-open for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is subcondensed holds b1 is semi-open proofend; cluster semi-open -> subcondensed for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is semi-open holds b1 is subcondensed proofend; end; theorem Th10: :: ISOMICHI:10 for T being TopSpace for A being Subset of T holds ( A is condensed iff ( Int (Cl A) c= A & A c= Cl (Int A) ) ) proofend; begin notation let T be TopStruct ; let A be Subset of T; synonym regular_open A for open_condensed ; end; notation let T be TopStruct ; let A be Subset of T; synonym regular_closed A for closed_condensed ; end; theorem :: ISOMICHI:11 for T being TopSpace holds ( [#] T is regular_open & [#] T is regular_closed ) proofend; registration let T be TopSpace; cluster [#] T -> regular_closed regular_open ; coherence ( [#] T is regular_open & [#] T is regular_closed ) proofend; end; registration let T be TopSpace; cluster empty -> regular_closed regular_open for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is empty holds ( b1 is regular_open & b1 is regular_closed ) proofend; end; theorem :: ISOMICHI:12 for T being TopSpace holds Int (Cl ({} T)) = {} T proofend; theorem Th13: :: ISOMICHI:13 for T being TopSpace for A being Subset of T st A is regular_open holds A ` is regular_closed proofend; registration let T be TopSpace; cluster regular_closed regular_open for Element of bool the carrier of T; existence ex b1 being Subset of T st ( b1 is regular_open & b1 is regular_closed ) proofend; end; registration let T be TopSpace; let A be regular_open Subset of T; clusterA ` -> regular_closed ; coherence A ` is regular_closed by Th13; end; theorem Th14: :: ISOMICHI:14 for T being TopSpace for A being Subset of T st A is regular_closed holds A ` is regular_open proofend; registration let T be TopSpace; let A be regular_closed Subset of T; clusterA ` -> regular_open ; coherence A ` is regular_open by Th14; end; registration let T be TopSpace; cluster regular_open -> open for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is regular_open holds b1 is open by TOPS_1:67; cluster regular_closed -> closed for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is regular_closed holds b1 is closed by TOPS_1:66; end; :: (A is regular_open & B is regular_open) implies :: A /\ B is regular_open by TOPS_1:109; :: A is regular_closed & B is regular_closed implies :: A \/ B is regular_closed by TOPS_1:108; theorem Th15: :: ISOMICHI:15 for T being TopSpace for A being Subset of T holds ( Int (Cl A) is regular_open & Cl (Int A) is regular_closed ) proofend; registration let T be TopSpace; let A be Subset of T; cluster Int (Cl A) -> regular_open ; coherence Int (Cl A) is regular_open by Th15; cluster Cl (Int A) -> regular_closed ; coherence Cl (Int A) is regular_closed by Th15; end; theorem :: ISOMICHI:16 for T being TopSpace for A being Subset of T holds ( A is regular_open iff ( A is supercondensed & A is open ) ) proofend; theorem :: ISOMICHI:17 for T being TopSpace for A being Subset of T holds ( A is regular_closed iff ( A is subcondensed & A is closed ) ) proofend; registration let T be TopSpace; cluster regular_open -> open condensed for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is regular_open holds ( b1 is condensed & b1 is open ) by TOPS_1:67; cluster open condensed -> regular_open for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is condensed & b1 is open holds b1 is regular_open by TOPS_1:67; cluster regular_closed -> closed condensed for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is regular_closed holds ( b1 is condensed & b1 is closed ) by TOPS_1:66; cluster closed condensed -> regular_closed for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is condensed & b1 is closed holds b1 is regular_closed by TOPS_1:66; end; theorem :: ISOMICHI:18 for T being TopSpace for A being Subset of T holds ( A is condensed iff ex B being Subset of T st ( B is regular_open & B c= A & A c= Cl B ) ) proofend; theorem :: ISOMICHI:19 for T being TopSpace for A being Subset of T holds ( A is condensed iff ex B being Subset of T st ( B is regular_closed & Int B c= A & A c= B ) ) proofend; begin definition let T be TopStruct ; let A be Subset of T; redefine func Fr A equals :: ISOMICHI:def 4 (Cl A) \ (Int A); compatibility for b1 being Element of bool the carrier of T holds ( b1 = Fr A iff b1 = (Cl A) \ (Int A) ) by TOPGEN_1:8; end; :: deftheorem defines Fr ISOMICHI:def_4_:_ for T being TopStruct for A being Subset of T holds Fr A = (Cl A) \ (Int A); theorem :: ISOMICHI:20 for T being TopSpace for A being Subset of T holds ( A is condensed iff ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) ) proofend; definition let T be TopStruct ; let A be Subset of T; func Border A -> Subset of T equals :: ISOMICHI:def 5 Int (Fr A); coherence Int (Fr A) is Subset of T ; end; :: deftheorem defines Border ISOMICHI:def_5_:_ for T being TopStruct for A being Subset of T holds Border A = Int (Fr A); theorem Th21: :: ISOMICHI:21 for T being TopSpace for A being Subset of T holds ( Border A is regular_open & Border A = (Int (Cl A)) \ (Cl (Int A)) & Border A = (Int (Cl A)) /\ (Int (Cl (A `))) ) proofend; registration let T be TopSpace; let A be Subset of T; cluster Border A -> regular_open ; coherence Border A is regular_open by Th21; end; theorem Th22: :: ISOMICHI:22 for T being TopSpace for A being Subset of T holds ( A is supercondensed iff ( Int A is regular_open & Border A is empty ) ) proofend; theorem Th23: :: ISOMICHI:23 for T being TopSpace for A being Subset of T holds ( A is subcondensed iff ( Cl A is regular_closed & Border A is empty ) ) proofend; registration let T be TopSpace; let A be Subset of T; cluster Border (Border A) -> empty ; coherence Border (Border A) is empty ; end; theorem :: ISOMICHI:24 for T being TopSpace for A being Subset of T holds ( A is condensed iff ( Int A is regular_open & Cl A is regular_closed & Border A is empty ) ) proofend; begin theorem :: ISOMICHI:25 for A being Subset of R^1 for a being real number st A = ].-infty,a.] holds Int A = ].-infty,a.[ proofend; theorem :: ISOMICHI:26 for A being Subset of R^1 for a being real number st A = [.a,+infty.[ holds Int A = ].a,+infty.[ proofend; theorem Th27: :: ISOMICHI:27 for A being Subset of R^1 for a, b being real number st A = (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ holds Cl A = the carrier of R^1 proofend; theorem :: ISOMICHI:28 for A being Subset of R^1 for a, b being real number st A = RAT (a,b) holds Int A = {} proofend; theorem :: ISOMICHI:29 for A being Subset of R^1 for a, b being real number st A = IRRAT (a,b) holds Int A = {} proofend; theorem :: ISOMICHI:30 for a, b being real number st a >= b holds IRRAT (a,b) = {} proofend; theorem Th31: :: ISOMICHI:31 for a, b being real number holds IRRAT (a,b) c= [.a,+infty.[ proofend; theorem Th32: :: ISOMICHI:32 for A being Subset of R^1 for a, b, c being real number st A = ].-infty,a.[ \/ (RAT (b,c)) & a < b & b < c holds Int A = ].-infty,a.[ proofend; Lm1: for a, b being real number st a < b holds [.a,b.] \/ {b} = [.a,b.] proofend; theorem :: ISOMICHI:33 for a, b being real number st a < b holds REAL = (].-infty,a.[ \/ [.a,b.]) \/ ].b,+infty.[ proofend; theorem Th34: :: ISOMICHI:34 for A being Subset of R^1 for a, b, c being real number st A = ].-infty,a.] \/ [.b,c.] & a < b & b < c holds Int A = ].-infty,a.[ \/ ].b,c.[ proofend; begin notation let A, B be set ; antonym A,B are_c=-incomparable for A,B are_c=-comparable ; end; theorem Th35: :: ISOMICHI:35 for A, B being set holds ( A,B are_c=-incomparable or A c= B or B c< A ) proofend; definition let T be TopSpace; let A be Subset of T; attrA is 1st_class means :Def6: :: ISOMICHI:def 6 Int (Cl A) c= Cl (Int A); attrA is 2nd_class means :Def7: :: ISOMICHI:def 7 Cl (Int A) c< Int (Cl A); attrA is 3rd_class means :Def8: :: ISOMICHI:def 8 Cl (Int A), Int (Cl A) are_c=-incomparable ; end; :: deftheorem Def6 defines 1st_class ISOMICHI:def_6_:_ for T being TopSpace for A being Subset of T holds ( A is 1st_class iff Int (Cl A) c= Cl (Int A) ); :: deftheorem Def7 defines 2nd_class ISOMICHI:def_7_:_ for T being TopSpace for A being Subset of T holds ( A is 2nd_class iff Cl (Int A) c< Int (Cl A) ); :: deftheorem Def8 defines 3rd_class ISOMICHI:def_8_:_ for T being TopSpace for A being Subset of T holds ( A is 3rd_class iff Cl (Int A), Int (Cl A) are_c=-incomparable ); theorem :: ISOMICHI:36 for T being TopSpace for A being Subset of T holds ( A is 1st_class or A is 2nd_class or A is 3rd_class ) proofend; registration let T be TopSpace; cluster 1st_class -> non 2nd_class non 3rd_class for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is 1st_class holds ( not b1 is 2nd_class & not b1 is 3rd_class ) proofend; cluster 2nd_class -> non 1st_class non 3rd_class for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is 2nd_class holds ( not b1 is 1st_class & not b1 is 3rd_class ) proofend; cluster 3rd_class -> non 1st_class non 2nd_class for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is 3rd_class holds ( not b1 is 1st_class & not b1 is 2nd_class ) ; end; theorem Th37: :: ISOMICHI:37 for T being TopSpace for A being Subset of T holds ( A is 1st_class iff Border A is empty ) proofend; registration let T be TopSpace; cluster supercondensed -> 1st_class for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is supercondensed holds b1 is 1st_class proofend; cluster subcondensed -> 1st_class for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is subcondensed holds b1 is 1st_class proofend; end; definition let T be TopSpace; attrT is with_1st_class_subsets means :Def9: :: ISOMICHI:def 9 ex A being Subset of T st A is 1st_class ; attrT is with_2nd_class_subsets means :Def10: :: ISOMICHI:def 10 ex A being Subset of T st A is 2nd_class ; attrT is with_3rd_class_subsets means :Def11: :: ISOMICHI:def 11 ex A being Subset of T st A is 3rd_class ; end; :: deftheorem Def9 defines with_1st_class_subsets ISOMICHI:def_9_:_ for T being TopSpace holds ( T is with_1st_class_subsets iff ex A being Subset of T st A is 1st_class ); :: deftheorem Def10 defines with_2nd_class_subsets ISOMICHI:def_10_:_ for T being TopSpace holds ( T is with_2nd_class_subsets iff ex A being Subset of T st A is 2nd_class ); :: deftheorem Def11 defines with_3rd_class_subsets ISOMICHI:def_11_:_ for T being TopSpace holds ( T is with_3rd_class_subsets iff ex A being Subset of T st A is 3rd_class ); registration let T be non empty anti-discrete TopSpace; cluster non empty proper -> 2nd_class for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is proper & not b1 is empty holds b1 is 2nd_class proofend; end; registration let T be non trivial strict anti-discrete TopSpace; cluster 2nd_class for Element of bool the carrier of T; existence ex b1 being Subset of T st b1 is 2nd_class proofend; end; registration cluster non trivial strict TopSpace-like with_1st_class_subsets with_2nd_class_subsets for TopStruct ; existence ex b1 being TopSpace st ( b1 is with_1st_class_subsets & b1 is with_2nd_class_subsets & b1 is strict & not b1 is trivial ) proofend; cluster non empty strict TopSpace-like with_3rd_class_subsets for TopStruct ; existence ex b1 being TopSpace st ( b1 is with_3rd_class_subsets & not b1 is empty & b1 is strict ) proofend; end; registration let T be TopSpace; cluster 1st_class for Element of bool the carrier of T; existence ex b1 being Subset of T st b1 is 1st_class proofend; end; registration let T be with_2nd_class_subsets TopSpace; cluster 2nd_class for Element of bool the carrier of T; existence ex b1 being Subset of T st b1 is 2nd_class by Def10; end; registration let T be with_3rd_class_subsets TopSpace; cluster 3rd_class for Element of bool the carrier of T; existence ex b1 being Subset of T st b1 is 3rd_class by Def11; end; theorem Th38: :: ISOMICHI:38 for T being TopSpace for A being Subset of T holds ( A is 1st_class iff A ` is 1st_class ) proofend; theorem Th39: :: ISOMICHI:39 for T being TopSpace for A being Subset of T holds ( A is 2nd_class iff A ` is 2nd_class ) proofend; theorem Th40: :: ISOMICHI:40 for T being TopSpace for A being Subset of T holds ( A is 3rd_class iff A ` is 3rd_class ) proofend; registration let T be TopSpace; let A be 1st_class Subset of T; clusterA ` -> 1st_class ; coherence A ` is 1st_class by Th38; end; registration let T be with_2nd_class_subsets TopSpace; let A be 2nd_class Subset of T; clusterA ` -> 2nd_class ; coherence A ` is 2nd_class by Th39; end; registration let T be with_3rd_class_subsets TopSpace; let A be 3rd_class Subset of T; clusterA ` -> 3rd_class ; coherence A ` is 3rd_class by Th40; end; theorem Th41: :: ISOMICHI:41 for T being TopSpace for A being Subset of T st A is 1st_class holds ( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) ) proofend; theorem Th42: :: ISOMICHI:42 for T being TopSpace for A being Subset of T st ( Int (Cl A) = Int (Cl (Int A)) or Cl (Int A) = Cl (Int (Cl A)) ) holds A is 1st_class proofend; theorem Th43: :: ISOMICHI:43 for T being TopSpace for A, B being Subset of T st A is 1st_class & B is 1st_class holds ( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) ) proofend; theorem :: ISOMICHI:44 for T being TopSpace for A, B being Subset of T st A is 1st_class & B is 1st_class holds ( A \/ B is 1st_class & A /\ B is 1st_class ) proofend;