:: The Jordan's Property for Certain Subsets of the Plane
:: by Yatsuka Nakamura and Jaros{\l}aw Kotowicz
::
:: Received August 24, 1992
:: Copyright (c) 1992-2017 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 NUMBERS, XBOOLE_0, PRE_TOPC, REAL_1, CARD_1, XXREAL_1, XXREAL_0,
FUNCT_1, BORSUK_1, ORDINAL2, RELAT_2, RELAT_1, SUBSET_1, FUNCOP_1,
CONNSP_1, EUCLID, RLVECT_1, CONVEX1, RLTOPSP1, TARSKI, TOPREAL1, TOPS_2,
STRUCT_0, ARYTM_3, MCART_1, ARYTM_1, PCOMPS_1, RCOMP_1, METRIC_1,
SQUARE_1, JORDAN1, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XXREAL_0, XCMPLX_0, XREAL_0,
REAL_1, FUNCT_1, RELSET_1, FUNCT_2, BINOP_1, NUMBERS, PRE_TOPC, TOPS_2,
CONNSP_1, SQUARE_1, RCOMP_1, STRUCT_0, METRIC_1, PCOMPS_1, BORSUK_1,
TOPREAL1, RLVECT_1, RLTOPSP1, EUCLID;
constructors REAL_1, SQUARE_1, RCOMP_1, CONNSP_1, TOPS_2, TOPMETR, TOPREAL1,
FUNCOP_1, FUNCSDOM, CONVEX1, BINOP_2, PCOMPS_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XREAL_0, MEMBERED, STRUCT_0,
PRE_TOPC, BORSUK_1, EUCLID, RLTOPSP1, SQUARE_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin
::
:: Selected theorems on connected space
::
reserve GX,GY for non empty TopSpace,
x,y for Point of GX,
r,s for Real;
theorem :: JORDAN1:1 ::Arcwise connectedness derives connectedness
for GX being non empty TopSpace st (for x,y being Point of GX
ex h being Function of I[01],GX st h is continuous & x=h.0 & y=h.1)
holds GX is connected;
theorem :: JORDAN1:2 ::Arcwise connectedness derives connectedness for subset
for A being Subset of GX st
(for xa,ya being Point of GX st xa in A & ya in A & xa<>ya
ex h being Function of I[01],GX|A st h is continuous & xa=h.0 & ya=h.1)
holds A is connected;
theorem :: JORDAN1:3
for A0 being Subset of GX, A1 being Subset of GX st
A0 is connected & A1 is connected & A0 meets A1
holds A0 \/ A1 is connected;
theorem :: JORDAN1:4
for A0,A1,A2 being Subset of GX st
A0 is connected & A1 is connected & A2 is connected & A0 meets A1 &
A1 meets A2 holds A0 \/ A1 \/ A2 is connected;
theorem :: JORDAN1:5
for A0,A1,A2,A3 being Subset of GX st A0 is connected & A1 is connected &
A2 is connected & A3 is connected & A0 meets A1 & A1 meets A2 &
A2 meets A3 holds A0 \/ A1 \/ A2 \/ A3 is connected;
begin
::
:: Certain connected and open subsets in the Euclidean plane
::
reserve Q,P1,P2 for Subset of TOP-REAL 2;
reserve P for Subset of TOP-REAL 2;
reserve w1,w2 for Point of TOP-REAL 2;
definition
let V be RealLinearSpace, P be Subset of V;
redefine attr P is convex means
:: JORDAN1:def 1
for w1,w2 being Element of V st w1 in P & w2 in P holds LSeg(w1,w2) c= P;
end;
registration let n be Nat;
cluster convex -> connected for Subset of TOP-REAL n;
end;
reserve pa,pb for Point of TOP-REAL 2,
s1,t1,s2,t2,s,t,s3,t3,s4,t4,s5,t5,s6,t6, l,sa,sd,ta,td for Real;
reserve s1a,t1a,s2a,t2a,s3a,t3a,sb,tb,sc,tc for Real;
::$CT
theorem :: JORDAN1:7
{|[ s,t ]|: s1~~s } is open Subset of TOP-REAL 2;
theorem :: JORDAN1:22
for s1 holds { |[ s,t ]|:s1t } is open Subset of TOP-REAL 2;
theorem :: JORDAN1:24
for s1,t1,s2,t2 holds
{ |[ s,t ]|:s1~~~~= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P1 = {pa where pa is Point of TOP-REAL 2:
s1 {} & P1 misses P2 &
for P1A,P2B being Subset of (TOP-REAL 2)|P` st P1A = P1 & P2B = P2 holds
P1A is a_component & P2B is a_component;
theorem :: JORDAN1:37
for s1,t1,s2,t2 for P,P1,P2 being Subset of TOP-REAL 2 st s1= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P1 = {pa where pa is Point of TOP-REAL 2:
s1= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P1 = {pa where pa is Point of TOP-REAL 2:
s1= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P1 = {pa where pa is Point of TOP-REAL 2:
s1= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P2 = {pb where pb is Point of TOP-REAL 2:
not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)} holds
P2 c= [#]((TOP-REAL 2)|P`);
theorem :: JORDAN1:41
for s1,s2,t1,t2,P,P2 st s1= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P2 = {pb where pb is Point of TOP-REAL 2:
not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)} holds
P2 is Subset of (TOP-REAL 2)|P`;
begin
::
:: The Jordan's property
::
definition
let S be Subset of TOP-REAL 2;
attr S is Jordan means
:: JORDAN1:def 2
S`<> {} & ex A1,A2 being Subset of TOP-REAL 2 st
S` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 &
for C1,C2 being Subset of (TOP-REAL 2)|S` st C1 = A1 & C2 = A2 holds
C1 is a_component & C2 is a_component;
end;
theorem :: JORDAN1:42
for S being Subset of TOP-REAL 2 st S is Jordan holds S`<> {} &
ex A1,A2 being Subset of TOP-REAL 2 st
ex C1,C2 being Subset of (TOP-REAL 2)|S` st S` = A1 \/ A2 & A1 misses A2 &
(Cl A1) \ A1 = (Cl A2) \ A2 & C1 = A1 & C2 = A2 &
C1 is a_component & C2 is a_component &
for C3 being Subset of (TOP-REAL 2)|S` st C3 is a_component holds
C3 = C1 or C3 = C2;
theorem :: JORDAN1:43
for s1,s2,t1,t2 for P being Subset of TOP-REAL 2 st s1= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} holds P is Jordan;
theorem :: JORDAN1:44
for s1,t1,s2,t2 for P,P2 being Subset of TOP-REAL 2 st s1= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P2 = {pb where pb is Point of TOP-REAL 2:
not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)}
holds Cl P2 = P \/ P2;
theorem :: JORDAN1:45
for s1,t1,s2,t2 for P,P1 being Subset of TOP-REAL 2 st s1= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P1 = {pa where pa is Point of TOP-REAL 2:
s1 convex;
cluster east_halfline p -> convex;
cluster south_halfline p -> convex;
cluster west_halfline p -> convex;
end;
~~