:: JORDAN16 semantic presentation

theorem Th1: :: JORDAN16:1

for b₁ being non empty finite Subset of REAL
for b₂ being Real st ( for b₃ being Real st b₃ in b₁ holds
b₃ < b₂ ) holds
max b₁ < b₂

proof end;

registration

let c₁ be Nat;
cluster trivial Element of K40(the carrier of (TOP-REAL a₁));
existence

proof end;

end;

theorem Th2: :: JORDAN16:2

for b₁, b₂, b₃, b₄ being set st b₁ in b₄ & b₂ in b₄ & b₃ in b₄ holds
{b₁,b₂,b₃} c= b₄

proof end;

theorem Th3: :: JORDAN16:3

for b₁ being Nat holds {} (TOP-REAL b₁) is Bounded

proof end;

theorem Th4: :: JORDAN16:4

for b₁ being Simple_closed_curve holds Lower_Arc b₁ <> Upper_Arc b₁

proof end;

theorem Th5: :: JORDAN16:5

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL 2) holds Segment b₁,b₂,b₃,b₄,b₅ c= b₁

proof end;

theorem Th6: :: JORDAN16:6

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
b₁ | b₂ is SubSpace of b₁ | b₃

proof end;

theorem Th7: :: JORDAN16:7

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₁ is_an_arc_of b₂,b₃ & b₄ in b₁ holds
b₄ in L_Segment b₁,b₂,b₃,b₄

proof end;

theorem Th8: :: JORDAN16:8

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₁ is_an_arc_of b₂,b₃ & b₄ in b₁ holds
b₄ in R_Segment b₁,b₂,b₃,b₄

proof end;

theorem Th9: :: JORDAN16:9

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL 2) st b₁ is_an_arc_of b₂,b₃ & LE b₄,b₅,b₁,b₂,b₃ holds
( b₄ in Segment b₁,b₂,b₃,b₄,b₅ & b₅ in Segment b₁,b₂,b₃,b₄,b₅ )

proof end;

theorem Th10: :: JORDAN16:10

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

proof end;

theorem Th11: :: JORDAN16:11

for b₁ being Simple_closed_curve
for b₂, b₃ being Point of (TOP-REAL 2) st b₂ in b₁ & b₃ in b₁ & not LE b₂,b₃,b₁ holds
LE b₃,b₂,b₁

proof end;

theorem Th12: :: JORDAN16:12

for b₁, b₂ being non empty TopSpace
for b₃ being non empty SubSpace of b₂
for b₄ being Function of b₁,b₂
for b₅ being Function of b₁,b₃ st b₄ = b₅ & b₄ is continuous holds
b₅ is continuous

proof end;

theorem Th13: :: JORDAN16:13

for b₁, b₂ being non empty TopSpace
for b₃ being non empty SubSpace of b₁
for b₄ being non empty SubSpace of b₂
for b₅ being Function of b₁,b₂ st b₅ is_homeomorphism holds
for b₆ being Function of b₃,b₄ st b₆ = b₅ | b₃ & b₆ is onto holds
b₆ is_homeomorphism

proof end;

theorem Th14: :: JORDAN16:14

for b₁, b₂, b₃ being Subset of (TOP-REAL 2)
for b₄, b₅ being Point of (TOP-REAL 2) st b₁ is_an_arc_of b₄,b₅ & b₂ is_an_arc_of b₄,b₅ & b₃ is_an_arc_of b₄,b₅ & b₂ /\ b₃ = {b₄,b₅} & b₁ c= b₂ \/ b₃ & not b₁ = b₂ holds
b₁ = b₃

proof end;

theorem Th15: :: JORDAN16:15

for b₁ being Simple_closed_curve
for b₂, b₃ being Subset of (TOP-REAL 2)
for b₄, b₅ being Point of (TOP-REAL 2) st b₂ is_an_arc_of b₄,b₅ & b₃ is_an_arc_of b₄,b₅ & b₂ c= b₁ & b₃ c= b₁ & b₂ <> b₃ holds
( b₂ \/ b₃ = b₁ & b₂ /\ b₃ = {b₄,b₅} )

proof end;

theorem Th16: :: JORDAN16:16

for b₁, b₂ being Subset of (TOP-REAL 2)
for b₃, b₄, b₅, b₆ being Point of (TOP-REAL 2) st b₁ is_an_arc_of b₃,b₄ & b₁ /\ b₂ = {b₅,b₆} holds
b₁ <> b₂

proof end;

theorem Th17: :: JORDAN16:17

proof end;

theorem Th18: :: JORDAN16:18

for b₁ being Simple_closed_curve
for b₂, b₃ being Subset of (TOP-REAL 2)
for b₄, b₅ being Point of (TOP-REAL 2) st b₂ c= b₁ & b₃ c= b₁ & b₂ <> b₃ & b₂ is_an_arc_of b₄,b₅ & b₃ is_an_arc_of b₄,b₅ holds
for b₆ being Subset of (TOP-REAL 2) st b₆ is_an_arc_of b₄,b₅ & b₆ c= b₁ & not b₆ = b₂ holds
b₆ = b₃

proof end;

theorem Th19: :: JORDAN16:19

for b₁ being Simple_closed_curve
for b₂ being non empty Subset of (TOP-REAL 2) st b₂ is_an_arc_of W-min b₁, E-max b₁ & b₂ c= b₁ & not b₂ = Lower_Arc b₁ holds
b₂ = Upper_Arc b₁

proof end;

theorem Th20: :: JORDAN16:20

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL 2) st b₁ is_an_arc_of b₂,b₃ & LE b₄,b₅,b₁,b₂,b₃ holds
ex b₆ being Function of I[01] ,((TOP-REAL 2) | b₁)ex b₇, b₈ being Real st
( b₆ is_homeomorphism & b₆ . 0 = b₂ & b₆ . 1 = b₃ & b₆ . b₇ = b₄ & b₆ . b₈ = b₅ & 0 <= b₇ & b₇ <= b₈ & b₈ <= 1 )

proof end;

theorem Th21: :: JORDAN16:21

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL 2) st b₁ is_an_arc_of b₂,b₃ & LE b₄,b₅,b₁,b₂,b₃ & b₄ <> b₅ holds
ex b₆ being Function of I[01] ,((TOP-REAL 2) | b₁)ex b₇, b₈ being Real st
( b₆ is_homeomorphism & b₆ . 0 = b₂ & b₆ . 1 = b₃ & b₆ . b₇ = b₄ & b₆ . b₈ = b₅ & 0 <= b₇ & b₇ < b₈ & b₈ <= 1 )

proof end;

theorem Th22: :: JORDAN16:22

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL 2) st b₁ is_an_arc_of b₂,b₃ & LE b₄,b₅,b₁,b₂,b₃ holds
not Segment b₁,b₂,b₃,b₄,b₅ is empty

proof end;

theorem Th23: :: JORDAN16:23

for b₁ being Simple_closed_curve
for b₂ being Point of (TOP-REAL 2) st b₂ in b₁ holds
( b₂ in Segment b₂,(W-min b₁),b₁ & W-min b₁ in Segment b₂,(W-min b₁),b₁ )

proof end;

definition

let c₁ be PartFunc of REAL , REAL ;
attr a₁ is continuous means :Def1: :: JORDAN16:def 1
a₁ is_continuous_on dom a₁;

end;

:: deftheorem Def1 defines continuous JORDAN16:def 1 :

definition

let c₁ be Function of REAL , REAL ;
redefine attr a₁ is continuous means :: JORDAN16:def 2
a₁ is_continuous_on REAL ;
compatibility

proof end;

end;

:: deftheorem Def2 defines continuous JORDAN16:def 2 :

definition

let c₁, c₂ be real number ;
func AffineMap c₁,c₂ -> Function of REAL , REAL means :Def3: :: JORDAN16:def 3
for b₁ being real number holds a₃ . b₁ = (a₁ * b₁) + a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines AffineMap JORDAN16:def 3 :

registration

let c₁, c₂ be real number ;
cluster AffineMap a₁,a₂ -> continuous ;
coherence

proof end;

end;

registration

cluster continuous M5( REAL , REAL );
existence

proof end;

end;

theorem Th24: :: JORDAN16:24

for b₁, b₂ being continuous PartFunc of REAL , REAL holds b₂ * b₁ is continuous PartFunc of REAL , REAL

proof end;

theorem Th25: :: JORDAN16:25

for b₁, b₂ being real number holds (AffineMap b₁,b₂) . 0 = b₂

proof end;

theorem Th26: :: JORDAN16:26

for b₁, b₂ being real number holds (AffineMap b₁,b₂) . 1 = b₁ + b₂

proof end;

theorem Th27: :: JORDAN16:27

for b₁, b₂ being real number st b₁ <> 0 holds
AffineMap b₁,b₂ is one-to-one

proof end;

theorem Th28: :: JORDAN16:28

for b₁, b₂, b₃, b₄ being real number st b₁ > 0 & b₃ < b₄ holds
(AffineMap b₁,b₂) . b₃ < (AffineMap b₁,b₂) . b₄

proof end;

theorem Th29: :: JORDAN16:29

for b₁, b₂, b₃, b₄ being real number st b₁ < 0 & b₃ < b₄ holds
(AffineMap b₁,b₂) . b₃ > (AffineMap b₁,b₂) . b₄

proof end;

theorem Th30: :: JORDAN16:30

for b₁, b₂, b₃, b₄ being real number st b₁ >= 0 & b₃ <= b₄ holds
(AffineMap b₁,b₂) . b₃ <= (AffineMap b₁,b₂) . b₄

proof end;

theorem Th31: :: JORDAN16:31

for b₁, b₂, b₃, b₄ being real number st b₁ <= 0 & b₃ <= b₄ holds
(AffineMap b₁,b₂) . b₃ >= (AffineMap b₁,b₂) . b₄

proof end;

theorem Th32: :: JORDAN16:32

for b₁, b₂ being real number st b₁ <> 0 holds
rng (AffineMap b₁,b₂) = REAL

proof end;

theorem Th33: :: JORDAN16:33

for b₁, b₂ being real number st b₁ <> 0 holds
(AffineMap b₁,b₂) " = AffineMap (b₁ " ),(- (b₂ / b₁))

proof end;

theorem Th34: :: JORDAN16:34

for b₁, b₂ being real number st b₁ > 0 holds
(AffineMap b₁,b₂) .: [.0,1.] = [.b₂,(b₁ + b₂).]

proof end;

theorem Th35: :: JORDAN16:35

for b₁ being Function of R^1 ,R^1
for b₂, b₃ being Real st b₂ <> 0 & b₁ = AffineMap b₂,b₃ holds
b₁ is_homeomorphism

proof end;

theorem Th36: :: JORDAN16:36

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL 2) st b₁ is_an_arc_of b₂,b₃ & LE b₄,b₅,b₁,b₂,b₃ & b₄ <> b₅ holds
Segment b₁,b₂,b₃,b₄,b₅ is_an_arc_of b₄,b₅

proof end;

theorem Th37: :: JORDAN16:37

for b₁ being Simple_closed_curve
for b₂, b₃ being Point of (TOP-REAL 2)
for b₄ being Subset of (TOP-REAL 2) st b₄ c= b₁ & b₄ is_an_arc_of b₂,b₃ & W-min b₁ in b₄ & E-max b₁ in b₄ & not Upper_Arc b₁ c= b₄ holds
Lower_Arc b₁ c= b₄

proof end;