:: JORDAN16 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
theorem :: JORDAN16:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: JORDAN16:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
X being
set st
a in X &
b in X &
c in X holds
{a,b,c} c= X
theorem :: JORDAN16:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: JORDAN16:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th5: :: JORDAN16:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th6: :: JORDAN16:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th7: :: JORDAN16:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th8: :: JORDAN16:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th9: :: JORDAN16:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
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
(
q1 in Segment A,
p1,
p2,
q1,
q2 &
q2 in Segment A,
p1,
p2,
q1,
q2 )
theorem :: JORDAN16:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: JORDAN16:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th12: :: JORDAN16:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th13: :: JORDAN16:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th14: :: JORDAN16:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th15: :: JORDAN16:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th16: :: JORDAN16:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: JORDAN16:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: JORDAN16:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th19: :: JORDAN16:19
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th20: :: JORDAN16:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
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_homeomorphism &
g . 0
= p1 &
g . 1
= p2 &
g . s1 = q1 &
g . s2 = q2 & 0
<= s1 &
s1 <= s2 &
s2 <= 1 )
theorem Th21: :: JORDAN16:21
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
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_homeomorphism &
g . 0
= p1 &
g . 1
= p2 &
g . s1 = q1 &
g . s2 = q2 & 0
<= s1 &
s1 < s2 &
s2 <= 1 )
theorem :: JORDAN16:22
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
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
not
Segment A,
p1,
p2,
q1,
q2 is
empty
theorem :: JORDAN16:23
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def1 defines continuous JORDAN16:def 1 :
:: deftheorem defines continuous JORDAN16:def 2 :
:: deftheorem Def3 defines AffineMap JORDAN16:def 3 :
theorem :: JORDAN16:24
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th25: :: JORDAN16:25
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th26: :: JORDAN16:26
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th27: :: JORDAN16:27
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: JORDAN16:28
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: JORDAN16:29
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th30: :: JORDAN16:30
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: JORDAN16:31
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th32: :: JORDAN16:32
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th33: :: JORDAN16:33
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th34: :: JORDAN16:34
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th35: :: JORDAN16:35
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th36: :: JORDAN16:36
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
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
theorem :: JORDAN16:37
:: Showing IDV graph ... (Click the Palm Tree again to close it) 