:: by Andrzej Trybulec and Yatsuka Nakamura

::

:: Received September 16, 2002

:: Copyright (c) 2002-2021 Association of Mizar Users

theorem Th2: :: JORDAN16:2

for A being Subset of (TOP-REAL 2)

for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds Segment (A,p1,p2,q1,q2) c= A

for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds Segment (A,p1,p2,q1,q2) c= A

proof end;

theorem Th3: :: JORDAN16:3

for A being Subset of (TOP-REAL 2)

for p1, p2, q being Point of (TOP-REAL 2) st q in A holds

q in L_Segment (A,p1,p2,q)

for p1, p2, q being Point of (TOP-REAL 2) st q in A holds

q in L_Segment (A,p1,p2,q)

proof end;

theorem Th4: :: JORDAN16:4

for A being Subset of (TOP-REAL 2)

for p1, p2, q being Point of (TOP-REAL 2) st q in A holds

q in R_Segment (A,p1,p2,q)

for p1, p2, q being Point of (TOP-REAL 2) st q in A holds

q in R_Segment (A,p1,p2,q)

proof end;

theorem Th5: :: JORDAN16:5

for A being Subset of (TOP-REAL 2)

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st LE q1,q2,A,p1,p2 holds

( q1 in Segment (A,p1,p2,q1,q2) & q2 in Segment (A,p1,p2,q1,q2) )

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st LE q1,q2,A,p1,p2 holds

( q1 in Segment (A,p1,p2,q1,q2) & q2 in Segment (A,p1,p2,q1,q2) )

proof end;

theorem :: JORDAN16:7

for C being Simple_closed_curve

for p, q being Point of (TOP-REAL 2) st p in C & q in C & not LE p,q,C holds

LE q,p,C

for p, q being Point of (TOP-REAL 2) st p in C & q in C & not LE p,q,C holds

LE q,p,C

proof end;

theorem Th8: :: JORDAN16:8

for X, Y being non empty TopSpace

for Y0 being non empty SubSpace of Y

for f being Function of X,Y

for g being Function of X,Y0 st f = g & f is continuous holds

g is continuous

for Y0 being non empty SubSpace of Y

for f being Function of X,Y

for g being Function of X,Y0 st f = g & f is continuous holds

g is continuous

proof end;

theorem Th9: :: JORDAN16:9

for S, T being non empty TopSpace

for S0 being non empty SubSpace of S

for T0 being non empty SubSpace of T

for f being Function of S,T st f is being_homeomorphism holds

for g being Function of S0,T0 st g = f | S0 & g is onto holds

g is being_homeomorphism

for S0 being non empty SubSpace of S

for T0 being non empty SubSpace of T

for f being Function of S,T st f is being_homeomorphism holds

for g being Function of S0,T0 st g = f | S0 & g is onto holds

g is being_homeomorphism

proof end;

theorem Th10: :: JORDAN16:10

for P1, P2, P3 being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P3 is_an_arc_of p1,p2 & P2 /\ P3 = {p1,p2} & P1 c= P2 \/ P3 & not P1 = P2 holds

P1 = P3

for p1, p2 being Point of (TOP-REAL 2) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P3 is_an_arc_of p1,p2 & P2 /\ P3 = {p1,p2} & P1 c= P2 \/ P3 & not P1 = P2 holds

P1 = P3

proof end;

theorem Th11: :: JORDAN16:11

for C being Simple_closed_curve

for A1, A2 being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 & A1 c= C & A2 c= C & A1 <> A2 holds

( A1 \/ A2 = C & A1 /\ A2 = {p1,p2} )

for A1, A2 being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 & A1 c= C & A2 c= C & A1 <> A2 holds

( A1 \/ A2 = C & A1 /\ A2 = {p1,p2} )

proof end;

theorem Th12: :: JORDAN16:12

for A1, A2 being Subset of (TOP-REAL 2)

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A1 /\ A2 = {q1,q2} holds

A1 <> A2

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A1 /\ A2 = {q1,q2} holds

A1 <> A2

proof end;

theorem :: JORDAN16:13

for C being Simple_closed_curve

for A1, A2 being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 & A1 c= C & A2 c= C & A1 /\ A2 = {p1,p2} holds

A1 \/ A2 = C

for A1, A2 being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 & A1 c= C & A2 c= C & A1 /\ A2 = {p1,p2} holds

A1 \/ A2 = C

proof end;

theorem :: JORDAN16:14

for C being Simple_closed_curve

for A1, A2 being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st A1 c= C & A2 c= C & A1 <> A2 & A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 holds

for A being Subset of (TOP-REAL 2) st A is_an_arc_of p1,p2 & A c= C & not A = A1 holds

A = A2

for A1, A2 being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st A1 c= C & A2 c= C & A1 <> A2 & A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 holds

for A being Subset of (TOP-REAL 2) st A is_an_arc_of p1,p2 & A c= C & not A = A1 holds

A = A2

proof end;

theorem Th15: :: JORDAN16:15

for C being Simple_closed_curve

for A being non empty Subset of (TOP-REAL 2) st A is_an_arc_of W-min C, E-max C & A c= C & not A = Lower_Arc C holds

A = Upper_Arc C

for A being non empty Subset of (TOP-REAL 2) st A is_an_arc_of W-min C, E-max C & A c= C & not A = Lower_Arc C holds

A = Upper_Arc C

proof end;

theorem Th16: :: JORDAN16:16

for A being Subset of (TOP-REAL 2)

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 holds

ex g being Function of I[01],((TOP-REAL 2) | A) ex s1, s2 being Real st

( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 )

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 holds

ex g being Function of I[01],((TOP-REAL 2) | A) ex s1, s2 being Real st

( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 )

proof end;

theorem Th17: :: JORDAN16:17

for A being Subset of (TOP-REAL 2)

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 & q1 <> q2 holds

ex g being Function of I[01],((TOP-REAL 2) | A) ex s1, s2 being Real st

( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 < s2 & s2 <= 1 )

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 & q1 <> q2 holds

ex g being Function of I[01],((TOP-REAL 2) | A) ex s1, s2 being Real st

( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 < s2 & s2 <= 1 )

proof end;

theorem :: JORDAN16:18

for A being Subset of (TOP-REAL 2)

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st LE q1,q2,A,p1,p2 holds

not Segment (A,p1,p2,q1,q2) is empty

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st LE q1,q2,A,p1,p2 holds

not Segment (A,p1,p2,q1,q2) is empty

proof end;

theorem :: JORDAN16:19

for C being Simple_closed_curve

for p being Point of (TOP-REAL 2) st p in C holds

( p in Segment (p,(W-min C),C) & W-min C in Segment (p,(W-min C),C) )

for p being Point of (TOP-REAL 2) st p in C holds

( p in Segment (p,(W-min C),C) & W-min C in Segment (p,(W-min C),C) )

proof end;

theorem Th20: :: JORDAN16:20

for f being Function of R^1,R^1

for a, b being Real st a <> 0 & f = AffineMap (a,b) holds

f is being_homeomorphism

for a, b being Real st a <> 0 & f = AffineMap (a,b) holds

f is being_homeomorphism

proof end;

theorem Th21: :: JORDAN16:21

for A being Subset of (TOP-REAL 2)

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 & q1 <> q2 holds

Segment (A,p1,p2,q1,q2) is_an_arc_of q1,q2

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 & q1 <> q2 holds

Segment (A,p1,p2,q1,q2) is_an_arc_of q1,q2

proof end;

theorem :: JORDAN16:22

for C being Simple_closed_curve

for p1, p2 being Point of (TOP-REAL 2)

for P being Subset of (TOP-REAL 2) st P c= C & P is_an_arc_of p1,p2 & W-min C in P & E-max C in P & not Upper_Arc C c= P holds

Lower_Arc C c= P

for p1, p2 being Point of (TOP-REAL 2)

for P being Subset of (TOP-REAL 2) st P c= C & P is_an_arc_of p1,p2 & W-min C in P & E-max C in P & not Upper_Arc C c= P holds

Lower_Arc C c= P

proof end;

:: Moved from JORDAN18, AK, 23.02.2006

theorem :: JORDAN16:23

for P being Subset of (TOP-REAL 2)

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 & q1 <> q2 holds

ex Q being non empty Subset of (TOP-REAL 2) st

( Q is_an_arc_of q1,q2 & Q c= P & Q misses {p1,p2} )

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 & q1 <> q2 holds

ex Q being non empty Subset of (TOP-REAL 2) st

( Q is_an_arc_of q1,q2 & Q c= P & Q misses {p1,p2} )

proof end;

:: moved from JORDAN20, AG 1.04.2006

theorem :: JORDAN16:24

for P being non empty Subset of (TOP-REAL 2)

for p1, p2, q1 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & p1 <> q1 holds

Segment (P,p1,p2,p1,q1) is_an_arc_of p1,q1

for p1, p2, q1 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & p1 <> q1 holds

Segment (P,p1,p2,p1,q1) is_an_arc_of p1,q1

proof end;