:: TOPREAL5 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for a, b, c being real number holds
( c in [.a,b.] iff ( a <= c & c <= b ) )
by RCOMP_1:48;

Lm2: for X, Y, Z being non empty TopSpace
for f being continuous Function of X,Y
for g being continuous Function of Y,Z holds g * f is continuous Function of X,Z
;

theorem :: TOPREAL5:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOPREAL5:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOPREAL5:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th4: :: TOPREAL5:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for A, B1, B2 being Subset of X st B1 is open & B2 is open & B1 meets A & B2 meets A & A c= B1 \/ B2 & B1 misses B2 holds
not A is connected
proof end;

theorem Th5: :: TOPREAL5:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for f being continuous Function of X,Y
for A being Subset of X st A is connected holds
f .: A is connected
proof end;

theorem Th6: :: TOPREAL5:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ra, rb being real number st ra <= rb holds
[#] (Closed-Interval-TSpace ra,rb) is connected
proof end;

Lm3: for A being Subset of R^1
for a being real number st A = { r where r is Element of REAL : a < r } holds
A is open
by JORDAN2B:31;

Lm4: for A being Subset of R^1
for a being real number st A = { r where r is Element of REAL : a > r } holds
A is open
by JORDAN2B:30;

theorem :: TOPREAL5:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOPREAL5:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th9: :: TOPREAL5:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Subset of R^1
for a being real number st not a in A & ex b, d being real number st
( b in A & d in A & b < a & a < d ) holds
not A is connected
proof end;

theorem :: TOPREAL5:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for xa, xb being Point of X
for a, b, d being Real
for f being continuous Function of X,R^1 st X is connected & f . xa = a & f . xb = b & a <= d & d <= b holds
ex xc being Point of X st f . xc = d
proof end;

theorem :: TOPREAL5:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for xa, xb being Point of X
for B being Subset of X
for a, b, d being Real
for f being continuous Function of X,R^1 st B is connected & f . xa = a & f . xb = b & a <= d & d <= b & xa in B & xb in B holds
ex xc being Point of X st
( xc in B & f . xc = d )
proof end;

theorem Th12: :: TOPREAL5:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ra, rb, a, b being real number st ra < rb holds
for f being continuous Function of (Closed-Interval-TSpace ra,rb),R^1
for d being real number st f . ra = a & f . rb = b & a < d & d < b holds
ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb )
proof end;

theorem Th13: :: TOPREAL5:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ra, rb, a, b being real number st ra < rb holds
for f being continuous Function of (Closed-Interval-TSpace ra,rb),R^1
for d being real number st f . ra = a & f . rb = b & a > d & d > b holds
ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb )
proof end;

theorem :: TOPREAL5:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ra, rb being real number
for g being continuous Function of (Closed-Interval-TSpace ra,rb),R^1
for s1, s2 being real number st ra < rb & s1 * s2 < 0 & s1 = g . ra & s2 = g . rb holds
ex r1 being Element of REAL st
( g . r1 = 0 & ra < r1 & r1 < rb )
proof end;

theorem Th15: :: TOPREAL5:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for g being Function of I[01] ,R^1
for s1, s2 being real number st g is continuous & g . 0 <> g . 1 & s1 = g . 0 & s2 = g . 1 holds
ex r1 being Element of REAL st
( 0 < r1 & r1 < 1 & g . r1 = (s1 + s2) / 2 )
proof end;

theorem Th16: :: TOPREAL5:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function of (TOP-REAL 2),R^1 st f = proj1 holds
f is continuous
proof end;

theorem Th17: :: TOPREAL5:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function of (TOP-REAL 2),R^1 st f = proj2 holds
f is continuous
proof end;

theorem Th18: :: TOPREAL5:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty Subset of (TOP-REAL 2)
for f being Function of I[01] ,((TOP-REAL 2) | P) st f is continuous holds
ex g being Function of I[01] ,R^1 st
( g is continuous & ( for r being Element of REAL
for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `1 = g . r ) )
proof end;

theorem Th19: :: TOPREAL5:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty Subset of (TOP-REAL 2)
for f being Function of I[01] ,((TOP-REAL 2) | P) st f is continuous holds
ex g being Function of I[01] ,R^1 st
( g is continuous & ( for r being Element of REAL
for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `2 = g . r ) )
proof end;

theorem Th20: :: TOPREAL5:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds
for r being Element of REAL ex p being Point of (TOP-REAL 2) st
( p in P & not p `2 = r )
proof end;

theorem Th21: :: TOPREAL5:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds
for r being Element of REAL ex p being Point of (TOP-REAL 2) st
( p in P & not p `1 = r )
proof end;

theorem Th22: :: TOPREAL5:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) st C is_simple_closed_curve holds
N-bound C > S-bound C
proof end;

theorem Th23: :: TOPREAL5:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) st C is_simple_closed_curve holds
E-bound C > W-bound C
proof end;

theorem :: TOPREAL5:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty compact Subset of (TOP-REAL 2) st P is_simple_closed_curve holds
S-min P <> N-max P
proof end;

theorem :: TOPREAL5:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty compact Subset of (TOP-REAL 2) st P is_simple_closed_curve holds
W-min P <> E-max P
proof end;