Volume 7, 1995

University of Bialystok

Copyright (c) 1995 Association of Mizar Users

### The abstract of the Mizar article:

### The Cantor Set

**by****Alexander Yu. Shibakov, and****Andrzej Trybulec**- Received January 9, 1995
- MML identifier: CANTOR_1

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCOP_1, ZF_REFLE, BOOLE, RELAT_1, SETFAM_1, TARSKI, PRE_TOPC, FINSET_1, SETWISEO, FINSUB_1, FUNCT_1, SUBSET_1, CARD_3, CANTOR_1, RLVECT_3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, NAT_1, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, FINSUB_1, SETWISEO, STRUCT_0, PRE_TOPC, TOPS_2, CARD_3, FUNCOP_1; constructors SETWISEO, TOPS_2, PRVECT_1, MEMBERED, XBOOLE_0; clusters PRE_TOPC, PRVECT_1, FINSET_1, COMPLSP1, FUNCOP_1, RELSET_1, SUBSET_1, SETFAM_1, FRAENKEL, MEMBERED, ZFMISC_1, XBOOLE_0; requirements BOOLE, SUBSET; begin definition let Y be set; let x be non empty set; cluster Y --> x -> non-empty; end; 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; mode Basis of X -> Subset-Family of X means :: CANTOR_1:def 2 it c= the topology of X & the topology of X c= UniCl it; 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 M be set; let B be Subset-Family of M; func Intersect(B) -> Subset of M equals :: CANTOR_1:def 3 meet B if B <> {} otherwise M; end; definition let X be set; let A be Subset-Family of X; func FinMeetCl(A) -> Subset-Family of X means :: CANTOR_1:def 4 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; definition let T be non empty TopSpace; cluster the topology of T -> non empty; end; 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 Subset-Family of X for x being set st x in X holds x in Intersect R iff for Y being set st Y in R holds x in Y; theorem :: CANTOR_1:11 for X being set for H, J being Subset-Family of X st H c= J holds Intersect J c= Intersect H; definition let X be set, R be Subset-Family of bool X; redefine mode Element of R -> Subset-Family of X; redefine func union R -> Subset-Family of X; end; theorem :: CANTOR_1:12 for X being set for R being non empty Subset-Family of bool X, F being Subset-Family of X st F = { Intersect x where x is Element of R: not contradiction} holds Intersect F = Intersect union R; definition let X, Y be set; let A be Subset-Family of X; let F be Function of Y, bool A; let x be set; redefine func F.x -> Subset-Family of X; end; theorem :: CANTOR_1:13 for X be set, A be Subset-Family of X holds FinMeetCl A = FinMeetCl FinMeetCl A; theorem :: CANTOR_1:14 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:15 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:16 for X being set, A,B being Subset-Family of X holds A c= B implies FinMeetCl A c= FinMeetCl B; definition let X be set; let A be Subset-Family of X; cluster FinMeetCl(A) -> non empty; end; theorem :: CANTOR_1:17 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; mode prebasis of X -> Subset-Family of X means :: CANTOR_1:def 5 it c= the topology of X & ex F being Basis of X st F c= FinMeetCl it; end; theorem :: CANTOR_1:18 for X being non empty set, Y being Subset-Family of X holds Y is Basis of TopStruct (#X, UniCl Y#); theorem :: CANTOR_1:19 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:20 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 6 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

Back to top