:: 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