let n be Nat; for a being Real
for P being Subset of (TOP-REAL n) st n >= 2 & P = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } holds
P is connected
let a be Real; for P being Subset of (TOP-REAL n) st n >= 2 & P = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } holds
P is connected
let P be Subset of (TOP-REAL n); ( n >= 2 & P = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } implies P is connected )
assume A1:
( n >= 2 & P = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } )
; P is connected
then reconsider Q = P as non empty Subset of (TOP-REAL n) by Th39, XXREAL_0:2;
for w1, w7 being Point of (TOP-REAL n) st w1 in Q & w7 in Q & w1 <> w7 holds
ex f being Function of I[01],((TOP-REAL n) | Q) st
( f is continuous & w1 = f . 0 & w7 = f . 1 )
proof
let w1,
w7 be
Point of
(TOP-REAL n);
( w1 in Q & w7 in Q & w1 <> w7 implies ex f being Function of I[01],((TOP-REAL n) | Q) st
( f is continuous & w1 = f . 0 & w7 = f . 1 ) )
assume that A2:
(
w1 in Q &
w7 in Q )
and
w1 <> w7
;
ex f being Function of I[01],((TOP-REAL n) | Q) st
( f is continuous & w1 = f . 0 & w7 = f . 1 )
per cases
( for r being Real holds
( not w1 = r * w7 & not w7 = r * w1 ) or ex r being Real st
( w1 = r * w7 or w7 = r * w1 ) )
;
suppose
ex
r being
Real st
(
w1 = r * w7 or
w7 = r * w1 )
;
ex f being Function of I[01],((TOP-REAL n) | Q) st
( f is continuous & w1 = f . 0 & w7 = f . 1 )then
ex
w2,
w3,
w4,
w5,
w6 being
Point of
(TOP-REAL n) st
(
w2 in Q &
w3 in Q &
w4 in Q &
w5 in Q &
w6 in Q &
LSeg (
w1,
w2)
c= Q &
LSeg (
w2,
w3)
c= Q &
LSeg (
w3,
w4)
c= Q &
LSeg (
w4,
w5)
c= Q &
LSeg (
w5,
w6)
c= Q &
LSeg (
w6,
w7)
c= Q )
by A1, A2, Th36;
hence
ex
f being
Function of
I[01],
((TOP-REAL n) | Q) st
(
f is
continuous &
w1 = f . 0 &
w7 = f . 1 )
by A2, Th27;
verum end; end;
end;
hence
P is connected
by JORDAN1:2; verum