Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Yatsuka Nakamura,
and
- Jaroslaw Kotowicz
- Received August 24, 1992
- MML identifier: JORDAN1
- [
Mizar article,
MML identifier index
]
environ
vocabulary PRE_TOPC, FUNCT_1, RELAT_1, SUBSET_1, RELAT_2, ORDINAL2, BOOLE,
RCOMP_1, BORSUK_1, FUNCOP_1, CONNSP_1, EUCLID, TOPREAL1, TOPS_2, ARYTM_1,
MCART_1, ARYTM_3, SQUARE_1, PCOMPS_1, METRIC_1, JORDAN1, ARYTM;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XREAL_0, REAL_1, RELAT_1,
NAT_1, FUNCT_1, FUNCT_2, BINOP_1, PRE_TOPC, TOPS_2, CONNSP_1, SQUARE_1,
RCOMP_1, STRUCT_0, METRIC_1, PCOMPS_1, BORSUK_1, TOPREAL1, EUCLID;
constructors REAL_1, TOPS_2, CONNSP_1, SQUARE_1, RCOMP_1, TOPMETR, TOPREAL1,
MEMBERED, NAT_1;
clusters PRE_TOPC, BORSUK_1, STRUCT_0, EUCLID, TOPREAL1, XREAL_0, RELSET_1,
MEMBERED, ZFMISC_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
for GX being TopStruct,
A being Subset of GX holds the carrier of (GX|A) = A;
theorem :: JORDAN1:2
for GX being non empty TopSpace st
(for x,y being Point of GX ex GY st (GY is connected &
ex f being map of GY,GX st
f is continuous & x in rng(f)& y in rng(f))) holds
GX is connected;
canceled;
theorem :: JORDAN1:4 ::Arcwise connectedness derives connectedness
for GX being non empty TopSpace st
(for x,y being Point of GX
ex h being map of I[01],GX st h is continuous & x=h.0 & y=h.1)
holds GX is connected;
theorem :: JORDAN1:5 ::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 map of I[01],GX|A st h is continuous & xa=h.0 & ya=h.1)
holds A is connected;
theorem :: JORDAN1:6
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:7
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:8
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 n be Nat, P be Subset of TOP-REAL n;
attr P is convex means
:: JORDAN1:def 1
for w1,w2 being Point of TOP-REAL n st w1 in P & w2 in P holds
LSeg(w1,w2) c= P;
end;
theorem :: JORDAN1:9
for n being Nat, P being Subset of TOP-REAL n st P is convex holds
P is connected;
reserve pa,pb for Point of TOP-REAL 2,
s1,t1,s2,t2,s,t,s3,t3,s4,t4,s5,t5,s6,t6,
l,lambda,sa,sd,ta,td for Real;
theorem :: JORDAN1:10
s1<s3 & s1<s4 & 0 <= l & l <= 1 implies s1<(1-l)*s3+l*s4;
theorem :: JORDAN1:11
s3<s1 & s4<s1 & 0 <= l & l <= 1 implies (1-l)*s3+l*s4<s1;
reserve s1a,t1a,s2a,t2a,s3a,t3a,sb,tb,sc,tc for Real;
theorem :: JORDAN1:12
{|[ s,t ]|: s1<s & s<s2 & t1<t & t<t2} =
{|[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2} /\ {|[s5,t5]|:t1<t5} /\
{|[s6,t6]|:t6<t2};
theorem :: JORDAN1:13
{|[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)} =
{|[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1} \/ {|[s5,t5]|:s2<s5} \/
{|[s6,t6]|:t2<t6};
theorem :: JORDAN1:14
for s1,t1,s2,t2,P st P = {|[ s,t ]|:s1<s & s<s2 & t1<t & t<t2}
holds P is convex;
theorem :: JORDAN1:15
for s1,t1,s2,t2,P st P = {|[ s,t ]|:s1<s & s<s2 & t1<t & t<t2}
holds P is connected;
theorem :: JORDAN1:16
for s1,P st P = { |[ s,t ]|:s1<s } holds P is convex;
theorem :: JORDAN1:17
for s1,P st P = { |[ s,t ]|:s1<s } holds P is connected;
theorem :: JORDAN1:18
for s2,P st P = {|[ s,t ]|:s<s2 } holds P is convex;
theorem :: JORDAN1:19
for s2,P st P = {|[ s,t ]|:s<s2 } holds P is connected;
theorem :: JORDAN1:20
for t1,P st P = {|[ s,t ]|:t1<t } holds P is convex;
theorem :: JORDAN1:21
for t1,P st P = {|[ s,t ]|:t1<t } holds P is connected;
theorem :: JORDAN1:22
for t2,P st P = { |[ s,t ]|: t<t2 } holds P is convex;
theorem :: JORDAN1:23
for t2,P st P = { |[ s,t ]|: t<t2 } holds P is connected;
theorem :: JORDAN1:24
for s1,t1,s2,t2,P st P = { |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)}
holds P is connected;
theorem :: JORDAN1:25
for s1 for P being Subset of TOP-REAL 2 st P = { |[ s,t ]|:s1<s } holds
P is open;
theorem :: JORDAN1:26
for s1 for P being Subset of TOP-REAL 2 st P = { |[ s,t ]|:s1>s } holds
P is open;
theorem :: JORDAN1:27
for s1 for P being Subset of TOP-REAL 2 st
P = { |[ s,t ]|:s1<t } holds P is open;
theorem :: JORDAN1:28
for s1 for P being Subset of TOP-REAL 2 st P = { |[ s,t ]|:s1>t } holds
P is open;
theorem :: JORDAN1:29
for s1,t1,s2,t2 for P being Subset of TOP-REAL 2 st
P = { |[ s,t ]|:s1<s & s<s2 & t1<t & t<t2} holds P is open;
theorem :: JORDAN1:30
for s1,t1,s2,t2 for P being Subset of TOP-REAL 2 st
P = { |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)} holds P is open;
theorem :: JORDAN1:31
for s1,t1,s2,t2,P,Q st
P = { |[ sa,ta ]|:s1<sa & sa<s2 & t1<ta & ta<t2} &
Q = { |[ sb,tb ]|:not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)} holds
P misses Q;
theorem :: JORDAN1:32
for s1,s2,t1,t2 be Real holds
{p where p is Point of TOP-REAL 2:s1<p`1 & p`1<s2 & t1<p`2 & p`2<t2} =
{|[sa,ta]|:s1<sa & sa<s2 & t1<ta & ta<t2};
theorem :: JORDAN1:33
for s1,s2,t1,t2 holds
{qc where qc is Point of TOP-REAL 2:
not (s1<=qc`1 & qc`1<=s2 & t1<=qc`2 & qc`2<=t2)} =
{|[sb,tb]| : not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)};
theorem :: JORDAN1:34
for s1,s2,t1,t2 holds
{ p0 where p0 is Point of TOP-REAL 2:s1<p0`1 & p0`1<s2 & t1<p0`2 & p0`2<t2}
is Subset of TOP-REAL 2;
theorem :: JORDAN1:35
for s1,s2,t1,t2 holds
{ pq where pq is Point of TOP-REAL 2:
not (s1<=pq`1 & pq`1<=s2 & t1<=pq`2 & pq`2<=t2)}
is Subset of TOP-REAL 2;
theorem :: JORDAN1:36
for s1,t1,s2,t2,P st
P = { p0 where p0 is Point of TOP-REAL 2:s1<p0`1 & p0`1<s2
& t1<p0`2 & p0`2<t2} holds P is connected;
theorem :: JORDAN1:37
for s1,t1,s2,t2,P st
P = { pq where pq is Point of TOP-REAL 2:
not (s1<=pq`1 & pq`1<=s2 & t1<=pq`2 & pq`2<=t2)} holds P is connected;
theorem :: JORDAN1:38
for s1,t1,s2,t2 for P being Subset of TOP-REAL 2 st
P = { p0 where p0 is Point of TOP-REAL 2:s1<p0`1 & p0`1<s2
& t1<p0`2 & p0`2<t2} holds P is open;
theorem :: JORDAN1:39
for s1,t1,s2,t2 for P being Subset of TOP-REAL 2 st
P = { pq where pq is Point of TOP-REAL 2:
not (s1<=pq`1 & pq`1<=s2 & t1<=pq`2 & pq`2<=t2)} holds P is open;
theorem :: JORDAN1:40
for s1,t1,s2,t2,P,Q st
P = {p where p is Point of TOP-REAL 2:s1<p`1 & p`1<s2 & t1<p`2 & p`2<t2} &
Q = {qc where qc is Point of TOP-REAL 2:
not (s1<=qc`1 & qc`1<=s2 & t1<=qc`2 & qc`2<=t2)}
holds P misses Q;
theorem :: JORDAN1:41
for s1,t1,s2,t2 for P,P1,P2 being Subset of TOP-REAL 2 st s1<s2 & t1<t2 &
P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= 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<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} &
P2 = {pb where pb is Point of TOP-REAL 2:
not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)} holds
P`= P1 \/ P2 & P`<> {} & P1 misses P2 &
for P1A,P2B being Subset of (TOP-REAL 2)|P`
st P1A = P1 & P2B = P2 holds
P1A is_a_component_of (TOP-REAL 2)|P` & P2B is_a_component_of (TOP-REAL 2)|P`
;
theorem :: JORDAN1:42
for s1,t1,s2,t2 for P,P1,P2 being Subset of TOP-REAL 2 st s1<s2 & t1<t2 &
P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= 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<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} &
P2 = {pb where pb is Point of TOP-REAL 2:
not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)}
holds P = (Cl P1) \ P1 & P = (Cl P2) \P2;
theorem :: JORDAN1:43
for s1,s2,t1,t2,P,P1 st P = { p where p is Point of TOP-REAL 2:
p`1 = s1 & p`2 <= t2 & p`2 >= 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<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} holds
P1 c= [#] ((TOP-REAL 2)|P`);
theorem :: JORDAN1:44
for s1,s2,t1,t2,P,P1 st P = { p where p is Point of TOP-REAL 2:
p`1 = s1 & p`2 <= t2 & p`2 >= 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<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} holds
P1 is Subset of (TOP-REAL 2)|P`;
theorem :: JORDAN1:45
for s1,s2,t1,t2,P,P2 st s1<s2 & t1<t2 &
P = { p where p is Point of TOP-REAL 2:
p`1 = s1 & p`2 <= t2 & p`2 >= 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:46
for s1,s2,t1,t2,P,P2 st s1<s2 & t1< t2 &
P = { p where p is Point of TOP-REAL 2:
p`1 = s1 & p`2 <= t2 & p`2 >= 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_of (TOP-REAL 2)|S` &
C2 is_a_component_of (TOP-REAL 2)|S`;
synonym S has_property_J;
end;
theorem :: JORDAN1:47
for S being Subset of TOP-REAL 2 st S has_property_J 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_of (TOP-REAL 2)|S` &
C2 is_a_component_of (TOP-REAL 2)|S` &
for C3 being Subset of (TOP-REAL 2)|S` st
C3 is_a_component_of (TOP-REAL 2)|S` holds C3 = C1 or C3 = C2;
theorem :: JORDAN1:48
for s1,s2,t1,t2 for P being Subset of TOP-REAL 2 st s1<s2 & t1<t2 &
P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= 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 has_property_J;
Back to top