:: 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-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 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 & s<s2 & t1<t & t<t2} =
  {|[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2} /\ {|[s5,t5]|:t1<t5} /\
  {|[s6,t6]|:t6<t2};

theorem :: JORDAN1:8
  {|[ 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:9
  for s1,t1,s2,t2,P st P = {|[ s,t ]|:s1<s & s<s2 & t1<t & t<t2}
  holds P is convex;

::$CT

theorem :: JORDAN1:11
  for s1,P st P = { |[ s,t ]|:s1<s } holds P is convex;

::$CT

theorem :: JORDAN1:13
  for s2,P st P = {|[ s,t ]|:s<s2 } holds P is convex;

::$CT

theorem :: JORDAN1:15
  for t1,P st P = {|[ s,t ]|:t1<t } holds P is convex;

::$CT

theorem :: JORDAN1:17
  for t2,P st P = { |[ s,t ]|: t<t2 } holds P is convex;

::$CT

theorem :: JORDAN1:19
  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:20
  for s1 holds { |[ s,t ]|:s1<s } is open Subset of TOP-REAL 2;

theorem :: JORDAN1:21
  for s1 holds { |[ s,t ]|:s1>s } is open Subset of TOP-REAL 2;

theorem :: JORDAN1:22
  for s1 holds { |[ s,t ]|:s1<t } is open Subset of TOP-REAL 2;

theorem :: JORDAN1:23
  for s1 holds { |[ s,t ]|:s1>t } is open Subset of TOP-REAL 2;

theorem :: JORDAN1:24
  for s1,t1,s2,t2 holds
  { |[ s,t ]|:s1<s & s<s2 & t1<t & t<t2} is open Subset of TOP-REAL 2;

theorem :: JORDAN1:25
  for s1,t1,s2,t2 holds
{ |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)} is open Subset of TOP-REAL 2;

theorem :: JORDAN1:26
  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:27
  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:28
  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:29
  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:30
  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:31
  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 convex;

theorem :: JORDAN1:32
  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:33
  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:34
  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:35
  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:36
  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 & P2B is a_component;

theorem :: JORDAN1:37
  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:38
  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:39
  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:40
  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:41
  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 & 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<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 is Jordan;

theorem :: JORDAN1:44
  for s1,t1,s2,t2 for P,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} &
  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<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} holds Cl P1 = P \/ P1;

:: Moved from JORDAN1H, AK, 22.02.2006

theorem :: JORDAN1:46
  for p,q being Point of TOP-REAL 2 holds LSeg(p,q) \ {p,q} is convex;

registration
  let p be Point of TOP-REAL 2;
  cluster north_halfline p -> convex;
  cluster east_halfline p -> convex;
  cluster south_halfline p -> convex;
  cluster west_halfline p -> convex;
end;