:: The Cantor Set :: by Alexander Yu. Shibakov and Andrzej Trybulec :: :: Received January 9, 1995 :: Copyright (c) 1995-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 SETFAM_1, SUBSET_1, TARSKI, PRE_TOPC, RCOMP_1, RLVECT_3, FINSET_1, XBOOLE_0, FINSUB_1, SETWISEO, ZFMISC_1, STRUCT_0, FUNCT_1, RELAT_1, CARD_3, NUMBERS, FUNCOP_1, CARD_1, NAT_1, CANTOR_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, NAT_1, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, FINSUB_1, SETWISEO, PROB_1, STRUCT_0, PRE_TOPC, TOPS_2, CARD_3, FUNCOP_1; constructors SETFAM_1, FUNCOP_1, SETWISEO, CARD_3, TOPS_2, RELSET_1, PROB_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCOP_1, FINSET_1, CARD_3, PRE_TOPC, FUNCT_1, TOPS_2; requirements BOOLE, SUBSET; begin definition let X be set; let A be Subset-Family of X; func UniCl(A) -> Subset-Family of X means :: CANTOR_1:def 1 for x being Subset of X holds x in it iff ex Y being Subset-Family of X st Y c=A & x = union Y; end; definition let X be TopStruct, F be Subset-Family of X; attr F is quasi_basis means :: CANTOR_1:def 2 the topology of X c= UniCl F; end; registration let X be TopStruct; cluster the topology of X -> quasi_basis; end; registration let X be TopStruct; cluster open quasi_basis for Subset-Family of X; end; definition let X be TopStruct; mode Basis of X is open quasi_basis Subset-Family of X; end; theorem :: CANTOR_1:1 for X being set for A being Subset-Family of X holds A c= UniCl A; theorem :: CANTOR_1:2 for S being TopStruct holds the topology of S is Basis of S; theorem :: CANTOR_1:3 for S being TopStruct holds the topology of S is open; definition let X be set; let A be Subset-Family of X; func FinMeetCl(A) -> Subset-Family of X means :: CANTOR_1:def 3 for x being Subset of X holds x in it iff ex Y being Subset-Family of X st Y c= A & Y is finite & x = Intersect Y; end; theorem :: CANTOR_1:4 for X being set for A being Subset-Family of X holds A c= FinMeetCl A; theorem :: CANTOR_1:5 for T being non empty TopSpace holds the topology of T = FinMeetCl the topology of T; theorem :: CANTOR_1:6 for T being TopSpace holds the topology of T = UniCl the topology of T; theorem :: CANTOR_1:7 for T being non empty TopSpace holds the topology of T = UniCl FinMeetCl the topology of T; theorem :: CANTOR_1:8 for X being set, A being Subset-Family of X holds X in FinMeetCl A; theorem :: CANTOR_1:9 for X being set for A, B being Subset-Family of X holds A c= B implies UniCl A c= UniCl B; theorem :: CANTOR_1:10 for X being set for R being non empty Subset-Family of bool X, F being Subset-Family of X st F = the set of all Intersect x where x is Element of R holds Intersect F = Intersect union R; theorem :: CANTOR_1:11 for X be set, A be Subset-Family of X holds FinMeetCl A = FinMeetCl FinMeetCl A; theorem :: CANTOR_1:12 for X being set, A being Subset-Family of X, a, b being set st a in FinMeetCl A & b in FinMeetCl A holds a /\ b in FinMeetCl A; theorem :: CANTOR_1:13 for X being set, A being Subset-Family of X, a, b being set st a c= FinMeetCl A & b c= FinMeetCl A holds INTERSECTION(a,b) c= FinMeetCl A; theorem :: CANTOR_1:14 for X being set, A,B being Subset-Family of X holds A c= B implies FinMeetCl A c= FinMeetCl B; registration let X be set; let A be Subset-Family of X; cluster FinMeetCl(A) -> non empty; end; theorem :: CANTOR_1:15 for X be non empty set, A be Subset-Family of X holds TopStruct (#X,UniCl FinMeetCl A#) is TopSpace-like; definition let X be TopStruct, F be Subset-Family of X; attr F is quasi_prebasis means :: CANTOR_1:def 4 ex G being Basis of X st G c= FinMeetCl F; end; registration let X be TopStruct; cluster the topology of X -> quasi_prebasis; cluster -> quasi_prebasis for Basis of X; cluster open quasi_prebasis for Subset-Family of X; end; definition let X be TopStruct; mode prebasis of X is open quasi_prebasis Subset-Family of X; end; theorem :: CANTOR_1:16 for X being non empty set, Y being Subset-Family of X holds Y is Basis of TopStruct (#X, UniCl Y#); theorem :: CANTOR_1:17 for T1, T2 being strict non empty TopSpace, P being prebasis of T1 st the carrier of T1 = the carrier of T2 & P is prebasis of T2 holds T1 = T2 ; theorem :: CANTOR_1:18 for X being non empty set, Y being Subset-Family of X holds Y is prebasis of TopStruct (#X, UniCl FinMeetCl Y#); definition func the_Cantor_set -> strict non empty TopSpace means :: CANTOR_1:def 5 the carrier of it = product (NAT-->{0,1}) & ex P being prebasis of it st for X being Subset of product (NAT-->{0,1}) holds X in P iff ex N,n being Nat st for F being Element of product (NAT-->{0,1}) holds F in X iff F.N=n; end; :: the aim is to prove: theorem the_Cantor_set is compact