environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, PRE_TOPC, FUNCT_1, SUBSET_1, RCOMP_1, ORDINAL2, FUNCT_4, RELAT_1, STRUCT_0, TARSKI, EUCLID, METRIC_1, COMPLEX1, ARYTM_1, ARYTM_3, SUPINF_2, MCART_1, CARD_1, JORDAN2C, FINSEQ_1, REAL_1, XXREAL_0, PCOMPS_1, SQUARE_1, TOPMETR, XXREAL_1, FUNCOP_1, PARTFUN1, BORSUK_1, JGRAPH_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, XXREAL_0, FUNCOP_1, FINSEQ_1, FINSEQ_2, NAT_1, DOMAIN_1, STRUCT_0, PRE_TOPC, PCOMPS_1, TOPMETR, METRIC_1, RCOMP_1, SQUARE_1, PSCOMP_1, RLVECT_1, EUCLID, FUNCT_4;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, RELAT_1, SUBSET_1, FUNCT_1, FUNCT_2, FUNCT_4, TOPS_1, TOPS_2, PARTFUN1, PRE_TOPC, REVROT_1, FINSEQ_2, FRECHET, TOPMETR, JORDAN6, EUCLID, JGRAPH_1, SQUARE_1, TOPREAL3, JORDAN5A, PSCOMP_1, METRIC_1, SPPOL_2, TSEP_1, XBOOLE_0, XBOOLE_1, XREAL_0, XCMPLX_0, XCMPLX_1, FUNCOP_1, XREAL_1, XXREAL_0, XXREAL_1;
schemes FUNCT_2, CLASSES1;
registrations RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, STRUCT_0, PRE_TOPC, BORSUK_1, MONOID_0, EUCLID, TOPMETR, PSCOMP_1, TOPS_1, ORDINAL1, VALUED_0, PARTFUN3;
constructors HIDDEN, FUNCT_4, REAL_1, SQUARE_1, RCOMP_1, MONOID_0, TOPMETR, PSCOMP_1, PCOMPS_1, FUNCOP_1, FUNCSDOM, FINSEQOP, MEASURE6, NUMBERS, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, SQUARE_1, EUCLID, STRUCT_0, XCMPLX_0;
expansions TARSKI, XBOOLE_0;
Lm1:
0. (TOP-REAL 2) = 0.REAL 2
by EUCLID:66;
theorem Th35:
for
K0,
B0 being
Subset of
(TOP-REAL 2) for
f being
Function of
((TOP-REAL 2) | K0),
((TOP-REAL 2) | B0) for
f1,
f2 being
Function of
((TOP-REAL 2) | K0),
R^1 st
f1 is
continuous &
f2 is
continuous &
K0 <> {} &
B0 <> {} & ( for
x,
y,
r,
s being
Real st
|[x,y]| in K0 &
r = f1 . |[x,y]| &
s = f2 . |[x,y]| holds
f . |[x,y]| = |[r,s]| ) holds
f is
continuous
Lm2:
now for p01, p02, px1, px2 being Real st (p01 - px1) - (p02 - px2) <= ((p01 - p02) / 4) - (- ((p01 - p02) / 4)) holds
(p01 - p02) / 2 <= px1 - px2
let p01,
p02,
px1,
px2 be
Real;
( (p01 - px1) - (p02 - px2) <= ((p01 - p02) / 4) - (- ((p01 - p02) / 4)) implies (p01 - p02) / 2 <= px1 - px2 )set r0 =
(p01 - p02) / 4;
assume
(p01 - px1) - (p02 - px2) <= ((p01 - p02) / 4) - (- ((p01 - p02) / 4))
;
(p01 - p02) / 2 <= px1 - px2then
(p01 - p02) - (px1 - px2) <= ((p01 - p02) / 4) + ((p01 - p02) / 4)
;
then
p01 - p02 <= (px1 - px2) + (((p01 - p02) / 4) + ((p01 - p02) / 4))
by XREAL_1:20;
then
(p01 - p02) - ((p01 - p02) / 2) <= px1 - px2
by XREAL_1:20;
hence
(p01 - p02) / 2
<= px1 - px2
;
verum
end;
deffunc H1( Point of (TOP-REAL 2)) -> object = $1 `1 ;
deffunc H2( Point of (TOP-REAL 2)) -> object = $1 `2 ;
Lm3:
for p, q being Point of (TOP-REAL 2) holds
( H1(p - q) = H1(p) - H1(q) & H2(p - q) = H2(p) - H2(q) )
by TOPREAL3:3;
Lm4:
for p, q being Point of (TOP-REAL 2) holds |.(p - q).| ^2 = (H1(p - q) ^2) + (H2(p - q) ^2)
by JGRAPH_1:29;
Lm5:
{ p7 where p7 is Point of (TOP-REAL 2) : H1(p7) <= H2(p7) } is closed Subset of (TOP-REAL 2)
from JGRAPH_2:sch 3(Lm3, Lm4);
Lm6:
for p, q being Point of (TOP-REAL 2) holds
( H2(p - q) = H2(p) - H2(q) & H1(p - q) = H1(p) - H1(q) )
by TOPREAL3:3;
Lm7:
for p, q being Point of (TOP-REAL 2) holds |.(p - q).| ^2 = (H2(p - q) ^2) + (H1(p - q) ^2)
by JGRAPH_1:29;
Lm8:
{ p7 where p7 is Point of (TOP-REAL 2) : H2(p7) <= H1(p7) } is closed Subset of (TOP-REAL 2)
from JGRAPH_2:sch 3(Lm6, Lm7);
deffunc H3( Point of (TOP-REAL 2)) -> object = - ($1 `1);
deffunc H4( Point of (TOP-REAL 2)) -> object = - ($1 `2);
Lm9:
now for p, q being Point of (TOP-REAL 2) holds
( H3(p - q) = H3(p) - H3(q) & H2(p - q) = H2(p) - H2(q) )
end;
Lm11:
{ p7 where p7 is Point of (TOP-REAL 2) : H3(p7) <= H2(p7) } is closed Subset of (TOP-REAL 2)
from JGRAPH_2:sch 3(Lm9, Lm10);
Lm12:
now for p, q being Point of (TOP-REAL 2) holds
( H2(p - q) = H2(p) - H2(q) & H3(p - q) = H3(p) - H3(q) )
end;
Lm14:
{ p7 where p7 is Point of (TOP-REAL 2) : H2(p7) <= H3(p7) } is closed Subset of (TOP-REAL 2)
from JGRAPH_2:sch 3(Lm12, Lm13);
Lm15:
now for p, q being Point of (TOP-REAL 2) holds
( H4(p - q) = H4(p) - H4(q) & H1(p - q) = H1(p) - H1(q) )
end;
Lm17:
{ p7 where p7 is Point of (TOP-REAL 2) : H4(p7) <= H1(p7) } is closed Subset of (TOP-REAL 2)
from JGRAPH_2:sch 3(Lm15, Lm16);
Lm18:
now for p, q being Point of (TOP-REAL 2) holds
( H1(p - q) = H1(p) - H1(q) & H4(p - q) = H4(p) - H4(q) )
end;
Lm20:
{ p7 where p7 is Point of (TOP-REAL 2) : H1(p7) <= H4(p7) } is closed Subset of (TOP-REAL 2)
from JGRAPH_2:sch 3(Lm18, Lm19);