Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users

### The Cantor Set

by
Alexander Yu. Shibakov, and
Andrzej Trybulec

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

```