environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, EUCLID, PRE_TOPC, FINSEQ_1, REAL_1, TOPREAL1, PARTFUN1, XBOOLE_0, RCOMP_1, RELAT_2, XXREAL_0, RELAT_1, FUNCT_1, TOPREAL2, MCART_1, METRIC_1, ARYTM_3, TARSKI, RLTOPSP1, ORDINAL4, NAT_1, CARD_1, ARYTM_1, PCOMPS_1, STRUCT_0, TOPREAL4;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, STRUCT_0, PRE_TOPC, CONNSP_1, METRIC_1, PCOMPS_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, XXREAL_0;
definitions TARSKI, TOPREAL1, XBOOLE_0;
theorems TARSKI, NAT_1, ZFMISC_1, FUNCT_1, FINSEQ_1, PRE_TOPC, CONNSP_1, EUCLID, TOPMETR, TOPREAL1, TOPREAL2, TOPREAL3, FINSEQ_4, FINSEQ_3, TBSP_1, PARTFUN2, RELAT_1, INT_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, PARTFUN1, ORDINAL1, RLTOPSP1;
schemes NAT_1;
registrations XBOOLE_0, RELSET_1, XREAL_0, NAT_1, MEMBERED, STRUCT_0, PRE_TOPC, EUCLID, ORDINAL1;
constructors HIDDEN, PARTFUN1, XXREAL_0, REAL_1, NAT_1, FINSEQ_4, CONNSP_1, PCOMPS_1, TOPREAL1, TOPREAL2, RELSET_1, FUNCSDOM, DOMAIN_1, COMPLEX1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities TOPREAL1, STRUCT_0;
expansions TARSKI, TOPREAL1, XBOOLE_0;
theorem Th8:
for
p,
q being
Point of
(TOP-REAL 2) for
f being
FinSequence of
(TOP-REAL 2) for
r being
Real for
u being
Point of
(Euclid 2) st
p `1 <> q `1 &
p `2 <> q `2 &
p in Ball (
u,
r) &
q in Ball (
u,
r) &
|[(p `1),(q `2)]| in Ball (
u,
r) &
f = <*p,|[(p `1),(q `2)]|,q*> holds
(
f is
being_S-Seq &
f /. 1
= p &
f /. (len f) = q &
L~ f is_S-P_arc_joining p,
q &
L~ f c= Ball (
u,
r) )
theorem Th9:
for
p,
q being
Point of
(TOP-REAL 2) for
f being
FinSequence of
(TOP-REAL 2) for
r being
Real for
u being
Point of
(Euclid 2) st
p `1 <> q `1 &
p `2 <> q `2 &
p in Ball (
u,
r) &
q in Ball (
u,
r) &
|[(q `1),(p `2)]| in Ball (
u,
r) &
f = <*p,|[(q `1),(p `2)]|,q*> holds
(
f is
being_S-Seq &
f /. 1
= p &
f /. (len f) = q &
L~ f is_S-P_arc_joining p,
q &
L~ f c= Ball (
u,
r) )
theorem Th20:
for
p being
Point of
(TOP-REAL 2) for
f,
h being
FinSequence of
(TOP-REAL 2) for
r being
Real for
u being
Point of
(Euclid 2) st
f /. (len f) in Ball (
u,
r) &
p in Ball (
u,
r) &
|[(p `1),((f /. (len f)) `2)]| in Ball (
u,
r) &
f is
being_S-Seq &
p `1 <> (f /. (len f)) `1 &
p `2 <> (f /. (len f)) `2 &
h = f ^ <*|[(p `1),((f /. (len f)) `2)]|,p*> &
((LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) \/ (LSeg (|[(p `1),((f /. (len f)) `2)]|,p))) /\ (L~ f) = {(f /. (len f))} holds
(
L~ h is_S-P_arc_joining f /. 1,
p &
L~ h c= (L~ f) \/ (Ball (u,r)) )
theorem Th21:
for
p being
Point of
(TOP-REAL 2) for
f,
h being
FinSequence of
(TOP-REAL 2) for
r being
Real for
u being
Point of
(Euclid 2) st
f /. (len f) in Ball (
u,
r) &
p in Ball (
u,
r) &
|[((f /. (len f)) `1),(p `2)]| in Ball (
u,
r) &
f is
being_S-Seq &
p `1 <> (f /. (len f)) `1 &
p `2 <> (f /. (len f)) `2 &
h = f ^ <*|[((f /. (len f)) `1),(p `2)]|,p*> &
((LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) \/ (LSeg (|[((f /. (len f)) `1),(p `2)]|,p))) /\ (L~ f) = {(f /. (len f))} holds
(
L~ h is_S-P_arc_joining f /. 1,
p &
L~ h c= (L~ f) \/ (Ball (u,r)) )
Lm1:
TopSpaceMetr (Euclid 2) = TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #)
by EUCLID:def 8;