The abstract of the Mizar article:

Connected Spaces

by

Beata Padlewska

Received May 6, 1989

MML identifier: CONNSP_1

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, BOOLE, SUBSET_1, RELAT_2, ORDINAL2, RELAT_1, TOPS_1,
      SETFAM_1, TARSKI, CONNSP_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, STRUCT_0, PRE_TOPC, TOPS_1;
 constructors TOPS_1, MEMBERED;
 clusters PRE_TOPC, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1;
 requirements SUBSET, BOOLE;


begin
 reserve GX for TopSpace;
 reserve A, B, C for Subset of GX;
 reserve TS for TopStruct;
 reserve K, K1, L, L1 for Subset of TS;

::
::                         Separated sets
::

definition let GX be TopStruct, A,B be Subset of GX;
 pred A,B are_separated means
:: CONNSP_1:def 1
    Cl A misses B & A misses Cl B;
 symmetry;
end;

canceled;

theorem :: CONNSP_1:2
  K,L are_separated implies K misses L;

theorem :: CONNSP_1:3
 [#]TS = K \/ L & K is closed & L is closed & K misses L
  implies K,L are_separated;

theorem :: CONNSP_1:4
 [#]GX = A \/ B & A is open & B is open & A misses B
  implies A,B are_separated;

theorem :: CONNSP_1:5
  [#]GX = A \/ B & A,B are_separated implies
        A is open closed & B is open closed;

theorem :: CONNSP_1:6
  for X' being SubSpace of GX, P1,Q1 being Subset of GX,
  P,Q being Subset of X' st P=P1 & Q=Q1 holds
  P,Q are_separated implies P1,Q1 are_separated;

theorem :: CONNSP_1:7
  for X' being SubSpace of GX, P,Q being Subset of GX,
  P1,Q1 being Subset of X' st P=P1 & Q=Q1 & P \/ Q c= [#](X')
  holds P,Q are_separated implies P1,Q1 are_separated;

theorem :: CONNSP_1:8
  K,L are_separated & K1 c= K & L1 c= L implies
  K1,L1 are_separated;

theorem :: CONNSP_1:9
  A,B are_separated & A,C are_separated implies A,B \/ C are_separated;

theorem :: CONNSP_1:10
  (K is closed & L is closed) or (K is open & L is open)
   implies K \ L,L \ K are_separated;

::
::                        Connected Spaces
::

definition let GX be TopStruct;
  attr GX is connected means
:: CONNSP_1:def 2
    for A, B being Subset of GX st
          [#]GX = A \/ B & A,B are_separated
          holds A = {}GX or B = {}GX;
end;

theorem :: CONNSP_1:11
 GX is connected iff for A, B being Subset of GX
  st [#]GX = A \/ B & A <> {}GX & B <> {}GX & A is closed &
  B is closed holds A meets B;

theorem :: CONNSP_1:12
    GX is connected iff for A,B being Subset of GX
  st [#]GX = A \/ B & A <> {}GX & B <> {}GX & A is open &
  B is open holds A meets B;

theorem :: CONNSP_1:13
  GX is connected iff for A being Subset of GX st A <> {}GX
  & A <> [#]GX holds Cl A meets Cl([#]GX \ A);

theorem :: CONNSP_1:14
    GX is connected iff for A being Subset of GX st A is open closed holds
   A = {}GX or A = [#]GX;

theorem :: CONNSP_1:15
    for GY being TopSpace
  for F being map of GX,GY st F is continuous
  & F.:[#]GX = [#]GY & GX is connected holds GY is connected;

::
::                          Connected Sets
::

definition let GX be TopStruct, A be Subset of GX;
  attr A is connected means
:: CONNSP_1:def 3
    GX|A is connected;
end;

theorem :: CONNSP_1:16
  A is connected
  iff for P,Q being Subset of GX st A = P \/ Q &
  P,Q are_separated holds P = {}GX or Q = {}GX;

theorem :: CONNSP_1:17
  A is connected & A c= B \/ C & B,C are_separated implies
  A c= B or A c= C;

theorem :: CONNSP_1:18
  A is connected & B is connected & not A,B are_separated
  implies A \/ B is connected;

theorem :: CONNSP_1:19
  C is connected & C c= A & A c= Cl C implies A is connected;

theorem :: CONNSP_1:20
  A is connected implies Cl A is connected;

theorem :: CONNSP_1:21
  GX is connected & A is connected & [#]GX \ A = B \/ C &
  B,C are_separated implies A \/ B is connected & A \/ C is connected;

theorem :: CONNSP_1:22
    [#]GX \ A = B \/ C & B,C are_separated & A is closed implies
  A \/ B is closed & A \/ C is closed;

theorem :: CONNSP_1:23
    C is connected & C meets A & C \ A <> {}GX implies C meets Fr A;

theorem :: CONNSP_1:24
  for X' being SubSpace of GX,
      A being Subset of GX,
      B being Subset of X' st A = B
   holds A is connected iff B is connected;

theorem :: CONNSP_1:25
   A is closed & B is closed & A \/ B is connected & A /\ B is connected
implies
  A is connected & B is connected;

theorem :: CONNSP_1:26
  for F being Subset-Family of GX st
  (for A being Subset of GX st A in F holds A is connected)
  & (ex A being Subset of GX st A <> {}GX & A in F &
  (for B being Subset of GX st B in F & B <> A holds
  not A,B are_separated)) holds union F is connected;

theorem :: CONNSP_1:27
  for F being Subset-Family of GX st
  (for A being Subset of GX st A in F holds A is connected)
  & meet F <> {}GX holds union F is connected;

theorem :: CONNSP_1:28
   :: do poprawienia, przy poprawnej definicji "connected" !!!
 [#]GX is connected iff GX is connected;

theorem :: CONNSP_1:29
  for GX being non empty TopSpace
  for x being Point of GX holds {x} is connected;

definition let GX be TopStruct, x,y be Point of GX;
  pred x, y are_joined means
:: CONNSP_1:def 4
ex C being Subset of GX st C is connected & x in C & y in C;
end;

theorem :: CONNSP_1:30
 for GX being non empty TopSpace st
  ex x being Point of GX st for y being Point of GX holds x,y are_joined
   holds GX is connected;

theorem :: CONNSP_1:31
  (ex x being Point of GX st for y being Point of GX holds
   x,y are_joined)
   iff (for x,y being Point of GX holds x,y are_joined);

theorem :: CONNSP_1:32
   for GX being non empty TopSpace st
  for x, y being Point of GX holds x,y are_joined holds
   GX is connected;

theorem :: CONNSP_1:33
  for GX being non empty TopSpace
  for x being Point of GX, F being Subset-Family of GX
  st for A being Subset of GX holds A in F iff A is connected & x in A
  holds F <> {};

::
::              Components of Topological Spaces
::

definition let GX be TopStruct, A be Subset of GX;
   pred A is_a_component_of GX means
:: CONNSP_1:def 5
    A is connected & for B being Subset of GX st
           B is connected holds A c= B implies A = B;
end;

theorem :: CONNSP_1:34
 for GX being non empty TopSpace, A being Subset of GX
  st A is_a_component_of GX holds A <> {}GX;

theorem :: CONNSP_1:35
    A is_a_component_of GX implies A is closed;

theorem :: CONNSP_1:36
  A is_a_component_of GX & B is_a_component_of GX implies
  A = B or A,B are_separated;

theorem :: CONNSP_1:37
  A is_a_component_of GX & B is_a_component_of GX implies
  A = B or A misses B;

theorem :: CONNSP_1:38
    C is connected implies
  for S being Subset of GX st S is_a_component_of GX holds
               C misses S or C c= S;

definition let GX be TopStruct, A, B be Subset of GX;
   pred B is_a_component_of A means
:: CONNSP_1:def 6
    ex B1 being Subset of GX|A st B1 = B & B1 is_a_component_of GX|A;
end;

theorem :: CONNSP_1:39
    GX is connected & A is connected & C is_a_component_of [#]GX \ A implies
   [#]GX \ C is connected;

::
::                    A Component of a Point
::

definition let GX be TopStruct, x be Point of GX;
  func skl x -> Subset of GX means
:: CONNSP_1:def 7
   ex F being Subset-Family of GX st
      (for A being Subset of GX holds A in F iff A is connected & x in A) &
      union F = it;
end;

reserve GX for non empty TopSpace;
reserve A, C for Subset of GX;
reserve x for Point of GX;

theorem :: CONNSP_1:40
  x in skl x;

theorem :: CONNSP_1:41
  skl x is connected;

theorem :: CONNSP_1:42
 C is connected & skl x c= C implies C = skl x;

theorem :: CONNSP_1:43
 A is_a_component_of GX iff ex x being Point of GX st A = skl x;

theorem :: CONNSP_1:44
    A is_a_component_of GX & x in A implies A = skl x;

theorem :: CONNSP_1:45
    A = skl x implies
   for p being Point of GX st p in A holds skl p = A;

theorem :: CONNSP_1:46
   for F being Subset-Family of GX st for A being Subset of GX
 holds A in F iff A is_a_component_of GX
 holds F is_a_cover_of GX;