:: Components and Unions of Components
::  by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received February 5, 1996
:: Copyright (c) 1996-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 XBOOLE_0, PRE_TOPC, SUBSET_1, CONNSP_1, SETFAM_1, RELAT_2,
      TARSKI, STRUCT_0, ZFMISC_1, RELAT_1, RUSUB_4, RCOMP_1, CONNSP_3;
 notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, STRUCT_0, PRE_TOPC, CONNSP_1;
 constructors SETFAM_1, CONNSP_1;
 registrations SUBSET_1, STRUCT_0, PRE_TOPC, CONNSP_1;
 requirements SUBSET, BOOLE;


begin :: The component of a subset in a topological space

reserve x,X,X2,Y,Y2 for set;
reserve GX for non empty TopSpace;
reserve A2,B2 for Subset of GX;
reserve B for Subset of GX;

definition
  let GX be TopStruct, V be Subset of GX;
  func Component_of V -> Subset of GX means
:: CONNSP_3:def 1

  ex F being Subset-Family of GX st
  (for A being Subset of GX holds A in F iff A is connected & V c= A) &
  union F = it;
end;

theorem :: CONNSP_3:1
  for GX being TopSpace, V being Subset of GX st (ex A being Subset
  of GX st A is connected & V c= A) holds V c= Component_of V;

theorem :: CONNSP_3:2
  for GX being TopSpace, V being Subset of GX st (not ex A being Subset
  of GX st A is connected & V c= A) holds Component_of V = {};

theorem :: CONNSP_3:3
  Component_of {}GX = the carrier of GX;

theorem :: CONNSP_3:4
  for V being Subset of GX st V is connected holds Component_of V <>{};

theorem :: CONNSP_3:5
  for GX being TopSpace, V being Subset of GX st V is connected & V
  <> {} holds Component_of V is connected;

theorem :: CONNSP_3:6
  for V,C being Subset of GX st V is connected & C is connected
  holds Component_of V c= C implies C = Component_of V;

theorem :: CONNSP_3:7
  for A being Subset of GX st A is a_component holds Component_of A=A;

theorem :: CONNSP_3:8
  for A being Subset of GX holds A is a_component iff ex V
  being Subset of GX st V is connected & V <> {} & A = Component_of V;

theorem :: CONNSP_3:9
  for V being Subset of GX st V is connected & V<>{} holds Component_of
  V is a_component;

theorem :: CONNSP_3:10
  for A, V be Subset of GX st A is a_component & V is connected &
  V c= A & V<>{} holds A = Component_of V;

theorem :: CONNSP_3:11
  for V being Subset of GX st V is connected & V<>{} holds
  Component_of (Component_of V)=Component_of V;

theorem :: CONNSP_3:12
  for A,B being Subset of GX st A is connected & B is connected &
  A<>{} & A c= B holds Component_of A = Component_of B;

theorem :: CONNSP_3:13
  for A,B being Subset of GX st A is connected & B is connected &
  A<>{} & A c= B holds B c= Component_of A;

theorem :: CONNSP_3:14
  for A being Subset of GX,B being Subset of GX st A is connected
  & A \/ B is connected & A<>{} holds A \/ B c= Component_of A;

theorem :: CONNSP_3:15
  for A being Subset of GX, p being Point of GX st A is connected
  & p in A holds Component_of p=Component_of A;

theorem :: CONNSP_3:16
  for A,B being Subset of GX st A is connected & B is connected & A
  meets B holds A \/ B c= Component_of A & A \/ B c= Component_of B & A c=
  Component_of B & B c= Component_of A;

theorem :: CONNSP_3:17
  for A being Subset of GX st A is connected & A<>{} holds Cl A c=
  Component_of A;

theorem :: CONNSP_3:18
  for A,B being Subset of GX st A is a_component & B is connected
  & B<>{} & A misses B holds A misses Component_of B;

begin

definition
  let GX be TopStruct;
  mode a_union_of_components of GX -> Subset of GX means
:: CONNSP_3:def 2

    ex F being
    Subset-Family of GX st (for B being Subset of GX st B in F holds B
    is a_component) & it = union F;
end;

theorem :: CONNSP_3:19
  {}(GX) is a_union_of_components of GX;

theorem :: CONNSP_3:20
  for A being Subset of GX st A=(the carrier of GX) holds A is
  a_union_of_components of GX;

theorem :: CONNSP_3:21
  for A being Subset of GX,p being Point of GX st p in A & A is
  a_union_of_components of GX holds Component_of p c= A;

theorem :: CONNSP_3:22
  for A,B being Subset of GX st A is a_union_of_components of GX & B is
a_union_of_components of GX holds A \/ B is a_union_of_components of GX & A /\
  B is a_union_of_components of GX;

theorem :: CONNSP_3:23
  for Fu being Subset-Family of GX st (for A being Subset of GX st A in
  Fu holds A is a_union_of_components of GX) holds union Fu is
  a_union_of_components of GX;

theorem :: CONNSP_3:24
  for Fu being Subset-Family of GX st (for A being Subset of GX st A in
  Fu holds A is a_union_of_components of GX) holds meet Fu is
  a_union_of_components of GX;

theorem :: CONNSP_3:25
  for A,B being Subset of GX st A is a_union_of_components of GX & B is
  a_union_of_components of GX holds A \ B is a_union_of_components of GX;

begin :: Operations Down and Up

definition
  let GX be TopStruct, B be Subset of GX, p be Point of GX;
  assume
 p in B;
  func Down(p,B) -> Point of GX|B equals
:: CONNSP_3:def 3

  p;
end;

definition
  let GX be TopStruct, B be Subset of GX, p be Point of GX|B;
  assume
 B<>{};
  func Up(p) -> Point of GX equals
:: CONNSP_3:def 4
  p;
end;

definition
  let GX be TopStruct, V,B be Subset of GX;
  func Down(V,B) -> Subset of GX|B equals
:: CONNSP_3:def 5
  V /\ B;
end;

definition
  let GX be TopStruct, B be Subset of GX;
  let V be Subset of GX|B;
  func Up(V) -> Subset of GX equals
:: CONNSP_3:def 6
  V;
end;

definition
  let GX be TopStruct, B be Subset of GX, p be Point of GX;
  assume
 p in B;
  func Component_of(p,B) -> Subset of GX means
:: CONNSP_3:def 7

  for q being Point of GX| B st q=p holds it=Component_of q;
end;

theorem :: CONNSP_3:26
  for B being Subset of GX, p be Point of GX st p in B holds p in
  Component_of(p,B);

theorem :: CONNSP_3:27
  for B being Subset of GX, p be Point of GX st p in B holds
  Component_of(p,B)=Component_of Down(p,B);

theorem :: CONNSP_3:28
  for GX being TopSpace for V,B being Subset of GX st V is open holds
  Down(V,B) is open;

theorem :: CONNSP_3:29
  for V,B being Subset of GX st V c= B holds Cl Down(V,B) =(Cl V) /\ B;

theorem :: CONNSP_3:30
  for B being Subset of GX,V being Subset of GX| B holds Cl V =(Cl Up(V) ) /\ B
;

theorem :: CONNSP_3:31
  for V,B being Subset of GX st V c= B holds Cl Down(V,B) c= Cl V;

theorem :: CONNSP_3:32
  for B being Subset of GX, V being Subset of GX|B st V c= B holds Down(
  Up(V),B)=V;

theorem :: CONNSP_3:33
  for B being Subset of GX, p be Point of GX st p in B holds
  Component_of(p,B) is connected;

:: Moved from JORDAN1B, AK, 22.02.2006

registration
  let T be non empty TopSpace;
  cluster non empty for a_union_of_components of T;
end;

theorem :: CONNSP_3:34
  for T being non empty TopSpace for A being non empty
  a_union_of_components of T st A is connected holds A is a_component;