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