environ
vocabularies HIDDEN, NUMBERS, PRE_TOPC, EUCLID, SUPINF_2, COMPLEX1, XXREAL_0, CARD_1, XBOOLE_0, FUNCT_1, TOPMETR, SUBSET_1, ORDINAL2, PARTFUN1, RCOMP_1, REAL_1, TARSKI, STRUCT_0, RELAT_1, ARYTM_3, TOPS_2, ARYTM_1, SQUARE_1, NAT_1, METRIC_1, XXREAL_2, PCOMPS_1, MCART_1, FUNCT_4, JGRAPH_4, FUNCT_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, COMPLEX1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, DOMAIN_1, STRUCT_0, PARTFUN1, TOPMETR, RLVECT_1, EUCLID, COMPTS_1, TOPS_2, METRIC_1, PCOMPS_1, SQUARE_1, TBSP_1, PSCOMP_1, PRE_TOPC, RLTOPSP1, FUNCT_4, XXREAL_0;
definitions TARSKI;
theorems TARSKI, RELAT_1, SUBSET_1, FUNCT_1, FUNCT_2, FUNCT_4, TOPS_1, TOPS_2, PARTFUN1, PRE_TOPC, TOPMETR, JORDAN6, EUCLID, JGRAPH_1, SQUARE_1, PSCOMP_1, METRIC_1, JGRAPH_2, GOBOARD6, GOBOARD9, TBSP_1, TOPREAL6, JGRAPH_3, ABSVALUE, JORDAN2C, TSEP_1, XREAL_0, XBOOLE_0, XBOOLE_1, TOPRNS_1, XCMPLX_0, XCMPLX_1, COMPLEX1, XREAL_1, JORDAN2B, XXREAL_0, RLVECT_1;
schemes FUNCT_2, DOMAIN_1, JGRAPH_2, BINOP_2, JGRAPH_3;
registrations XBOOLE_0, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, MEMBERED, STRUCT_0, PRE_TOPC, EUCLID, TOPMETR, TOPREAL1, PSCOMP_1, FUNCT_2, COMPTS_1, TBSP_1, RELSET_1, FUNCT_1, JORDAN2C, ORDINAL1;
constructors HIDDEN, FUNCT_4, REAL_1, SQUARE_1, BINOP_2, COMPLEX1, TOPS_2, COMPTS_1, TBSP_1, TOPMETR, PSCOMP_1, FUNCSDOM, PCOMPS_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities SQUARE_1, STRUCT_0, PCOMPS_1, ALGSTR_0;
expansions TARSKI;
Lm1:
for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) holds
|.p.| > 0
Lm2:
for K being non empty Subset of (TOP-REAL 2) holds
( proj1 | K is continuous Function of ((TOP-REAL 2) | K),R^1 & ( for q being Point of ((TOP-REAL 2) | K) holds (proj1 | K) . q = proj1 . q ) )
Lm3:
for K being non empty Subset of (TOP-REAL 2) holds
( proj2 | K is continuous Function of ((TOP-REAL 2) | K),R^1 & ( for q being Point of ((TOP-REAL 2) | K) holds (proj2 | K) . q = proj2 . q ) )
Lm4:
dom (2 NormF) = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
Lm5:
for K being non empty Subset of (TOP-REAL 2) holds
( (2 NormF) | K is continuous Function of ((TOP-REAL 2) | K),R^1 & ( for q being Point of ((TOP-REAL 2) | K) holds ((2 NormF) | K) . q = (2 NormF) . q ) )
Lm6:
for K1 being non empty Subset of (TOP-REAL 2)
for g1 being Function of ((TOP-REAL 2) | K1),R^1 st g1 = (2 NormF) | K1 & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
q <> 0. (TOP-REAL 2) ) holds
for q being Point of ((TOP-REAL 2) | K1) holds g1 . q <> 0
Lm7:
for sn being Real
for K1 being Subset of (TOP-REAL 2) st K1 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `2 >= sn * |.p7.| } holds
K1 is closed
Lm8:
for sn being Real
for K1 being Subset of (TOP-REAL 2) st K1 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `1 >= sn * |.p7.| } holds
K1 is closed
Lm9:
for sn being Real
for K1 being Subset of (TOP-REAL 2) st K1 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `2 <= sn * |.p7.| } holds
K1 is closed
Lm10:
for sn being Real
for K1 being Subset of (TOP-REAL 2) st K1 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `1 <= sn * |.p7.| } holds
K1 is closed
Lm11:
TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2)
by EUCLID:def 8;
Lm12:
for q4, q, p2 being Point of (TOP-REAL 2)
for O, u, uq being Point of (Euclid 2) st u in cl_Ball (O,(|.p2.| + 1)) & q = uq & q4 = u & O = 0. (TOP-REAL 2) & |.q4.| = |.q.| holds
q in cl_Ball (O,(|.p2.| + 1))