:: JORDAN2C semantic presentation

theorem Th1: :: JORDAN2C:1

for b₁ being Real st b₁ <= 0 holds
abs b₁ = - b₁

proof end;

theorem Th2: :: JORDAN2C:2

for b₁, b₂ being Nat st b₁ <= b₂ & b₂ <= b₁ + 2 & not b₂ = b₁ & not b₂ = b₁ + 1 holds
b₂ = b₁ + 2

proof end;

theorem Th3: :: JORDAN2C:3

for b₁, b₂ being Nat st b₁ <= b₂ & b₂ <= b₁ + 3 & not b₂ = b₁ & not b₂ = b₁ + 1 & not b₂ = b₁ + 2 holds
b₂ = b₁ + 3

proof end;

theorem Th4: :: JORDAN2C:4

for b₁, b₂ being Nat st b₁ <= b₂ & b₂ <= b₁ + 4 & not b₂ = b₁ & not b₂ = b₁ + 1 & not b₂ = b₁ + 2 & not b₂ = b₁ + 3 holds
b₂ = b₁ + 4

proof end;

Lemma5: for b₁, b₂ being real number st b₁ >= 0 & b₂ >= 0 holds
b₁ + b₂ >= 0
by XREAL_1:35;

Lemma6: for b₁, b₂ being real number st b₁ > 0 & b₂ >= 0 holds
b₁ + b₂ > 0
by XREAL_1:36;

theorem Th5: :: JORDAN2C:5

canceled;

theorem Th6: :: JORDAN2C:6

canceled;

theorem Th7: :: JORDAN2C:7

for b₁, b₂ being set
for b₃ being FinSequence st rng b₃ = {b₁,b₂} & len b₃ = 2 & not ( b₃ . 1 = b₁ & b₃ . 2 = b₂ ) holds
( b₃ . 1 = b₂ & b₃ . 2 = b₁ )

proof end;

theorem Th8: :: JORDAN2C:8

for b₁, b₂ being Real
for b₃ being increasing FinSequence of REAL st rng b₃ = {b₁,b₂} & len b₃ = 2 & b₁ <= b₂ holds
( b₃ . 1 = b₁ & b₃ . 2 = b₂ )

proof end;

theorem Th9: :: JORDAN2C:9

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

proof end;

theorem Th10: :: JORDAN2C:10

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds abs |.b₂.| = |.b₂.|

proof end;

theorem Th11: :: JORDAN2C:11

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds abs (|.b₂.| - |.b₃.|) <= |.(b₂ - b₃).|

proof end;

theorem Th12: :: JORDAN2C:12

for b₁ being Real holds |.|[b₁]|.| = abs b₁

proof end;

theorem Th13: :: JORDAN2C:13

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds
( b₂ - (0.REAL b₁) = b₂ & (0.REAL b₁) - b₂ = - b₂ )

proof end;

theorem Th14: :: JORDAN2C:14

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) st b₂ is convex holds
b₂ is connected

proof end;

theorem Th15: :: JORDAN2C:15

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁
for b₄ being Subset of (b₁ | b₃) st b₂ = b₄ & b₂ is connected holds
b₄ is connected

proof end;

definition

let c₁ be Nat;
let c₂ be Subset of (TOP-REAL c₁);
canceled;
attr a₂ is Bounded means :Def2: :: JORDAN2C:def 2
a₂ is bounded Subset of (Euclid a₁);
correctness ;

end;

:: deftheorem Def1 JORDAN2C:def 1 :

:: deftheorem Def2 defines Bounded JORDAN2C:def 2 :

theorem Th16: :: JORDAN2C:16

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) st b₃ is Bounded & b₂ c= b₃ holds
b₂ is Bounded

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Subset of (TOP-REAL c₁);
pred c₃ is_inside_component_of c₂ means :Def3: :: JORDAN2C:def 3
( a₃ is_a_component_of a₂ ` & a₃ is Bounded );

end;

:: deftheorem Def3 defines is_inside_component_of JORDAN2C:def 3 :

registration

let c₁ be non empty MetrStruct ;
cluster bounded Element of bool the carrier of a₁;
existence

proof end;

end;

theorem Th17: :: JORDAN2C:17

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) holds
( b₃ is_inside_component_of b₂ iff ex b₄ being Subset of ((TOP-REAL b₁) | (b₂ ` )) st
( b₄ = b₃ & b₄ is_a_component_of (TOP-REAL b₁) | (b₂ ` ) & b₄ is bounded Subset of (Euclid b₁) ) )

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Subset of (TOP-REAL c₁);
pred c₃ is_outside_component_of c₂ means :Def4: :: JORDAN2C:def 4
( a₃ is_a_component_of a₂ ` & not a₃ is Bounded );

end;

:: deftheorem Def4 defines is_outside_component_of JORDAN2C:def 4 :

theorem Th18: :: JORDAN2C:18

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) holds
( b₃ is_outside_component_of b₂ iff ex b₄ being Subset of ((TOP-REAL b₁) | (b₂ ` )) st
( b₄ = b₃ & b₄ is_a_component_of (TOP-REAL b₁) | (b₂ ` ) & b₄ is not bounded Subset of (Euclid b₁) ) )

proof end;

theorem Th19: :: JORDAN2C:19

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) st b₃ is_inside_component_of b₂ holds
b₃ c= b₂ `

proof end;

theorem Th20: :: JORDAN2C:20

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) st b₃ is_outside_component_of b₂ holds
b₃ c= b₂ `

proof end;

definition

let c₁ be Nat;
let c₂ be Subset of (TOP-REAL c₁);
func BDD c₂ -> Subset of (TOP-REAL a₁) equals :: JORDAN2C:def 5
union { b₁ where B is Subset of (TOP-REAL a₁) : b₁ is_inside_component_of a₂ } ;
correctness

proof end;

end;

:: deftheorem Def5 defines BDD JORDAN2C:def 5 :

definition

let c₁ be Nat;
let c₂ be Subset of (TOP-REAL c₁);
func UBD c₂ -> Subset of (TOP-REAL a₁) equals :: JORDAN2C:def 6
union { b₁ where B is Subset of (TOP-REAL a₁) : b₁ is_outside_component_of a₂ } ;
correctness

proof end;

end;

:: deftheorem Def6 defines UBD JORDAN2C:def 6 :

theorem Th21: :: JORDAN2C:21

for b₁ being Nat holds [#] (TOP-REAL b₁) is convex

proof end;

theorem Th22: :: JORDAN2C:22

for b₁ being Nat holds [#] (TOP-REAL b₁) is connected

proof end;

registration

let c₁ be Nat;
cluster [#] (TOP-REAL a₁) -> connected ;
coherence by Th22;

end;

theorem Th23: :: JORDAN2C:23

for b₁ being Nat holds [#] (TOP-REAL b₁) is_a_component_of TOP-REAL b₁

proof end;

theorem Th24: :: JORDAN2C:24

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) holds BDD b₂ is a_union_of_components of (TOP-REAL b₁) | (b₂ ` )

proof end;

theorem Th25: :: JORDAN2C:25

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) holds UBD b₂ is a_union_of_components of (TOP-REAL b₁) | (b₂ ` )

proof end;

theorem Th26: :: JORDAN2C:26

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) st b₃ is_inside_component_of b₂ holds
b₃ c= BDD b₂

proof end;

theorem Th27: :: JORDAN2C:27

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) st b₃ is_outside_component_of b₂ holds
b₃ c= UBD b₂

proof end;

theorem Th28: :: JORDAN2C:28

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) holds BDD b₂ misses UBD b₂

proof end;

theorem Th29: :: JORDAN2C:29

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) holds BDD b₂ c= b₂ `

proof end;

theorem Th30: :: JORDAN2C:30

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) holds UBD b₂ c= b₂ `

proof end;

theorem Th31: :: JORDAN2C:31

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) holds (BDD b₂) \/ (UBD b₂) = b₂ `

proof end;

theorem Th32: :: JORDAN2C:32

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being Point of b₁
for b₅, b₆ being Function of I[01] ,b₁ st b₅ is continuous & b₂ = b₅ . 0 & b₃ = b₅ . 1 & b₆ is continuous & b₃ = b₆ . 0 & b₄ = b₆ . 1 holds
ex b₇ being Function of I[01] ,b₁ st
( b₇ is continuous & b₂ = b₇ . 0 & b₄ = b₇ . 1 & rng b₇ c= (rng b₅) \/ (rng b₆) )

proof end;

theorem Th33: :: JORDAN2C:33

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) st b₂ = REAL b₁ holds
b₂ is connected

proof end;

definition

let c₁ be Nat;
func 1* c₁ -> FinSequence of REAL equals :: JORDAN2C:def 7
a₁ |-> 1;
coherence by FINSEQ_2:77;

end;

:: deftheorem Def7 defines 1* JORDAN2C:def 7 :

definition

let c₁ be Nat;
redefine func 1* as 1* c₁ -> Element of REAL a₁;
coherence

proof end;

end;

definition

let c₁ be Nat;
func 1.REAL c₁ -> Point of (TOP-REAL a₁) equals :: JORDAN2C:def 8
1* a₁;
coherence by EUCLID:25;

end;

:: deftheorem Def8 defines 1.REAL JORDAN2C:def 8 :

theorem Th34: :: JORDAN2C:34

for b₁ being Nat holds abs (1* b₁) = b₁ |-> 1

proof end;

theorem Th35: :: JORDAN2C:35

for b₁ being Nat holds |.(1* b₁).| = sqrt b₁

proof end;

theorem Th36: :: JORDAN2C:36

1.REAL 1 = <*1*> by FINSEQ_2:73;

theorem Th37: :: JORDAN2C:37

for b₁ being Nat holds |.(1.REAL b₁).| = sqrt b₁

proof end;

theorem Th38: :: JORDAN2C:38

for b₁ being Nat st 1 <= b₁ holds
1 <= |.(1.REAL b₁).|

proof end;

theorem Th39: :: JORDAN2C:39

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

proof end;

theorem Th40: :: JORDAN2C:40

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) holds
( b₂ is Bounded iff ex b₃ being Real st
for b₄ being Point of (TOP-REAL b₁) st b₄ in b₂ holds
|.b₄.| < b₃ )

proof end;

theorem Th41: :: JORDAN2C:41

for b₁ being Nat st b₁ >= 1 holds
not [#] (TOP-REAL b₁) is Bounded

proof end;

theorem Th42: :: JORDAN2C:42

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

proof end;

theorem Th43: :: JORDAN2C:43

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁)
for b₅ being non empty Subset of (TOP-REAL b₁)
for b₆, b₇ being Function of I[01] ,((TOP-REAL b₁) | b₅) st b₆ is continuous & b₂ = b₆ . 0 & b₃ = b₆ . 1 & b₇ is continuous & b₃ = b₇ . 0 & b₄ = b₇ . 1 holds
ex b₈ being Function of I[01] ,((TOP-REAL b₁) | b₅) st
( b₈ is continuous & b₂ = b₈ . 0 & b₄ = b₈ . 1 )

proof end;

theorem Th44: :: JORDAN2C:44

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄, b₅ being Point of (TOP-REAL b₁) st b₃ in b₂ & b₄ in b₂ & b₅ in b₂ & LSeg b₃,b₄ c= b₂ & LSeg b₄,b₅ c= b₂ holds
ex b₆ being Function of I[01] ,((TOP-REAL b₁) | b₂) st
( b₆ is continuous & b₃ = b₆ . 0 & b₅ = b₆ . 1 )

proof end;

theorem Th45: :: JORDAN2C:45

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄, b₅, b₆ being Point of (TOP-REAL b₁) st b₃ in b₂ & b₄ in b₂ & b₅ in b₂ & b₆ in b₂ & LSeg b₃,b₄ c= b₂ & LSeg b₄,b₅ c= b₂ & LSeg b₅,b₆ c= b₂ holds
ex b₇ being Function of I[01] ,((TOP-REAL b₁) | b₂) st
( b₇ is continuous & b₃ = b₇ . 0 & b₆ = b₇ . 1 )

proof end;

theorem Th46: :: JORDAN2C:46

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄, b₅, b₆, b₇, b₈, b₉ being Point of (TOP-REAL b₁) st b₃ in b₂ & b₄ in b₂ & b₅ in b₂ & b₆ in b₂ & b₇ in b₂ & b₈ in b₂ & b₉ in b₂ & LSeg b₃,b₄ c= b₂ & LSeg b₄,b₅ c= b₂ & LSeg b₅,b₆ c= b₂ & LSeg b₆,b₇ c= b₂ & LSeg b₇,b₈ c= b₂ & LSeg b₈,b₉ c= b₂ holds
ex b₁₀ being Function of I[01] ,((TOP-REAL b₁) | b₂) st
( b₁₀ is continuous & b₃ = b₁₀ . 0 & b₉ = b₁₀ . 1 )

proof end;

theorem Th47: :: JORDAN2C:47

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) st ( for b₄ being Real holds
( not b₂ = b₄ * b₃ & not b₃ = b₄ * b₂ ) ) holds
not 0.REAL b₁ in LSeg b₂,b₃

proof end;

theorem Th48: :: JORDAN2C:48

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁)
for b₄ being Subset of (TopSpaceMetr (Euclid b₁)) st b₄ = LSeg b₂,b₃ & not 0.REAL b₁ in LSeg b₂,b₃ holds
ex b₅ being Point of (TOP-REAL b₁) st
( b₅ in LSeg b₂,b₃ & |.b₅.| > 0 & |.b₅.| = (dist_min b₄) . (0.REAL b₁) )

proof end;

theorem Th49: :: JORDAN2C:49

for b₁ being Nat
for b₂ being Real
for b₃ being Subset of (TOP-REAL b₁)
for b₄, b₅ being Point of (TOP-REAL b₁) st b₃ = { b₆ where B is Point of (TOP-REAL b₁) : |.b₆.| > b₂ } & b₄ in b₃ & b₅ in b₃ & ( for b₆ being Real holds
( not b₄ = b₆ * b₅ & not b₅ = b₆ * b₄ ) ) holds
ex b₆, b₇ being Point of (TOP-REAL b₁) st
( b₆ in b₃ & b₇ in b₃ & LSeg b₄,b₆ c= b₃ & LSeg b₆,b₇ c= b₃ & LSeg b₇,b₅ c= b₃ )

proof end;

theorem Th50: :: JORDAN2C:50

for b₁ being Nat
for b₂ being Real
for b₃ being Subset of (TOP-REAL b₁)
for b₄, b₅ being Point of (TOP-REAL b₁) st b₃ = (REAL b₁) \ { b₆ where B is Point of (TOP-REAL b₁) : |.b₆.| < b₂ } & b₄ in b₃ & b₅ in b₃ & ( for b₆ being Real holds
( not b₄ = b₆ * b₅ & not b₅ = b₆ * b₄ ) ) holds
ex b₆, b₇ being Point of (TOP-REAL b₁) st
( b₆ in b₃ & b₇ in b₃ & LSeg b₄,b₆ c= b₃ & LSeg b₆,b₇ c= b₃ & LSeg b₇,b₅ c= b₃ )

proof end;

theorem Th51: :: JORDAN2C:51

canceled;

theorem Th52: :: JORDAN2C:52

for b₁ being FinSequence of REAL holds
( b₁ is Element of REAL (len b₁) & b₁ is Point of (TOP-REAL (len b₁)) )

proof end;

theorem Th53: :: JORDAN2C:53

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃, b₄ being FinSequence of REAL
for b₅ being Real st b₃ = b₂ & b₄ = b₅ * b₂ holds
( len b₃ = len b₄ & ( for b₆ being Nat st 1 <= b₆ & b₆ <= len b₃ holds
b₄ /. b₆ = b₅ * (b₃ /. b₆) ) )

proof end;

theorem Th54: :: JORDAN2C:54

for b₁ being Nat
for b₂ being Element of REAL b₁
for b₃ being FinSequence st b₂ <> 0* b₁ & b₂ = b₃ holds
ex b₄ being Nat st
( 1 <= b₄ & b₄ <= b₁ & b₃ . b₄ <> 0 )

proof end;

theorem Th55: :: JORDAN2C:55

for b₁ being Nat
for b₂ being Element of REAL b₁ st b₁ >= 2 & b₂ <> 0* b₁ holds
ex b₃ being Element of REAL b₁ st
for b₄ being Real holds
( not b₃ = b₄ * b₂ & not b₂ = b₄ * b₃ )

proof end;

theorem Th56: :: JORDAN2C:56

for b₁ being Nat
for b₂ being Real
for b₃ being Subset of (TOP-REAL b₁)
for b₄, b₅ being Point of (TOP-REAL b₁) st b₁ >= 2 & b₃ = { b₆ where B is Point of (TOP-REAL b₁) : |.b₆.| > b₂ } & b₄ in b₃ & b₅ in b₃ & ex b₆ being Real st
( b₄ = b₆ * b₅ or b₅ = b₆ * b₄ ) holds
ex b₆, b₇, b₈, b₉, b₁₀ being Point of (TOP-REAL b₁) st
( b₆ in b₃ & b₇ in b₃ & b₈ in b₃ & b₉ in b₃ & b₁₀ in b₃ & LSeg b₄,b₆ c= b₃ & LSeg b₆,b₇ c= b₃ & LSeg b₇,b₈ c= b₃ & LSeg b₈,b₉ c= b₃ & LSeg b₉,b₁₀ c= b₃ & LSeg b₁₀,b₅ c= b₃ )

proof end;

theorem Th57: :: JORDAN2C:57

for b₁ being Nat
for b₂ being Real
for b₃ being Subset of (TOP-REAL b₁)
for b₄, b₅ being Point of (TOP-REAL b₁) st b₁ >= 2 & b₃ = (REAL b₁) \ { b₆ where B is Point of (TOP-REAL b₁) : |.b₆.| < b₂ } & b₄ in b₃ & b₅ in b₃ & ex b₆ being Real st
( b₄ = b₆ * b₅ or b₅ = b₆ * b₄ ) holds
ex b₆, b₇, b₈, b₉, b₁₀ being Point of (TOP-REAL b₁) st
( b₆ in b₃ & b₇ in b₃ & b₈ in b₃ & b₉ in b₃ & b₁₀ in b₃ & LSeg b₄,b₆ c= b₃ & LSeg b₆,b₇ c= b₃ & LSeg b₇,b₈ c= b₃ & LSeg b₈,b₉ c= b₃ & LSeg b₉,b₁₀ c= b₃ & LSeg b₁₀,b₅ c= b₃ )

proof end;

theorem Th58: :: JORDAN2C:58

for b₁ being Nat
for b₂ being Real st b₁ >= 1 holds
{ b₃ where B is Point of (TOP-REAL b₁) : |.b₃.| > b₂ } <> {}

proof end;

theorem Th59: :: JORDAN2C:59

for b₁ being Nat
for b₂ being Real
for b₃ being Subset of (TOP-REAL b₁) st b₁ >= 2 & b₃ = { b₄ where B is Point of (TOP-REAL b₁) : |.b₄.| > b₂ } holds
b₃ is connected

proof end;

theorem Th60: :: JORDAN2C:60

for b₁ being Nat
for b₂ being Real st b₁ >= 1 holds
(REAL b₁) \ { b₃ where B is Point of (TOP-REAL b₁) : |.b₃.| < b₂ } <> {}

proof end;

theorem Th61: :: JORDAN2C:61

for b₁ being Nat
for b₂ being Real
for b₃ being Subset of (TOP-REAL b₁) st b₁ >= 2 & b₃ = (REAL b₁) \ { b₄ where B is Point of (TOP-REAL b₁) : |.b₄.| < b₂ } holds
b₃ is connected

proof end;

theorem Th62: :: JORDAN2C:62

for b₁ being Real
for b₂ being Nat
for b₃ being Subset of (TOP-REAL b₂) st b₂ >= 1 & b₃ = (REAL b₂) \ { b₄ where B is Point of (TOP-REAL b₂) : |.b₄.| < b₁ } holds
not b₃ is Bounded

proof end;

theorem Th63: :: JORDAN2C:63

for b₁ being Real
for b₂ being Subset of (TOP-REAL 1) st b₂ = { b₃ where B is Point of (TOP-REAL 1) : ex b₁ being Real st
( b₃ = <*b₄*> & b₄ > b₁ ) } holds
b₂ is convex

proof end;

theorem Th64: :: JORDAN2C:64

for b₁ being Real
for b₂ being Subset of (TOP-REAL 1) st b₂ = { b₃ where B is Point of (TOP-REAL 1) : ex b₁ being Real st
( b₃ = <*b₄*> & b₄ < - b₁ ) } holds
b₂ is convex

proof end;

theorem Th65: :: JORDAN2C:65

for b₁ being Real
for b₂ being Subset of (TOP-REAL 1) st b₂ = { b₃ where B is Point of (TOP-REAL 1) : ex b₁ being Real st
( b₃ = <*b₄*> & b₄ > b₁ ) } holds
b₂ is connected

proof end;

theorem Th66: :: JORDAN2C:66

for b₁ being Real
for b₂ being Subset of (TOP-REAL 1) st b₂ = { b₃ where B is Point of (TOP-REAL 1) : ex b₁ being Real st
( b₃ = <*b₄*> & b₄ < - b₁ ) } holds
b₂ is connected

proof end;

theorem Th67: :: JORDAN2C:67

for b₁ being Subset of (Euclid 1)
for b₂ being Real
for b₃ being Subset of (TOP-REAL 1) st b₁ = { b₄ where B is Point of (TOP-REAL 1) : ex b₁ being Real st
( b₄ = <*b₅*> & b₅ > b₂ ) } & b₃ = b₁ holds
( b₃ is connected & not b₁ is bounded )

proof end;

theorem Th68: :: JORDAN2C:68

for b₁ being Subset of (Euclid 1)
for b₂ being Real
for b₃ being Subset of (TOP-REAL 1) st b₁ = { b₄ where B is Point of (TOP-REAL 1) : ex b₁ being Real st
( b₄ = <*b₅*> & b₅ < - b₂ ) } & b₃ = b₁ holds
( b₃ is connected & not b₁ is bounded )

proof end;

theorem Th69: :: JORDAN2C:69

for b₁ being Nat
for b₂ being Subset of (Euclid b₁)
for b₃ being Real
for b₄ being Subset of (TOP-REAL b₁) st b₁ >= 2 & b₂ = { b₅ where B is Point of (TOP-REAL b₁) : |.b₅.| > b₃ } & b₄ = b₂ holds
( b₄ is connected & not b₂ is bounded )

proof end;

theorem Th70: :: JORDAN2C:70

for b₁ being Nat
for b₂ being Subset of (Euclid b₁)
for b₃ being Real
for b₄ being Subset of (TOP-REAL b₁) st b₁ >= 2 & b₂ = (REAL b₁) \ { b₅ where B is Point of (TOP-REAL b₁) : |.b₅.| < b₃ } & b₄ = b₂ holds
( b₄ is connected & not b₂ is bounded )

proof end;

theorem Th71: :: JORDAN2C:71

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁)
for b₅ being Subset of (Euclid b₁) st b₂ = b₅ & b₂ is connected & not b₅ is bounded & b₃ = skl (Down b₂,(b₄ ` )) & b₅ misses b₄ holds
b₃ is_outside_component_of b₄

proof end;

theorem Th72: :: JORDAN2C:72

for b₁ being Nat
for b₂ being Subset of (Euclid b₁)
for b₃ being non empty Subset of (Euclid b₁)
for b₄ being Subset of ((Euclid b₁) | b₃) st b₂ c= b₃ & b₂ = b₄ & b₄ is bounded holds
b₂ is bounded

proof end;

theorem Th73: :: JORDAN2C:73

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) st b₂ is compact holds
b₂ is Bounded

proof end;

registration

let c₁ be Nat;
cluster compact -> Bounded Element of bool the carrier of (TOP-REAL a₁);
coherence by Th73;

end;

theorem Th74: :: JORDAN2C:74

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) st 1 <= b₁ & b₂ is Bounded holds
b₂ ` <> {}

proof end;

theorem Th75: :: JORDAN2C:75

for b₁ being Nat
for b₂ being Real holds
( ex b₃ being Subset of (Euclid b₁) st b₃ = { b₄ where B is Point of (TOP-REAL b₁) : |.b₄.| < b₂ } & ( for b₃ being Subset of (Euclid b₁) st b₃ = { b₄ where B is Point of (TOP-REAL b₁) : |.b₄.| < b₂ } holds
b₃ is bounded ) )

proof end;

theorem Th76: :: JORDAN2C:76

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) st b₁ >= 2 & b₂ is Bounded holds
ex b₃ being Subset of (TOP-REAL b₁) st
( b₃ is_outside_component_of b₂ & b₃ = UBD b₂ )

proof end;

theorem Th77: :: JORDAN2C:77

for b₁ being Nat
for b₂ being Real
for b₃ being Subset of (TOP-REAL b₁) st b₃ = { b₄ where B is Point of (TOP-REAL b₁) : |.b₄.| < b₂ } holds
b₃ is convex

proof end;

theorem Th78: :: JORDAN2C:78

for b₁ being Nat
for b₂ being Point of (Euclid b₁)
for b₃ being Real
for b₄ being Subset of (TOP-REAL b₁) st b₄ = Ball b₂,b₃ holds
b₄ is convex

proof end;

theorem Th79: :: JORDAN2C:79

for b₁ being Nat
for b₂ being Real
for b₃ being Subset of (TOP-REAL b₁) st b₃ = { b₄ where B is Point of (TOP-REAL b₁) : |.b₄.| < b₂ } holds
b₃ is connected

proof end;

theorem Th80: :: JORDAN2C:80

for b₁ being Nat
for b₂ being Real
for b₃, b₄ being Point of (TOP-REAL b₁)
for b₅ being Point of (Euclid b₁) st b₃ <> b₄ & b₃ in Ball b₅,b₂ & b₄ in Ball b₅,b₂ holds
ex b₆ being Function of I[01] ,(TOP-REAL b₁) st
( b₆ is continuous & b₆ . 0 = b₃ & b₆ . 1 = b₄ & rng b₆ c= Ball b₅,b₂ )

proof end;

theorem Th81: :: JORDAN2C:81

for b₁ being Nat
for b₂ being Real
for b₃, b₄, b₅ being Point of (TOP-REAL b₁)
for b₆ being Point of (Euclid b₁)
for b₇ being Function of I[01] ,(TOP-REAL b₁) st b₇ is continuous & b₇ . 0 = b₃ & b₇ . 1 = b₄ & b₅ in Ball b₆,b₂ & b₄ in Ball b₆,b₂ holds
ex b₈ being Function of I[01] ,(TOP-REAL b₁) st
( b₈ is continuous & b₈ . 0 = b₃ & b₈ . 1 = b₅ & rng b₈ c= (rng b₇) \/ (Ball b₆,b₂) )

proof end;

theorem Th82: :: JORDAN2C:82

for b₁ being Nat
for b₂ being Real
for b₃, b₄, b₅ being Point of (TOP-REAL b₁)
for b₆ being Point of (Euclid b₁)
for b₇ being Subset of (TOP-REAL b₁)
for b₈ being Function of I[01] ,(TOP-REAL b₁) st b₈ is continuous & rng b₈ c= b₇ & b₈ . 0 = b₃ & b₈ . 1 = b₄ & b₅ in Ball b₆,b₂ & b₄ in Ball b₆,b₂ & Ball b₆,b₂ c= b₇ holds
ex b₉ being Function of I[01] ,(TOP-REAL b₁) st
( b₉ is continuous & rng b₉ c= b₇ & b₉ . 0 = b₃ & b₉ . 1 = b₅ )

proof end;

theorem Th83: :: JORDAN2C:83

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃ being Point of (TOP-REAL b₁)
for b₄ being Subset of (TOP-REAL b₁) st b₂ is connected & b₂ is open & b₄ = { b₅ where B is Point of (TOP-REAL b₁) : ( b₅ <> b₃ & b₅ in b₂ & ( for b₁ being Function of I[01] ,(TOP-REAL b₁) holds
( not b₆ is continuous or not rng b₆ c= b₂ or not b₆ . 0 = b₃ or not b₆ . 1 = b₅ ) ) ) } holds
b₄ is open

proof end;

theorem Th84: :: JORDAN2C:84

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁)
for b₃, b₄ being Subset of (TOP-REAL b₁) st b₃ is connected & b₃ is open & b₂ in b₃ & b₄ = { b₅ where B is Point of (TOP-REAL b₁) : ( b₅ = b₂ or ex b₁ being Function of I[01] ,(TOP-REAL b₁) st
( b₆ is continuous & rng b₆ c= b₃ & b₆ . 0 = b₂ & b₆ . 1 = b₅ ) ) } holds
b₄ is open

proof end;

theorem Th85: :: JORDAN2C:85

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁)
for b₃, b₄ being Subset of (TOP-REAL b₁) st b₂ in b₄ & b₃ = { b₅ where B is Point of (TOP-REAL b₁) : ( b₅ = b₂ or ex b₁ being Function of I[01] ,(TOP-REAL b₁) st
( b₆ is continuous & rng b₆ c= b₄ & b₆ . 0 = b₂ & b₆ . 1 = b₅ ) ) } holds
b₃ c= b₄

proof end;

theorem Th86: :: JORDAN2C:86

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁)
for b₄ being Point of (TOP-REAL b₁) st b₃ is connected & b₃ is open & b₄ in b₃ & b₂ = { b₅ where B is Point of (TOP-REAL b₁) : ( b₅ = b₄ or ex b₁ being Function of I[01] ,(TOP-REAL b₁) st
( b₆ is continuous & rng b₆ c= b₃ & b₆ . 0 = b₄ & b₆ . 1 = b₅ ) ) } holds
b₃ c= b₂

proof end;

theorem Th87: :: JORDAN2C:87

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄ being Point of (TOP-REAL b₁) st b₂ is connected & b₂ is open & b₃ in b₂ & b₄ in b₂ & b₃ <> b₄ holds
ex b₅ being Function of I[01] ,(TOP-REAL b₁) st
( b₅ is continuous & rng b₅ c= b₂ & b₅ . 0 = b₃ & b₅ . 1 = b₄ )

proof end;

theorem Th88: :: JORDAN2C:88

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃ being real number st b₂ = { b₄ where B is Point of (TOP-REAL b₁) : |.b₄.| = b₃ } holds
( b₂ ` is open & b₂ is closed )

proof end;

theorem Th89: :: JORDAN2C:89

for b₁ being Nat
for b₂ being non empty Subset of (TOP-REAL b₁) st b₂ is open holds
(TOP-REAL b₁) | b₂ is locally_connected

proof end;

theorem Th90: :: JORDAN2C:90

for b₁ being Nat
for b₂ being non empty Subset of (TOP-REAL b₁)
for b₃ being Subset of (TOP-REAL b₁)
for b₄ being real number st b₃ = { b₅ where B is Point of (TOP-REAL b₁) : |.b₅.| = b₄ } & b₃ ` = b₂ holds
(TOP-REAL b₁) | b₂ is locally_connected

proof end;

theorem Th91: :: JORDAN2C:91

for b₁ being Nat
for b₂ being Function of (TOP-REAL b₁),R^1 st ( for b₃ being Point of (TOP-REAL b₁) holds b₂ . b₃ = |.b₃.| ) holds
b₂ is continuous

proof end;

theorem Th92: :: JORDAN2C:92

for b₁ being Nat ex b₂ being Function of (TOP-REAL b₁),R^1 st
( ( for b₃ being Point of (TOP-REAL b₁) holds b₂ . b₃ = |.b₃.| ) & b₂ is continuous )

proof end;

definition

let c₁, c₂ be non empty 1-sorted ;
let c₃ be Function of c₁,c₂;
let c₄ be set ;
assume E91: c₄ is Point of c₁ ;
canceled;
func pi c₃,c₄ -> Point of a₂ equals :Def10: :: JORDAN2C:def 10
a₃ . a₄;
coherence

proof end;

end;

:: deftheorem Def9 JORDAN2C:def 9 :

:: deftheorem Def10 defines pi JORDAN2C:def 10 :

theorem Th93: :: JORDAN2C:93

for b₁ being Nat
for b₂ being Function of I[01] ,(TOP-REAL b₁) st b₂ is continuous holds
ex b₃ being Function of I[01] ,R^1 st
( ( for b₄ being Point of I[01] holds b₃ . b₄ = |.(b₂ . b₄).| ) & b₃ is continuous )

proof end;

theorem Th94: :: JORDAN2C:94

for b₁ being Nat
for b₂ being Function of I[01] ,(TOP-REAL b₁)
for b₃ being Real st b₂ is continuous & |.(pi b₂,0).| <= b₃ & b₃ <= |.(pi b₂,1).| holds
ex b₄ being Point of I[01] st |.(pi b₂,b₄).| = b₃

proof end;

theorem Th95: :: JORDAN2C:95

for b₁ being Nat
for b₂ being Real
for b₃ being Point of (TOP-REAL b₁) st b₃ = <*b₂*> holds
|.b₃.| = abs b₂

proof end;

theorem Th96: :: JORDAN2C:96

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃ being Real st b₁ >= 1 & b₃ > 0 & b₂ = { b₄ where B is Point of (TOP-REAL b₁) : |.b₄.| = b₃ } holds
ex b₄ being Subset of (TOP-REAL b₁) st
( b₄ is_inside_component_of b₂ & b₄ = BDD b₂ )

proof end;

theorem Th97: :: JORDAN2C:97

for b₁ being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( len (GoB (SpStSeq b₁)) = 2 & width (GoB (SpStSeq b₁)) = 2 & (SpStSeq b₁) /. 1 = (GoB (SpStSeq b₁)) * 1,2 & (SpStSeq b₁) /. 2 = (GoB (SpStSeq b₁)) * 2,2 & (SpStSeq b₁) /. 3 = (GoB (SpStSeq b₁)) * 2,1 & (SpStSeq b₁) /. 4 = (GoB (SpStSeq b₁)) * 1,1 & (SpStSeq b₁) /. 5 = (GoB (SpStSeq b₁)) * 1,2 )

proof end;

theorem Th98: :: JORDAN2C:98

for b₁ being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds not LeftComp (SpStSeq b₁) is Bounded

proof end;

theorem Th99: :: JORDAN2C:99

for b₁ being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds LeftComp (SpStSeq b₁) c= UBD (L~ (SpStSeq b₁))

proof end;

theorem Th100: :: JORDAN2C:100

for b₁ being TopSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂ is_a_component_of b₁ & b₃ is_a_component_of b₁ & b₄ is connected & b₂ meets b₄ & b₃ meets b₄ holds
b₂ = b₃

proof end;

theorem Th101: :: JORDAN2C:101

for b₁ being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2) st b₂ is_a_component_of (L~ (SpStSeq b₁)) ` & not b₂ is Bounded holds
b₂ = LeftComp (SpStSeq b₁)

proof end;

theorem Th102: :: JORDAN2C:102

for b₁ being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( RightComp (SpStSeq b₁) c= BDD (L~ (SpStSeq b₁)) & RightComp (SpStSeq b₁) is Bounded )

proof end;

theorem Th103: :: JORDAN2C:103

for b₁ being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( LeftComp (SpStSeq b₁) = UBD (L~ (SpStSeq b₁)) & RightComp (SpStSeq b₁) = BDD (L~ (SpStSeq b₁)) )

proof end;

theorem Th104: :: JORDAN2C:104

for b₁ being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( UBD (L~ (SpStSeq b₁)) <> {} & UBD (L~ (SpStSeq b₁)) is_outside_component_of L~ (SpStSeq b₁) & BDD (L~ (SpStSeq b₁)) <> {} & BDD (L~ (SpStSeq b₁)) is_inside_component_of L~ (SpStSeq b₁) )

proof end;

theorem Th105: :: JORDAN2C:105

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ ` <> {} holds
( b₂ is boundary iff for b₃ being set
for b₄ being Subset of b₁ st b₃ in b₂ & b₃ in b₄ & b₄ is open holds
ex b₅ being Subset of b₁ st
( b₅ is_a_component_of b₂ ` & b₄ meets b₅ ) )

proof end;

theorem Th106: :: JORDAN2C:106

for b₁ being Subset of (TOP-REAL 2) st b₁ ` <> {} holds
( ( b₁ is boundary & b₁ is Jordan ) iff ex b₂, b₃ being Subset of (TOP-REAL 2) st
( b₁ ` = b₂ \/ b₃ & b₂ misses b₃ & (Cl b₂) \ b₂ = (Cl b₃) \ b₃ & b₁ = (Cl b₂) \ b₂ & ( for b₄, b₅ being Subset of ((TOP-REAL 2) | (b₁ ` )) st b₄ = b₂ & b₅ = b₃ holds
( b₄ is_a_component_of (TOP-REAL 2) | (b₁ ` ) & b₅ is_a_component_of (TOP-REAL 2) | (b₁ ` ) ) ) ) )

proof end;

theorem Th107: :: JORDAN2C:107

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁)
for b₃ being Subset of (TOP-REAL b₁) st b₁ >= 1 & b₃ = {b₂} holds
b₃ is boundary

proof end;

theorem Th108: :: JORDAN2C:108

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

proof end;

theorem Th109: :: JORDAN2C:109

for b₁, b₂ being Point of (TOP-REAL 2) holds LSeg b₁,b₂ is boundary

proof end;

registration

let c₁, c₂ be Point of (TOP-REAL 2);
cluster LSeg a₁,a₂ -> boundary ;
coherence by Th109;

end;

theorem Th110: :: JORDAN2C:110

for b₁ being FinSequence of (TOP-REAL 2) holds L~ b₁ is boundary

proof end;

registration

let c₁ be FinSequence of (TOP-REAL 2);
cluster L~ a₁ -> boundary Bounded ;
coherence by Th110;

end;

theorem Th111: :: JORDAN2C:111

for b₁ being Nat
for b₂ being Real
for b₃ being Point of (Euclid b₁)
for b₄, b₅ being Point of (TOP-REAL b₁) st b₄ = b₃ & b₅ in Ball b₃,b₂ holds
( |.(b₄ - b₅).| < b₂ & |.(b₅ - b₄).| < b₂ )

proof end;

theorem Th112: :: JORDAN2C:112

for b₁ being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂ being Real
for b₃ being Point of (TOP-REAL 2) st b₂ > 0 & b₃ in L~ (SpStSeq b₁) holds
ex b₄ being Point of (TOP-REAL 2) st
( b₄ in UBD (L~ (SpStSeq b₁)) & |.(b₃ - b₄).| < b₂ )

proof end;

theorem Th113: :: JORDAN2C:113

REAL 0 = {(0.REAL 0)}

proof end;

theorem Th114: :: JORDAN2C:114

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) st b₂ is Bounded holds
BDD b₂ is Bounded

proof end;

theorem Th115: :: JORDAN2C:115

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₂ is_a_component_of b₁ & b₃ is_a_component_of b₁ & b₄ is_a_component_of b₁ & b₂ \/ b₃ = the carrier of b₁ & b₄ misses b₂ holds
b₄ = b₃

proof end;

theorem Th116: :: JORDAN2C:116

for b₁ being Subset of (TOP-REAL 2) st b₁ is Bounded & b₁ is Jordan holds
BDD b₁ is_inside_component_of b₁

proof end;

theorem Th117: :: JORDAN2C:117

for b₁ being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂ being Real
for b₃ being Point of (TOP-REAL 2) st b₂ > 0 & b₃ in L~ (SpStSeq b₁) holds
ex b₄ being Point of (TOP-REAL 2) st
( b₄ in BDD (L~ (SpStSeq b₁)) & |.(b₃ - b₄).| < b₂ )

proof end;

theorem Th118: :: JORDAN2C:118

for b₁ being non constant standard clockwise_oriented special_circular_sequence
for b₂ being Point of (TOP-REAL 2) st b₁ /. 1 = N-min (L~ b₁) & b₂ `1 < W-bound (L~ b₁) holds
b₂ in LeftComp b₁

proof end;

theorem Th119: :: JORDAN2C:119

for b₁ being non constant standard clockwise_oriented special_circular_sequence
for b₂ being Point of (TOP-REAL 2) st b₁ /. 1 = N-min (L~ b₁) & b₂ `1 > E-bound (L~ b₁) holds
b₂ in LeftComp b₁

proof end;

theorem Th120: :: JORDAN2C:120

for b₁ being non constant standard clockwise_oriented special_circular_sequence
for b₂ being Point of (TOP-REAL 2) st b₁ /. 1 = N-min (L~ b₁) & b₂ `2 < S-bound (L~ b₁) holds
b₂ in LeftComp b₁

proof end;

theorem Th121: :: JORDAN2C:121

for b₁ being non constant standard clockwise_oriented special_circular_sequence
for b₂ being Point of (TOP-REAL 2) st b₁ /. 1 = N-min (L~ b₁) & b₂ `2 > N-bound (L~ b₁) holds
b₂ in LeftComp b₁

proof end;