:: Components and Unions of Components
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received February 5, 1996
:: Copyright (c) 1996-2018 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;