environ
vocabularies HIDDEN, NUMBERS, REAL_1, SUBSET_1, XBOOLE_0, METRIC_1, PRE_TOPC, EUCLID, CARD_1, XXREAL_0, SQUARE_1, ARYTM_3, RELAT_1, COMPLEX1, ARYTM_1, CARD_3, FINSEQ_2, FINSEQ_1, NAT_1, FUNCT_1, NEWTON, RVSUM_1, TARSKI, XXREAL_1, ORDINAL2, XXREAL_2, FINSET_1, RELAT_2, CONNSP_1, T_0TOPSP, TOPS_2, SETFAM_1, RCOMP_1, ZFMISC_1, STRUCT_0, FUNCOP_1, SUPINF_2, MCART_1, RLTOPSP1, PSCOMP_1, SPPOL_1, TOPREAL4, CONVEX1, TOPREAL1, TOPREAL2, SPRECT_1, PCOMPS_1, SEQ_1, SEQ_2, TOPMETR, PARTFUN1, CONNSP_2, TOPS_1, BORSUK_1, SEQ_4, FUNCT_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, FINSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, SQUARE_1, NAT_1, NAT_D, FUNCOP_1, FUNCT_4, SEQ_1, SEQ_2, SEQ_4, STRUCT_0, METRIC_1, TBSP_1, FINSEQ_1, FINSEQ_2, RVSUM_1, NEWTON, XXREAL_0, XXREAL_2, CARD_3, FINSEQ_4, RCOMP_1, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_1, CONNSP_2, COMPTS_1, BORSUK_1, MEASURE6, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID, WEIERSTR, TOPMETR, TOPREAL1, TOPREAL2, T_0TOPSP, TOPREAL4, PSCOMP_1, SPPOL_1, SPRECT_1;
definitions TARSKI, FUNCT_1, TOPS_2, CONNSP_1, BORSUK_1, SPPOL_1, T_0TOPSP, TOPREAL2, XBOOLE_0, JORDAN1, XXREAL_2;
theorems ABSVALUE, BORSUK_1, BORSUK_3, CARD_3, FUNCT_4, COMPTS_1, CONNSP_1, CONNSP_2, EUCLID, FINSEQ_1, FINSEQ_2, FUNCT_1, FUNCT_2, FUNCT_3, GOBOARD6, GOBOARD7, JGRAPH_1, JORDAN1, JORDAN2C, JORDAN5A, JORDAN6, METRIC_1, METRIC_6, NEWTON, NAT_1, PCOMPS_1, PRE_TOPC, PREPOWER, PSCOMP_1, RCOMP_1, RELAT_1, RVSUM_1, SEQ_4, SPRECT_1, SQUARE_1, SUBSET_1, TARSKI, TBSP_1, TOPMETR, TOPREAL1, TOPREAL3, TOPREAL4, TOPS_1, TOPS_2, WEIERSTR, YELLOW12, ZFMISC_1, XREAL_0, FUNCOP_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, COMPLEX1, XREAL_1, XXREAL_0, XXREAL_1, XXREAL_2, NAT_D, VALUED_1, MEASURE6, RLTOPSP1, ORDINAL1, RLVECT_1;
schemes FINSET_1, NAT_1, BINOP_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_4, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, MEMBERED, FINSEQ_1, RCOMP_1, STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1, METRIC_1, PCOMPS_1, BORSUK_1, TEX_4, MONOID_0, EUCLID, TOPMETR, JORDAN1, PSCOMP_1, GOBOARD9, WAYBEL_2, TOPGRP_1, JORDAN2C, VALUED_0, XXREAL_2, RLTOPSP1, TBSP_1, SPRECT_1, FUNCT_2, JORDAN5A, NEWTON, RVSUM_1, NAT_1;
constructors HIDDEN, SETFAM_1, FUNCT_3, REAL_1, SQUARE_1, NAT_1, CARD_3, FINSEQOP, RCOMP_1, FINSEQ_4, FINSOP_1, NEWTON, NAT_D, TOPS_1, CONNSP_1, TOPS_2, COMPTS_1, TBSP_1, T_0TOPSP, MONOID_0, TOPREAL1, TOPREAL2, TOPREAL4, SPPOL_1, JORDAN1, PSCOMP_1, WEIERSTR, SPRECT_1, JORDAN2C, XXREAL_2, SEQ_4, FUNCSDOM, CONVEX1, BINOP_2, SEQ_2, MEASURE6, PCOMPS_1, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities SUBSET_1, BORSUK_1, BINOP_1, EUCLID, SQUARE_1, STRUCT_0, FINSEQ_2, RLTOPSP1;
expansions TARSKI, FUNCT_1, TOPS_2, CONNSP_1, SPPOL_1, T_0TOPSP, XBOOLE_0, XXREAL_2;
Lm1:
for M being non empty MetrSpace
for z being Point of M
for r being Real
for A being Subset of (TopSpaceMetr M) st A = cl_Ball (z,r) holds
A ` is open
definition
let n be
Nat;
let a,
b be
Point of
(TOP-REAL n);
existence
ex b1 being Real ex p, q being Point of (Euclid n) st
( p = a & q = b & b1 = dist (p,q) )
uniqueness
for b1, b2 being Real st ex p, q being Point of (Euclid n) st
( p = a & q = b & b1 = dist (p,q) ) & ex p, q being Point of (Euclid n) st
( p = a & q = b & b2 = dist (p,q) ) holds
b1 = b2
;
commutativity
for b1 being Real
for a, b being Point of (TOP-REAL n) st ex p, q being Point of (Euclid n) st
( p = a & q = b & b1 = dist (p,q) ) holds
ex p, q being Point of (Euclid n) st
( p = b & q = a & b1 = dist (p,q) )
;
end;