environ
vocabularies HIDDEN, ARYTM_1, ARYTM_3, BROUWER, CARD_1, COMPLEX1, EUCLID, FUNCT_1, METRIC_1, NAT_1, NUMBERS, ORDINAL1, PCOMPS_1, PRE_TOPC, RCOMP_1, RELAT_1, STRUCT_0, SUBSET_1, SUPINF_2, TARSKI, TOPS_1, TOPS_2, XBOOLE_0, XREAL_0, XXREAL_0, XCMPLX_0, FINSET_1, ZFMISC_1, REAL_1, SETFAM_1, T_0TOPSP, CONNSP_2, MFOLD_1, RELAT_2, EQREL_1, CONNSP_1, CONNSP_3, MFOLD_0, WAYBEL23, COMPTS_1, RLVECT_3;
notations HIDDEN, TARSKI, XBOOLE_0, FINSET_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, COMPLEX1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, XXREAL_3, NAT_1, CARD_1, REAL_1, SETFAM_1, STRUCT_0, PRE_TOPC, TOPS_1, METRIC_1, PCOMPS_1, RLVECT_1, EUCLID, TOPREAL9, TOPS_2, CONNSP_1, CONNSP_2, CONNSP_3, COMPTS_1, BROUWER, DOMAIN_1, ZFMISC_1, MFOLD_1, BORSUK_1, BORSUK_2, NAT_D, BINOP_1, EQREL_1, BORSUK_3, WAYBEL23, CANTOR_1;
definitions TARSKI, XBOOLE_0;
theorems ABSVALUE, BORSUK_1, BROUWER, COMPTS_1, CONNSP_2, EUCLID, FUNCT_1, FUNCT_2, GOBOARD6, JORDAN24, JORDAN2C, ORDINAL1, PRE_TOPC, RELAT_1, RLVECT_1, SUBSET_1, TARSKI, TOPMETR, TOPREAL9, TOPRNS_1, TOPS_1, TOPS_2, XBOOLE_0, XBOOLE_1, XREAL_0, XREAL_1, XXREAL_0, ZFMISC_1, CARD_1, TSEP_1, SETFAM_1, BROUWER2, NAT_1, TOPGRP_1, JORDAN, METRIZTS, T_0TOPSP, MFOLD_1, BORSUK_3, EUCLID_2, TOPREALA, FUNCT_3, EQREL_1, TIETZE_2, CONNSP_1, CONNSP_3, CARD_2, WAYBEL23, YELLOW12, BROUWER3;
schemes FUNCT_2, NAT_1, CLASSES1;
registrations BORSUK_1, BROUWER, EUCLID, FUNCT_1, FUNCT_2, NAT_1, PRE_TOPC, RELAT_1, SIMPLEX2, STRUCT_0, SUBSET_1, TOPGRP_1, TOPS_1, XBOOLE_0, XREAL_0, XXREAL_0, RELSET_1, FINSET_1, TOPREALC, CARD_1, TOPREAL9, XXREAL_3, MFOLD_1, BORSUK_3, WAYBEL_2, XCMPLX_0, JORDAN1, BORSUK_2, CONNSP_1, ORDINAL1, METRIZTS, COMPTS_1, TOPREAL1;
constructors HIDDEN, MONOID_0, CONVEX1, TOPREAL9, TOPS_1, COMPTS_1, FUNCSDOM, BROUWER, SEQ_4, EUCLID_9, SIMPLEX0, CONNSP_1, CONNSP_3, BORSUK_3, MFOLD_1, NAT_D, BORSUK_2, WAYBEL23, CANTOR_1, REAL_1;
requirements HIDDEN, ARITHM, BOOLE, NUMERALS, SUBSET, REAL;
equalities BINOP_1, STRUCT_0, XCMPLX_0, TOPREAL9, BROUWER, ORDINAL1;
expansions TARSKI, XBOOLE_0;
Lm1:
for n being Nat
for p, q being Point of (TOP-REAL n)
for r, s being real number st r > 0 & s > 0 holds
Tdisk (p,r), Tdisk (q,s) are_homeomorphic
Lm2:
for M being non empty TopSpace holds
( ( M is locally_euclidean & ( for M1 being non empty locally_euclidean TopSpace st M1 = M holds
M1 is without_boundary ) ) iff for p being Point of M ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic )
Lm3:
for n being Nat holds
( Tball ((0. (TOP-REAL n)),1) is n -locally_euclidean & ( for M1 being non empty b1 -locally_euclidean TopSpace st M1 = Tball ((0. (TOP-REAL n)),1) holds
M1 is without_boundary ) )
Lm4:
for M being non empty locally_euclidean TopSpace
for p being Point of (M | (Int M)) ex U being a_neighborhood of p ex n being Nat st (M | (Int M)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
Lm5:
for M being non empty locally_euclidean with_boundary TopSpace
for p being Point of M
for pM being Point of (M | (Fr M)) st p = pM holds
for U being a_neighborhood of p
for n being Nat
for h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) holds
ex n1 being Nat ex U being a_neighborhood of pM st
( n1 + 1 = n & (M | (Fr M)) | U, Tball ((0. (TOP-REAL n1)),1) are_homeomorphic )