:: JORDAN1K semantic presentation

theorem Th1: :: JORDAN1K:1

for b₁ being set
for b₂ being non empty set
for b₃ being Function of b₁,b₂ st b₃ is onto holds
for b₄ being Element of b₂ ex b₅ being set st
( b₅ in b₁ & b₄ = b₃ . b₅ )

proof end;

theorem Th2: :: JORDAN1K:2

for b₁ being set
for b₂ being non empty set
for b₃ being Function of b₁,b₂ st b₃ is onto holds
for b₄ being Element of b₂ ex b₅ being Element of b₁ st b₄ = b₃ . b₅

proof end;

theorem Th3: :: JORDAN1K:3

for b₁ being set
for b₂ being non empty set
for b₃ being Function of b₁,b₂
for b₄ being Subset of b₁ st b₃ is onto holds
(b₃ .: b₄) ` c= b₃ .: (b₄ ` )

proof end;

theorem Th4: :: JORDAN1K:4

for b₁ being set
for b₂ being non empty set
for b₃ being Function of b₁,b₂
for b₄ being Subset of b₁ st b₃ is one-to-one holds
b₃ .: (b₄ ` ) c= (b₃ .: b₄) `

proof end;

theorem Th5: :: JORDAN1K:5

for b₁ being set
for b₂ being non empty set
for b₃ being Function of b₁,b₂
for b₄ being Subset of b₁ st b₃ is bijective holds
(b₃ .: b₄) ` = b₃ .: (b₄ ` )

proof end;

theorem Th6: :: JORDAN1K:6

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is_a_component_of {} b₁ iff b₂ is empty )

proof end;

theorem Th7: :: JORDAN1K:7

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂ c= b₃ & b₂ is_a_component_of b₄ & b₃ is_a_component_of b₄ holds
b₂ = b₃

proof end;

theorem Th8: :: JORDAN1K:8

for b₁ being Nat st b₁ >= 1 holds
for b₂ being Subset of (Euclid b₁) st b₂ is bounded holds
not b₂ ` is bounded

proof end;

theorem Th9: :: JORDAN1K:9

for b₁ being non empty MetrSpace
for b₂ being non empty Subset of (TopSpaceMetr b₁)
for b₃ being Point of (TopSpaceMetr b₁) holds (dist_min b₂) . b₃ >= 0

proof end;

theorem Th10: :: JORDAN1K:10

for b₁ being Real
for b₂ being non empty MetrSpace
for b₃ being non empty Subset of (TopSpaceMetr b₂)
for b₄ being Point of b₂ st ( for b₅ being Point of b₂ st b₅ in b₃ holds
dist b₄,b₅ >= b₁ ) holds
(dist_min b₃) . b₄ >= b₁

proof end;

theorem Th11: :: JORDAN1K:11

for b₁ being non empty MetrSpace
for b₂, b₃ being non empty Subset of (TopSpaceMetr b₁) holds min_dist_min b₂,b₃ >= 0

proof end;

theorem Th12: :: JORDAN1K:12

for b₁ being non empty MetrSpace
for b₂, b₃ being compact Subset of (TopSpaceMetr b₁) st b₂ meets b₃ holds
min_dist_min b₂,b₃ = 0

proof end;

theorem Th13: :: JORDAN1K:13

for b₁ being Real
for b₂ being non empty MetrSpace
for b₃, b₄ being non empty Subset of (TopSpaceMetr b₂) st ( for b₅, b₆ being Point of b₂ st b₅ in b₃ & b₆ in b₄ holds
dist b₅,b₆ >= b₁ ) holds
min_dist_min b₃,b₄ >= b₁

proof end;

theorem Th14: :: JORDAN1K:14

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) holds
( not b₂ is_a_component_of b₃ ` or b₂ is_inside_component_of b₃ or b₂ is_outside_component_of b₃ )

proof end;

theorem Th15: :: JORDAN1K:15

for b₁ being Nat st b₁ >= 1 holds
BDD ({} (TOP-REAL b₁)) = {} (TOP-REAL b₁)

proof end;

theorem Th16: :: JORDAN1K:16

for b₁ being Nat holds BDD ([#] (TOP-REAL b₁)) = {} (TOP-REAL b₁)

proof end;

theorem Th17: :: JORDAN1K:17

for b₁ being Nat st b₁ >= 1 holds
UBD ({} (TOP-REAL b₁)) = [#] (TOP-REAL b₁)

proof end;

theorem Th18: :: JORDAN1K:18

for b₁ being Nat holds UBD ([#] (TOP-REAL b₁)) = {} (TOP-REAL b₁)

proof end;

theorem Th19: :: JORDAN1K:19

for b₁ being Nat
for b₂ being connected Subset of (TOP-REAL b₁)
for b₃ being Subset of (TOP-REAL b₁) holds
( not b₂ misses b₃ or b₂ c= UBD b₃ or b₂ c= BDD b₃ )

proof end;

theorem Th20: :: JORDAN1K:20

for b₁ being Point of (TOP-REAL 2)
for b₂ being Real holds dist |[0,0]|,(b₂ * b₁) = (abs b₂) * (dist |[0,0]|,b₁)

proof end;

theorem Th21: :: JORDAN1K:21

for b₁, b₂, b₃ being Point of (TOP-REAL 2) holds dist (b₁ + b₂),(b₃ + b₂) = dist b₁,b₃

proof end;

theorem Th22: :: JORDAN1K:22

for b₁, b₂ being Point of (TOP-REAL 2) st b₁ <> b₂ holds
dist b₁,b₂ > 0

proof end;

theorem Th23: :: JORDAN1K:23

for b₁, b₂, b₃ being Point of (TOP-REAL 2) holds dist (b₁ - b₂),(b₃ - b₂) = dist b₁,b₃

proof end;

theorem Th24: :: JORDAN1K:24

for b₁, b₂ being Point of (TOP-REAL 2) holds dist b₁,b₂ = dist (- b₁),(- b₂)

proof end;

theorem Th25: :: JORDAN1K:25

for b₁, b₂, b₃ being Point of (TOP-REAL 2) holds dist (b₁ - b₂),(b₁ - b₃) = dist b₂,b₃

proof end;

theorem Th26: :: JORDAN1K:26

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being Real holds dist (b₃ * b₁),(b₃ * b₂) = (abs b₃) * (dist b₁,b₂)

proof end;

theorem Th27: :: JORDAN1K:27

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being Real st b₃ <= 1 holds
dist b₁,((b₃ * b₁) + ((1 - b₃) * b₂)) = (1 - b₃) * (dist b₁,b₂)

proof end;

theorem Th28: :: JORDAN1K:28

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being Real st 0 <= b₃ holds
dist b₁,((b₃ * b₂) + ((1 - b₃) * b₁)) = b₃ * (dist b₂,b₁)

proof end;

theorem Th29: :: JORDAN1K:29

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st b₁ in LSeg b₂,b₃ holds
(dist b₂,b₁) + (dist b₁,b₃) = dist b₂,b₃

proof end;

theorem Th30: :: JORDAN1K:30

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st b₁ in LSeg b₂,b₃ & b₁ <> b₂ holds
dist b₁,b₃ < dist b₂,b₃

proof end;

theorem Th31: :: JORDAN1K:31

for b₁ being Real
for b₂ being Point of (Euclid 2) st b₂ = |[0,0]| holds
Ball b₂,b₁ = { b₃ where B is Point of (TOP-REAL 2) : |.b₃.| < b₁ }

proof end;

theorem Th32: :: JORDAN1K:32

for b₁ being Point of (TOP-REAL 2)
for b₂, b₃, b₄ being Real holds (AffineMap b₂,b₃,b₂,b₄) . b₁ = (b₂ * b₁) + |[b₃,b₄]|

proof end;

theorem Th33: :: JORDAN1K:33

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being Real holds (AffineMap b₃,(b₁ `1 ),b₃,(b₁ `2 )) . b₂ = (b₃ * b₂) + b₁

proof end;

theorem Th34: :: JORDAN1K:34

for b₁, b₂, b₃, b₄ being Real st b₁ > 0 & b₂ > 0 holds
(AffineMap b₁,b₃,b₂,b₄) * (AffineMap (1 / b₁),(- (b₃ / b₁)),(1 / b₂),(- (b₄ / b₂))) = id (REAL 2)

proof end;

theorem Th35: :: JORDAN1K:35

for b₁ being Point of (TOP-REAL 2)
for b₂ being Real
for b₃, b₄ being Point of (Euclid 2) st b₃ = |[0,0]| & b₄ = b₁ & b₂ > 0 holds
(AffineMap b₂,(b₁ `1 ),b₂,(b₁ `2 )) .: (Ball b₃,1) = Ball b₄,b₂

proof end;

theorem Th36: :: JORDAN1K:36

for b₁, b₂, b₃, b₄ being Real st b₁ > 0 & b₃ > 0 holds
AffineMap b₁,b₂,b₃,b₄ is onto

proof end;

theorem Th37: :: JORDAN1K:37

for b₁ being Real
for b₂ being Point of (Euclid 2) holds (Ball b₂,b₁) ` is connected Subset of (TOP-REAL 2)

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Subset of (TOP-REAL c₁);
func dist_min c₂,c₃ -> Real means :Def1: :: JORDAN1K:def 1
ex b₁, b₂ being Subset of (TopSpaceMetr (Euclid a₁)) st
( a₂ = b₁ & a₃ = b₂ & a₄ = min_dist_min b₁,b₂ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def1 defines dist_min JORDAN1K:def 1 :

definition

let c₁ be non empty MetrSpace;
let c₂, c₃ be non empty compact Subset of (TopSpaceMetr c₁);
redefine func min_dist_min as min_dist_min c₂,c₃ -> Element of REAL ;
commutativity

proof end;

redefine func max_dist_max as max_dist_max c₂,c₃ -> Element of REAL ;
commutativity

proof end;

end;

definition

let c₁ be Nat;
let c₂, c₃ be non empty compact Subset of (TOP-REAL c₁);
redefine func dist_min as dist_min c₂,c₃ -> Real;
commutativity

proof end;

end;

theorem Th38: :: JORDAN1K:38

for b₁ being Nat
for b₂, b₃ being non empty Subset of (TOP-REAL b₁) holds dist_min b₂,b₃ >= 0

proof end;

theorem Th39: :: JORDAN1K:39

for b₁ being Nat
for b₂, b₃ being compact Subset of (TOP-REAL b₁) st b₂ meets b₃ holds
dist_min b₂,b₃ = 0

proof end;

theorem Th40: :: JORDAN1K:40

for b₁ being Nat
for b₂ being Real
for b₃, b₄ being non empty Subset of (TOP-REAL b₁) st ( for b₅, b₆ being Point of (TOP-REAL b₁) st b₅ in b₃ & b₆ in b₄ holds
dist b₅,b₆ >= b₂ ) holds
dist_min b₃,b₄ >= b₂

proof end;

theorem Th41: :: JORDAN1K:41

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄ being non empty Subset of (TOP-REAL b₁) st b₄ c= b₂ holds
dist_min b₃,b₂ <= dist_min b₃,b₄

proof end;

theorem Th42: :: JORDAN1K:42

for b₁ being Nat
for b₂, b₃ being non empty compact Subset of (TOP-REAL b₁) ex b₄, b₅ being Point of (TOP-REAL b₁) st
( b₄ in b₂ & b₅ in b₃ & dist_min b₂,b₃ = dist b₄,b₅ )

proof end;

theorem Th43: :: JORDAN1K:43

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds dist_min {b₂},{b₃} = dist b₂,b₃

proof end;

definition

let c₁ be Nat;
let c₂ be Point of (TOP-REAL c₁);
let c₃ be Subset of (TOP-REAL c₁);
func dist c₂,c₃ -> Real equals :: JORDAN1K:def 2
dist_min {a₂},a₃;
coherence ;

end;

:: deftheorem Def2 defines dist JORDAN1K:def 2 :

theorem Th44: :: JORDAN1K:44

for b₁ being Nat
for b₂ being non empty Subset of (TOP-REAL b₁)
for b₃ being Point of (TOP-REAL b₁) holds dist b₃,b₂ >= 0 by Th38;

theorem Th45: :: JORDAN1K:45

for b₁ being Nat
for b₂ being compact Subset of (TOP-REAL b₁)
for b₃ being Point of (TOP-REAL b₁) st b₃ in b₂ holds
dist b₃,b₂ = 0

proof end;

theorem Th46: :: JORDAN1K:46

for b₁ being Nat
for b₂ being non empty compact Subset of (TOP-REAL b₁)
for b₃ being Point of (TOP-REAL b₁) ex b₄ being Point of (TOP-REAL b₁) st
( b₄ in b₂ & dist b₃,b₂ = dist b₃,b₄ )

proof end;

theorem Th47: :: JORDAN1K:47

for b₁ being Nat
for b₂ being non empty Subset of (TOP-REAL b₁)
for b₃ being Subset of (TOP-REAL b₁) st b₂ c= b₃ holds
for b₄ being Point of (TOP-REAL b₁) holds dist b₄,b₃ <= dist b₄,b₂ by Th41;

theorem Th48: :: JORDAN1K:48

for b₁ being Nat
for b₂ being Real
for b₃ being non empty Subset of (TOP-REAL b₁)
for b₄ being Point of (TOP-REAL b₁) st ( for b₅ being Point of (TOP-REAL b₁) st b₅ in b₃ holds
dist b₄,b₅ >= b₂ ) holds
dist b₄,b₃ >= b₂

proof end;

theorem Th49: :: JORDAN1K:49

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds dist b₂,{b₃} = dist b₂,b₃ by Th43;

theorem Th50: :: JORDAN1K:50

for b₁ being Nat
for b₂ being non empty Subset of (TOP-REAL b₁)
for b₃, b₄ being Point of (TOP-REAL b₁) st b₄ in b₂ holds
dist b₃,b₂ <= dist b₃,b₄

proof end;

theorem Th51: :: JORDAN1K:51

for b₁ being non empty compact Subset of (TOP-REAL 2)
for b₂ being open Subset of (TOP-REAL 2) st b₁ c= b₂ holds
for b₃ being Point of (TOP-REAL 2) st not b₃ in b₂ holds
dist b₃,b₂ < dist b₃,b₁

proof end;

theorem Th52: :: JORDAN1K:52

for b₁, b₂ being Simple_closed_curve holds UBD b₁ meets UBD b₂

proof end;

theorem Th53: :: JORDAN1K:53

for b₁ being Simple_closed_curve
for b₂, b₃ being Point of (TOP-REAL 2) st b₂ in UBD b₁ & b₃ in BDD b₁ holds
dist b₂,b₁ < dist b₂,b₃

proof end;

registration

let c₁ be Simple_closed_curve;
cluster BDD a₁ -> non empty ;
coherence

proof end;

end;

theorem Th54: :: JORDAN1K:54

for b₁ being Simple_closed_curve
for b₂ being Point of (TOP-REAL 2) st not b₂ in BDD b₁ holds
dist b₂,b₁ <= dist b₂,(BDD b₁)

proof end;

theorem Th55: :: JORDAN1K:55

for b₁, b₂ being Simple_closed_curve holds
( not b₁ c= BDD b₂ or not b₂ c= BDD b₁ )

proof end;

theorem Th56: :: JORDAN1K:56

for b₁, b₂ being Simple_closed_curve st b₁ c= BDD b₂ holds
b₂ c= UBD b₁

proof end;

theorem Th57: :: JORDAN1K:57

for b₁ being Simple_closed_curve
for b₂ being Nat holds L~ (Cage b₁,b₂) c= UBD b₁

proof end;

definition

let c₁ be Simple_closed_curve;
func Lower_Middle_Point c₁ -> Point of (TOP-REAL 2) equals :: JORDAN1K:def 3
First_Point (Lower_Arc a₁),(W-min a₁),(E-max a₁),(Vertical_Line (((W-bound a₁) + (E-bound a₁)) / 2));
coherence ;
func Upper_Middle_Point c₁ -> Point of (TOP-REAL 2) equals :: JORDAN1K:def 4
First_Point (Upper_Arc a₁),(W-min a₁),(E-max a₁),(Vertical_Line (((W-bound a₁) + (E-bound a₁)) / 2));
coherence ;

end;

:: deftheorem Def3 defines Lower_Middle_Point JORDAN1K:def 3 :

:: deftheorem Def4 defines Upper_Middle_Point JORDAN1K:def 4 :

theorem Th58: :: JORDAN1K:58

for b₁ being Simple_closed_curve holds Lower_Arc b₁ meets Vertical_Line (((W-bound b₁) + (E-bound b₁)) / 2)

proof end;

theorem Th59: :: JORDAN1K:59

for b₁ being Simple_closed_curve holds Upper_Arc b₁ meets Vertical_Line (((W-bound b₁) + (E-bound b₁)) / 2)

proof end;

theorem Th60: :: JORDAN1K:60

for b₁ being Simple_closed_curve holds (Lower_Middle_Point b₁) `1 = ((W-bound b₁) + (E-bound b₁)) / 2

proof end;

theorem Th61: :: JORDAN1K:61

for b₁ being Simple_closed_curve holds (Upper_Middle_Point b₁) `1 = ((W-bound b₁) + (E-bound b₁)) / 2

proof end;

theorem Th62: :: JORDAN1K:62

for b₁ being Simple_closed_curve holds Lower_Middle_Point b₁ in Lower_Arc b₁

proof end;

theorem Th63: :: JORDAN1K:63

for b₁ being Simple_closed_curve holds Upper_Middle_Point b₁ in Upper_Arc b₁

proof end;