### The Mizar article:

### On the Minimal Distance Between Sets in Euclidean Space

**by****Andrzej Trybulec**

- Received August 19, 2002
Copyright (c) 2002 Association of Mizar Users

- MML identifier: JORDAN1K
- [ MML identifier index ]

environ vocabulary JORDAN1K, JGRAPH_2, TARSKI, BOOLE, SUBSET_1, ARYTM, RELAT_2, RELAT_1, ARYTM_1, PRE_TOPC, COMPTS_1, CONNSP_1, EUCLID, TOPREAL2, SQUARE_1, GOBOARD5, JORDAN2C, JORDAN1H, JORDAN11, ABSVALUE, SEQ_2, SEQ_4, TREES_1, JORDAN8, TOPREAL1, ORDINAL2, JORDAN6, JORDAN9, FINSEQ_1, FUNCT_1, PSCOMP_1, MCART_1, ARYTM_3, JORDAN5C, PCOMPS_1, WEIERSTR, LATTICES, METRIC_1, COMPLEX1, SGRAPH1; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1, NAT_1, ABSVALUE, SQUARE_1, FUNCT_1, RELSET_1, BINARITH, PARTFUN1, FUNCT_2, FINSEQ_1, MATRIX_1, SEQ_4, STRUCT_0, GRCAT_1, PRE_TOPC, COMPTS_1, CONNSP_1, METRIC_1, METRIC_6, PSCOMP_1, PCOMPS_1, EUCLID, TOPREAL1, TOPREAL2, WEIERSTR, GOBOARD5, JORDAN2C, JORDAN5C, JORDAN6, JORDAN8, JORDAN9, GOBRD14, JGRAPH_1, JGRAPH_2, JORDAN1H, JORDAN11; constructors JORDAN1, CONNSP_1, JORDAN2C, TOPS_1, JORDAN1H, JORDAN11, REAL_1, REALSET1, PSCOMP_1, JORDAN8, JORDAN6, JORDAN9, JORDAN5C, TOPS_2, T_0TOPSP, WEIERSTR, TBSP_1, TOPRNS_1, SQUARE_1, ABSVALUE, JGRAPH_2, GOBRD14, GRCAT_1, BINARITH, CARD_4, MEMBERED, PARTFUN1; clusters METRIC_1, PCOMPS_1, GOBRD14, TOPS_1, TOPMETR, FINSET_1, EUCLID, JGRAPH_2, TOPREAL6, JORDAN8, RELSET_1, SUBSET_1, PRE_TOPC, JORDAN1A, NAT_1, BORSUK_3, STRUCT_0, BORSUK_4, SPRECT_4, BORSUK_2, JORDAN1C, XREAL_0, MEMBERED, ZFMISC_1, FUNCT_2, PARTFUN1; requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM; definitions XBOOLE_0, TARSKI, FUNCT_2, SEQ_4; theorems XBOOLE_1, JORDAN6, XBOOLE_0, JORDAN5C, TOPS_1, PSCOMP_1, SPRECT_1, JORDAN10, JORDAN2C, SUBSET_1, GOBOARD9, TSEP_1, CONNSP_1, PRE_TOPC, STRUCT_0, ZFMISC_1, EUCLID, METRIC_6, WEIERSTR, TOPREAL3, TBSP_1, JORDAN1C, AXIOMS, SQUARE_1, ABSVALUE, REAL_1, FUNCT_1, METRIC_1, FUNCT_2, REAL_2, JGRAPH_2, JORDAN1A, GOBRD14, GRCAT_1, TOPREAL5, RELAT_1, TOPMETR, PCOMPS_1, TARSKI, JORDAN11, JORDAN1H, XREAL_0, SUB_METR, JORDAN9, TOPREAL1, SPPOL_1, TOPRNS_1, XCMPLX_0, XCMPLX_1; begin :: Preliminaries reserve X for set, Y for non empty set; theorem Th1: for f being Function of X,Y st f is onto for y being Element of Y ex x being set st x in X & y = f.x proof let f be Function of X,Y such that A1: f is onto; let y be Element of Y; rng f = Y by A1,FUNCT_2:def 3; hence ex x being set st x in X & f.x = y by FUNCT_2:17; end; theorem for f being Function of X,Y st f is onto for y being Element of Y ex x being Element of X st y = f.x proof let f be Function of X,Y such that A1: f is onto; let y be Element of Y; ex x being set st x in X & f.x = y by A1,Th1; hence ex x being Element of X st y = f.x; end; theorem Th3: for f being Function of X,Y, A being Subset of X st f is onto holds (f.:A)` c= f.:A` proof let f be Function of X,Y, A be Subset of X such that A1: f is onto; let e be set; assume A2: e in (f.:A)`; then reconsider y = e as Element of Y; consider u being set such that A3: u in X and A4: y = f.u by A1,Th1; reconsider x=u as Element of X by A3; now assume x in A; then y in f.:A by A4,FUNCT_2:43; hence contradiction by A2,SUBSET_1:54; end; then x in A` by A3,SUBSET_1:50; hence e in f.:A` by A4,FUNCT_2:43; end; theorem Th4: for f being Function of X,Y, A being Subset of X st f is one-to-one holds f.:A` c= (f.:A)` proof let f be Function of X,Y, A be Subset of X such that A1: f is one-to-one; let e be set; assume A2: e in f.:A`; then reconsider y = e as Element of Y; consider x1 being set such that A3: x1 in X and A4: x1 in A` and A5: y = f.x1 by A2,FUNCT_2:115; assume not e in (f.:A)`; then y in f.:A by SUBSET_1:50; then consider x2 being set such that x2 in X and A6: x2 in A and A7: y = f.x2 by FUNCT_2:115; not x1 in A by A4,SUBSET_1:54; hence contradiction by A1,A3,A5,A6,A7,FUNCT_2:25; end; theorem Th5: for f being Function of X,Y, A being Subset of X st f is bijective holds (f.:A)` = f.:A` proof let f be Function of X,Y, A being Subset of X; assume A1: f is bijective; then f is onto by FUNCT_2:def 4; then A2: (f.:A)` c= f.:A` by Th3; f is one-to-one by A1,FUNCT_2:def 4; then f.:A` c= (f.:A)` by Th4; hence thesis by A2,XBOOLE_0:def 10; end; begin :: Topological and metrizable spaces theorem Th6: for T being TopSpace for A be Subset of T holds A is_a_component_of {}T iff A is empty proof let T be TopSpace; let A be Subset of T; hereby assume A is_a_component_of {}T; then A c= {}T by SPRECT_1:7; hence A is empty by XBOOLE_1:3; end; assume A1: A is empty; then A c= the carrier of T|{}T by XBOOLE_1:2; then reconsider B = A as Subset of T|{}T; A2: B = {}(T|{}T) by A1; for C being Subset of T|{}T st C is connected holds B c= C implies B = C proof let C be Subset of T|{}T such that C is connected & B c= C; the carrier of T|{}T is empty by STRUCT_0:def 1; hence B = C by A1,XBOOLE_1:3; end; then B is_a_component_of T|{}T by A2,CONNSP_1:def 5; hence A is_a_component_of {}T by CONNSP_1:def 6; end; theorem Th7: for T being non empty TopSpace for A,B,C being Subset of T st A c= B & A is_a_component_of C & B is_a_component_of C holds A = B proof let T be non empty TopSpace; let A,B,C be Subset of T such that A1: A c= B and A2: A is_a_component_of C and A3: B is_a_component_of C; per cases; suppose C = {}; then C = {}T; then A = {} & B = {} by A2,A3,Th6; hence thesis; suppose C is non empty; then A <> {} by A2,SPRECT_1:6; then A meets B by A1,XBOOLE_1:69; hence A = B by A2,A3,GOBOARD9:3; end; reserve n for Nat; theorem Th8: n >= 1 implies for P being Subset of Euclid n holds P is bounded implies P` is not bounded proof assume A1: n>=1; let P be Subset of Euclid n; A2: the carrier of Euclid n = the carrier of TOP-REAL n by TOPREAL3:13 .= REAL n by EUCLID:25; then REAL n c= the carrier of Euclid n; then reconsider W = REAL n as Subset of Euclid n; assume A3: P is bounded & P` is bounded; P \/ P` = [#]Euclid n by PRE_TOPC:18 .= W by A2,PRE_TOPC:12; then W is bounded by A3,TBSP_1:20; hence contradiction by A1,JORDAN2C:39; end; reserve r for Real, M for non empty MetrSpace; theorem Th9: for C being non empty Subset of TopSpaceMetr M, p being Point of TopSpaceMetr M holds (dist_min C).p >= 0 proof let C be non empty Subset of TopSpaceMetr M, p be Point of TopSpaceMetr M; A1: TopSpaceMetr M = TopStruct (#the carrier of M,Family_open_set M#) by PCOMPS_1:def 6; then reconsider x = p as Point of M; set B = [#]((dist x).:C); A2: B = (dist x).:C by WEIERSTR:def 3; A3: for r being real number st r in B holds 0 <= r proof let r be real number; assume r in B; then consider y being set such that y in dom dist x and A4: y in C and A5: r = (dist x).y by A2,FUNCT_1:def 12; reconsider y' = y as Point of M by A1,A4; r = dist(x,y') by A5,WEIERSTR:def 6; hence 0 <= r by METRIC_1:5; end; dom dist x = the carrier of TopSpaceMetr M by FUNCT_2:def 1; then B is non empty by A2,RELAT_1:152; then lower_bound B >= 0 by A3,PSCOMP_1:8; then lower_bound((dist x).:C) >= 0 by WEIERSTR:def 5; hence (dist_min C).p >= 0 by WEIERSTR:def 8; end; theorem Th10: for C being non empty Subset of TopSpaceMetr M, p being Point of M st for q being Point of M st q in C holds dist(p,q) >= r holds (dist_min C).p >= r proof let C be non empty Subset of TopSpaceMetr M, p be Point of M such that A1: for q being Point of M st q in C holds dist(p,q) >= r; A2: TopSpaceMetr M = TopStruct (#the carrier of M,Family_open_set M#) by PCOMPS_1:def 6; set B = [#]((dist p).:C); A3: B = (dist p).:C by WEIERSTR:def 3; A4: for s being real number st s in B holds r <= s proof let s be real number; assume s in B; then consider y being set such that y in dom dist p and A5: y in C and A6: s = (dist p).y by A3,FUNCT_1:def 12; reconsider y' = y as Point of M by A2,A5; s = dist(p,y') by A6,WEIERSTR:def 6; hence r <= s by A1,A5; end; dom dist p = the carrier of TopSpaceMetr M by FUNCT_2:def 1; then B is non empty by A3,RELAT_1:152; then lower_bound B >= r by A4,PSCOMP_1:8; then lower_bound((dist p).:C) >= r by WEIERSTR:def 5; hence (dist_min C).p >= r by WEIERSTR:def 8; end; theorem Th11: for A,B being non empty Subset of TopSpaceMetr M holds min_dist_min(A,B) >= 0 proof let A,B be non empty Subset of TopSpaceMetr M; set X = [#]((dist_min A).:B); A1: X = (dist_min A).:B by WEIERSTR:def 3; A2: for r being real number st r in X holds 0 <= r proof let r be real number; assume r in X; then consider y being set such that y in dom dist_min A and A3: y in B and A4: r = (dist_min A).y by A1,FUNCT_1:def 12; reconsider y as Point of TopSpaceMetr M by A3; (dist_min A).y >= 0 by Th9; hence 0 <= r by A4; end; dom dist_min A = the carrier of TopSpaceMetr M by FUNCT_2:def 1; then X is non empty by A1,RELAT_1:152; then lower_bound X >= 0 by A2,PSCOMP_1:8; then lower_bound((dist_min A).:B) >= 0 by WEIERSTR:def 5; hence min_dist_min(A,B) >= 0 by WEIERSTR:def 9; end; theorem Th12: for A,B being compact Subset of TopSpaceMetr M st A meets B holds min_dist_min(A,B) = 0 proof let A,B be compact Subset of TopSpaceMetr M; assume A meets B; then consider p being set such that A1: p in A and A2: p in B by XBOOLE_0:3; TopSpaceMetr M = TopStruct (#the carrier of M,Family_open_set M#) by PCOMPS_1:def 6; then reconsider p as Point of M by A1; A3: min_dist_min(A,B) >= 0 by A1,A2,Th11; min_dist_min(A,B) <= dist(p,p) by A1,A2,WEIERSTR:40; hence min_dist_min(A,B) = 0 by A3,METRIC_1:1; end; theorem Th13: for A,B being non empty Subset of TopSpaceMetr M st for p,q being Point of M st p in A & q in B holds dist(p,q) >= r holds min_dist_min(A,B) >= r proof let A,B be non empty Subset of TopSpaceMetr M such that A1: for p,q being Point of M st p in A & q in B holds dist(p,q) >= r; set X = [#]((dist_min A).:B); A2: X = (dist_min A).:B by WEIERSTR:def 3; A3: for s being real number st s in X holds r <= s proof let s be real number; assume s in X; then consider y being set such that y in dom dist_min A and A4: y in B and A5: s = (dist_min A).y by A2,FUNCT_1:def 12; reconsider y as Point of TopSpaceMetr M by A4; reconsider p = y as Point of M by TOPMETR:16; for q being Point of M st q in A holds dist(p,q) >= r by A1,A4; hence r <= s by A5,Th10; end; dom dist_min A = the carrier of TopSpaceMetr M by FUNCT_2:def 1; then X is non empty by A2,RELAT_1:152; then lower_bound X >= r by A3,PSCOMP_1:8; then lower_bound((dist_min A).:B) >= r by WEIERSTR:def 5; hence min_dist_min(A,B) >= r by WEIERSTR:def 9; end; begin :: Euclid topological spaces theorem Th14: for P,Q being Subset of TOP-REAL n st P is_a_component_of Q` holds P is_inside_component_of Q or P is_outside_component_of Q proof let P,Q be Subset of TOP-REAL n; P is Bounded or P is not Bounded; hence thesis by JORDAN2C:def 3,def 4; end; theorem n>= 1 implies BDD {}TOP-REAL n = {}TOP-REAL n proof assume n>= 1; then A1: [#](TOP-REAL n) is not Bounded by JORDAN2C:41; set X = {B where B is Subset of TOP-REAL n: B is_inside_component_of {}(TOP-REAL n)}; now assume X <> {}; then consider x being set such that A2: x in X by XBOOLE_0:def 1; consider B being Subset of TOP-REAL n such that x = B and A3: B is_inside_component_of {}(TOP-REAL n) by A2; A4: B is_a_component_of ({}(TOP-REAL n))` by A3,JORDAN2C:def 3; A5: [#]TOP-REAL n = ({}TOP-REAL n)` by PRE_TOPC:27; A6: [#](TOP-REAL n) is_a_component_of TOP-REAL n by JORDAN2C:23; (TOP-REAL n)| [#]TOP-REAL n = TOP-REAL n by TSEP_1:3; then A7: [#]TOP-REAL n is_a_component_of [#]TOP-REAL n by A6,CONNSP_1:def 6 ; B c= [#]TOP-REAL n by PRE_TOPC:14; then B = [#]TOP-REAL n by A4,A5,A7,Th7; hence contradiction by A1,A3,JORDAN2C:def 3; end; hence BDD {}TOP-REAL n = {}TOP-REAL n by JORDAN2C:def 5,ZFMISC_1:2; end; theorem BDD [#]TOP-REAL n = {}TOP-REAL n proof BDD [#]TOP-REAL n c= ([#]TOP-REAL n)` by JORDAN2C:29; then BDD [#]TOP-REAL n c= ([#]TOP-REAL n)`; then BDD [#]TOP-REAL n c= {}TOP-REAL n by TOPS_1:8; hence BDD [#]TOP-REAL n = {}TOP-REAL n by XBOOLE_1:3; end; theorem n>= 1 implies UBD {}TOP-REAL n = [#]TOP-REAL n proof assume n>= 1; then A1: [#](TOP-REAL n) is not Bounded by JORDAN2C:41; UBD {}TOP-REAL n c= the carrier of TOP-REAL n; hence UBD {}TOP-REAL n c= [#]TOP-REAL n by PRE_TOPC:def 3; A2: [#](TOP-REAL n) is_a_component_of TOP-REAL n by JORDAN2C:23; (TOP-REAL n)| [#]TOP-REAL n = TOP-REAL n by TSEP_1:3; then A3: [#]TOP-REAL n is_a_component_of [#]TOP-REAL n by A2,CONNSP_1:def 6 ; set X = {B where B is Subset of TOP-REAL n: B is_outside_component_of {}TOP-REAL n}; [#]TOP-REAL n = ({}TOP-REAL n)` by PRE_TOPC:27; then [#]TOP-REAL n is_outside_component_of {}TOP-REAL n by A1,A3,JORDAN2C:def 4; then [#]TOP-REAL n in X; then [#]TOP-REAL n c= union X by ZFMISC_1:92; hence [#]TOP-REAL n c= UBD {}TOP-REAL n by JORDAN2C:def 6; end; theorem UBD [#]TOP-REAL n = {}TOP-REAL n proof UBD [#]TOP-REAL n c= ([#]TOP-REAL n)` by JORDAN2C:30; then UBD [#]TOP-REAL n c= ([#]TOP-REAL n)`; then UBD [#]TOP-REAL n c= {}TOP-REAL n by TOPS_1:8; hence UBD [#]TOP-REAL n = {}TOP-REAL n by XBOOLE_1:3; end; theorem Th19: for P being connected Subset of TOP-REAL n, Q being Subset of TOP-REAL n st P misses Q holds P c= UBD Q or P c= BDD Q proof let P be connected Subset of TOP-REAL n, Q being Subset of TOP-REAL n such that A1: P misses Q; per cases; suppose P is empty; hence thesis by XBOOLE_1:2; suppose A2: Q = [#]TOP-REAL n; P c= the carrier of TOP-REAL n; then P c= Q by A2,PRE_TOPC:12; then P = {} by A1,XBOOLE_1:67; hence thesis by XBOOLE_1:2; suppose that A3: P is not empty and A4: Q <> [#]TOP-REAL n; Q`` <> [#]TOP-REAL n by A4; then Q` <> {}TOP-REAL n by PRE_TOPC:27; then A5: Q` is non empty; P c= Q` by A1,SUBSET_1:43; then consider C being Subset of TOP-REAL n such that A6: C is_a_component_of Q` and A7: P c= C by A3,A5,GOBOARD9:5; C is_inside_component_of Q or C is_outside_component_of Q by A6,Th14; then C c= UBD Q or C c= BDD Q by JORDAN2C:26,27; hence P c= UBD Q or P c= BDD Q by A7,XBOOLE_1:1; end; begin :: Euclid plane reserve C,D for Simple_closed_curve, n for Nat, p,q,q1,q2 for Point of TOP-REAL 2, r,s1,s2,t1,t2 for Real, x,y for Point of Euclid 2; theorem Th20: dist(|[0,0]|,r*q) = abs(r)*dist(|[0,0]|,q) proof A1: r^2 >= 0 by SQUARE_1:72; A2: q`1^2 >=0 by SQUARE_1:72; q`2^2 >=0 by SQUARE_1:72; then A3: q`1^2 + q`2^2 >=0 by A2,JORDAN2C:5; A4: |[0,0]|`1 = 0 & |[0,0]|`2 = 0 by EUCLID:56; then A5: dist(|[0,0]|,q) = sqrt((0-q`1)^2 + (0-q`2)^2) by GOBRD14:9 .= sqrt((-q`1)^2 + (0-q`2)^2) by XCMPLX_1:150 .= sqrt((-q`1)^2 + (-q`2)^2) by XCMPLX_1:150 .= sqrt((q`1)^2 + (-q`2)^2) by SQUARE_1:61 .= sqrt(q`1^2 + q`2^2) by SQUARE_1:61; thus dist(|[0,0]|,r*q) = sqrt((0-(r*q)`1)^2 + (0-(r*q)`2)^2) by A4,GOBRD14:9 .= sqrt((-(r*q)`1)^2 + (0-(r*q)`2)^2) by XCMPLX_1:150 .= sqrt((-(r*q)`1)^2 + (-(r*q)`2)^2) by XCMPLX_1:150 .= sqrt(((r*q)`1)^2 + (-(r*q)`2)^2) by SQUARE_1:61 .= sqrt(((r*q)`1)^2 + ((r*q)`2)^2) by SQUARE_1:61 .= sqrt((r*q`1)^2 + ((r*q)`2)^2) by TOPREAL3:9 .= sqrt((r*q`1)^2 + (r*q`2)^2) by TOPREAL3:9 .= sqrt(r^2*q`1^2 + (r*q`2)^2) by SQUARE_1:68 .= sqrt(r^2*q`1^2 + r^2*q`2^2) by SQUARE_1:68 .= sqrt(r^2*(q`1^2 + q`2^2)) by XCMPLX_1:8 .= sqrt(r^2)*sqrt(q`1^2 + q`2^2) by A1,A3,SQUARE_1:97 .= abs(r)*dist(|[0,0]|,q) by A5,SQUARE_1:91; end; theorem Th21: dist(q1+q,q2+q) = dist(q1,q2) proof A1: (q1+q)`1-(q2+q)`1 = q1`1+q`1-(q2+q)`1 by TOPREAL3:7 .= q1`1+q`1-(q2`1+q`1) by TOPREAL3:7 .= q1`1+q`1-q2`1-q`1 by XCMPLX_1:36 .= q1`1-q2`1+q`1-q`1 by XCMPLX_1:29 .= q1`1-q2`1+(q`1-q`1) by XCMPLX_1:29 .= q1`1-q2`1+0 by XCMPLX_1:14; A2: (q1+q)`2-(q2+q)`2 = q1`2+q`2-(q2+q)`2 by TOPREAL3:7 .= q1`2+q`2-(q2`2+q`2) by TOPREAL3:7 .= q1`2+q`2-q2`2-q`2 by XCMPLX_1:36 .= q1`2-q2`2+q`2-q`2 by XCMPLX_1:29 .= q1`2-q2`2+(q`2-q`2) by XCMPLX_1:29 .= q1`2-q2`2+0 by XCMPLX_1:14; thus dist(q1+q,q2+q) = sqrt (((q1+q)`1-(q2+q)`1)^2 + ((q1+q)`2-(q2+q)`2)^2) by GOBRD14:9 .= dist(q1,q2) by A1,A2,GOBRD14:9; end; theorem Th22: p <> q implies dist(p,q) > 0 proof ex p', q' being Point of Euclid 2 st p' = p & q' = q & dist(p,q) = dist(p',q') by GOBRD14:def 1; hence thesis by SUB_METR:2; end; theorem Th23: dist(q1-q,q2-q) = dist(q1,q2) proof q1-q = q1+-q & q2-q = q2+-q by EUCLID:45; hence dist(q1-q,q2-q) = dist(q1,q2) by Th21; end; theorem Th24: dist(p,q) = dist(-p,-q) proof thus dist(p,q) = dist(q-q,p-q) by Th23 .= dist(q-q,p+-q) by EUCLID:45 .= dist(|[0,0]|,p+-q) by EUCLID:46,58 .= dist(p-p,p+-q) by EUCLID:46,58 .= dist(p+-p,p+-q) by EUCLID:45 .= dist(-p,-q) by Th21; end; theorem Th25: dist(q-q1,q-q2) = dist(q1,q2) proof -(q-q1)= q1-q & -(q-q2) = q2-q by EUCLID:48; hence dist(q-q1,q-q2) = dist(q1-q,q2-q) by Th24 .= dist(q1,q2) by Th23; end; theorem Th26: dist(r*p,r*q) = abs(r)*dist(p,q) proof thus dist(r*p,r*q) = dist(r*p-r*p,r*p-r*q) by Th25 .= dist(|[0,0]|,r*p-r*q) by EUCLID:46,58 .= dist(|[0,0]|,r*(p-q)) by EUCLID:53 .= abs(r)*dist(|[0,0]|,p-q) by Th20 .= abs(r)*dist(p-p,p-q) by EUCLID:46,58 .= abs(r)*dist(p,q) by Th25; end; theorem Th27: r <= 1 implies dist(p,r*p+(1-r)*q) = (1-r)*dist(p,q) proof assume r <= 1; then 1+ r <= 1 + 1 by AXIOMS:24; then 1-r >= 1-1 by REAL_2:167; then A1: abs(1-r) = 1-r by ABSVALUE:def 1; thus dist(p,r*p+(1-r)*q) = dist(1 *p,r*p+(1-r)*q) by EUCLID:33 .= dist((r+(1-r))*p,r*p+(1-r)*q) by XCMPLX_1:27 .= dist(r*p+(1-r)*p,r*p+(1-r)*q) by EUCLID:37 .= dist((1-r)*p,(1-r)*q) by Th21 .= (1-r)*dist(p,q) by A1,Th26; end; theorem Th28: 0 <= r implies dist(q,r*p+(1-r)*q) = r*dist(p,q) proof assume 0 <= r; then A1: abs r = r by ABSVALUE:def 1; thus dist(q,r*p+(1-r)*q) = dist(1 *q,r*p+(1-r)*q) by EUCLID:33 .= dist(r*p+(1-r)*q,(r+(1-r))*q) by XCMPLX_1:27 .= dist(r*q+(1-r)*q,r*p+(1-r)*q) by EUCLID:37 .= dist(r*q,r*p) by Th21 .= r*dist(p,q) by A1,Th26; end; theorem Th29: p in LSeg(q1,q2) implies dist(q1,p) + dist(p,q2) = dist(q1,q2) proof assume p in LSeg(q1,q2); then consider r such that A1: 0<=r and A2: r<=1 and A3: p = (1-r)*q1+r*q2 by SPPOL_1:21; A4: dist(q1,p) = r*dist(q1,q2) by A1,A3,Th28; dist(q2,p) = (1-r)*dist(q1,q2) by A2,A3,Th27; hence dist(q1,p) + dist(p,q2) = (r+ (1-r))*dist(q1,q2) by A4,XCMPLX_1:8 .= 1 *dist(q1,q2) by XCMPLX_1:27 .= dist(q1,q2); end; theorem Th30: q1 in LSeg(q2,p) & q1 <> q2 implies dist(q1,p) < dist(q2,p) proof assume that A1: q1 in LSeg(q2,p) and A2: q1 <> q2; A3: dist(q2,q1) + dist(q1,p) = dist(q2,p) by A1,Th29; dist(q2,q1) > 0 by A2,Th22; hence dist(q1,p) < dist(q2,p) by A3,REAL_1:69; end; theorem Th31: y = |[0,0]| implies Ball(y,r) = {q : |.q.| < r } proof assume A1: y = |[0,0]|; set X = { q : |.|[0,0]|-q.| < r }, Y = {q : |.q.| < r }; A2: X c= Y proof let u be set; assume u in X; then consider q such that A3: u = q & |.|[0,0]|-q.| < r; |.|[0,0]|-q.| = |.q-|[0,0]|.| by TOPRNS_1:28 .= |.q.| by EUCLID:58,JORDAN2C:13; hence u in Y by A3; end; A4: Y c= X proof let u be set; assume u in Y; then consider q such that A5: u = q & |.q.| < r; |.|[0,0]|-q.| = |.q-|[0,0]|.| by TOPRNS_1:28 .= |.q.| by EUCLID:58,JORDAN2C:13; hence u in X by A5; end; thus Ball(y,r) = { q : |.|[0,0]|-q.| < r } by A1,JGRAPH_2:10 .= {q : |.q.| < r } by A2,A4,XBOOLE_0:def 10; end; begin :: Affine maps theorem Th32: AffineMap(r,s1,r,s2).p = r*p+|[s1,s2]| proof thus AffineMap(r,s1,r,s2).p = |[r*(p`1)+s1,r*(p`2)+s2]| by JGRAPH_2:def 2 .= |[(r*p)`1+s1,r*(p`2)+s2]| by TOPREAL3:9 .= |[(r*p)`1+s1,(r*p)`2+s2]| by TOPREAL3:9 .= |[(r*p)`1,(r*p)`2]|+ |[s1,s2]| by EUCLID:60 .= r*p + |[s1,s2]| by EUCLID:57; end; theorem Th33: AffineMap(r,q`1,r,q`2).p = r*p+q proof thus AffineMap(r,q`1,r,q`2).p = r*p+|[q`1,q`2]| by Th32 .= r*p+q by EUCLID:57; end; theorem Th34: s1 > 0 & s2 > 0 implies AffineMap(s1,t1,s2,t2)*AffineMap(1/s1,-t1/s1,1/s2,-t2/s2) = id REAL 2 proof assume that A1: s1 > 0 and A2: s2 > 0; the carrier of TOP-REAL 2 = REAL 2 by EUCLID:25; then reconsider f = id REAL 2 as Function of the carrier of TOP-REAL 2, the carrier of TOP-REAL 2; now let p be Point of TOP-REAL 2; p in the carrier of TOP-REAL 2; then A3: p in REAL 2 by EUCLID:25; set q = |[1/s1*(p`1)-t1/s1,1/s2*(p`2)-t2/s2]|; A4: q`2 = 1/s2*(p`2)-t2/s2 by EUCLID:56; A5: s1*(1/s1) = 1 by A1,XCMPLX_1:107; thus (AffineMap(s1,t1,s2,t2)*AffineMap(1/s1,-t1/s1,1/s2,-t2/s2)).p = AffineMap(s1,t1,s2,t2).(AffineMap(1/s1,-t1/s1,1/s2,-t2/s2).p) by FUNCT_2:70 .= AffineMap(s1,t1,s2,t2). |[1/s1*(p`1)+-t1/s1,1/s2*(p`2)+-t2/s2]| by JGRAPH_2:def 2 .= AffineMap(s1,t1,s2,t2). |[1/s1*(p`1)-t1/s1,1/s2*(p`2)+-t2/s2]| by XCMPLX_0:def 8 .= AffineMap(s1,t1,s2,t2).q by XCMPLX_0:def 8 .= |[s1*(q`1)+t1,s2*(q`2)+t2]| by JGRAPH_2:def 2 .= |[s1*(1/s1*(p`1)-t1/s1)+t1,s2*(q`2)+t2]| by EUCLID:56 .= |[s1*(1/s1*(p`1))-s1*(t1/s1)+t1,s2*(q`2)+t2]| by XCMPLX_1:40 .= |[s1*(1/s1*(p`1))-t1+t1,s2*(q`2)+t2]| by A1,XCMPLX_1:88 .= |[ 1 *(p`1)-1 *t1+t1,s2*(q`2)+t2]| by A5,XCMPLX_1:4 .= |[p`1,s2*(q`2)+t2]| by XCMPLX_1:27 .= |[p`1,s2*(1/s2*(p`2))-s2*(t2/s2)+t2]| by A4,XCMPLX_1:40 .= |[p`1,s2*(1/s2)*(p`2)-s2*(t2/s2)+t2]| by XCMPLX_1:4 .= |[p`1,s2*(1/s2)*(p`2)-t2+t2]| by A2,XCMPLX_1:88 .= |[p`1,1 *(p`2)-1 *t2+t2]| by A2,XCMPLX_1:107 .= |[p`1,p`2]| by XCMPLX_1:27 .= p by EUCLID:57 .= f.p by A3,FUNCT_1:35; end; hence AffineMap(s1,t1,s2,t2)*AffineMap(1/s1,-t1/s1,1/s2,-t2/s2) = id REAL 2 by FUNCT_2:113; end; theorem Th35: y = |[0,0]| & x = q & r > 0 implies AffineMap(r,q`1,r,q`2).:Ball(y,1) = Ball(x,r) proof assume that A1: y = |[0,0]| and A2: x = q and A3: r > 0; reconsider A = Ball(y,1), B = Ball(x,r) as Subset of TOP-REAL 2 by TOPREAL3:13; A4: AffineMap(r,q`1,r,q`2).:A c= B proof let u be set; assume A5: u in AffineMap(r,q`1,r,q`2).:A; then reconsider q1 = u as Point of TOP-REAL 2; consider q2 such that A6: q2 in A and A7: q1 = AffineMap(r,q`1,r,q`2).q2 by A5,FUNCT_2:116; A8: q1 = r*q2 + q by A7,Th33; reconsider x1 = q1, x2 = q2 as Element of Euclid 2 by TOPREAL3:13; A9: dist(y,x2) < 1 by A6,METRIC_1:12; consider z1,z2 being Point of Euclid 2 such that A10: z1 = q & z2 = r*q2+q and A11: dist(q,r*q2+q) = dist(z1,z2) by GOBRD14:def 1; consider z3,z4 being Point of Euclid 2 such that A12: z3 = |[0,0]| & z4 = q2 and A13: dist(|[0,0]|,q2) = dist(z3,z4) by GOBRD14:def 1; dist(x,x1) = dist(|[0,0]|+q,r*q2 + q) by A2,A8,A10,A11,EUCLID:31,58 .= dist(|[0,0]|,r*q2) by Th21 .= abs(r)*dist(|[0,0]|,q2) by Th20 .= r*dist(y,x2) by A1,A3,A12,A13,ABSVALUE:def 1; then dist(x,x1) < r by A3,A9,REAL_2:145; hence u in B by METRIC_1:12; end; B c= AffineMap(r,q`1,r,q`2).:A proof let u be set; assume A14: u in B; then reconsider q1 = u as Point of TOP-REAL 2; set q2 = AffineMap(1/r,-q`1/r,1/r,-q`2/r).q1; consider z1,z2 being Point of Euclid 2 such that A15: z1 = q & z2 = r*q2+q and A16: dist(q,r*q2+q) = dist(z1,z2) by GOBRD14:def 1; consider z3,z4 being Point of Euclid 2 such that A17: z3 = |[0,0]| & z4 = q2 and A18: dist(|[0,0]|,q2) = dist(z3,z4) by GOBRD14:def 1; reconsider x1 = q1 as Element of Euclid 2 by TOPREAL3:13; q1 in the carrier of TOP-REAL2; then A19: q1 in REAL 2 by EUCLID:25; z2 = AffineMap(r,q`1,r,q`2).q2 by A15,Th33 .= (AffineMap(r,q`1,r,q`2)*AffineMap(1/r,-q`1/r,1/r,-q`2/r)).q1 by FUNCT_2:21 .= (id REAL 2).q1 by A3,Th34 .= x1 by A19,FUNCT_1:35; then dist(x,x1) = dist(|[0,0]|+q,r*q2 + q) by A2,A15,A16,EUCLID:31,58 .= dist(|[0,0]|,r*q2) by Th21 .= abs(r)*dist(|[0,0]|,q2) by Th20 .= r*dist(y,z4) by A1,A3,A17,A18,ABSVALUE:def 1; then r*dist(y,z4) < 1 *r by A14,METRIC_1:12; then dist(y,z4) < 1 by A3,AXIOMS:25; then A20: q2 in A by A17,METRIC_1:12; AffineMap(r,q`1,r,q`2).q2 = (AffineMap(r,q`1,r,q`2)*AffineMap(1/r,-q`1/r,1/r,-q`2/r)).q1 by FUNCT_2:70 .= (id REAL 2).q1 by A3,Th34 .= (id the carrier of TOP-REAL 2).q1 by EUCLID:25 .= (id TOP-REAL 2).q1 by GRCAT_1:def 11 .= q1 by GRCAT_1:11; hence u in AffineMap(r,q`1,r,q`2).:A by A20,FUNCT_2:43; end; hence thesis by A4,XBOOLE_0:def 10; end; theorem Th36: for A,B,C,D being Real st A>0 & C>0 holds AffineMap(A,B,C,D) is onto proof let A,B,C,D be Real such that A1: A>0 and A2: C>0; thus rng AffineMap(A,B,C,D) c= the carrier of TOP-REAL 2; let e be set; assume e in the carrier of TOP-REAL 2; then reconsider q1 = e as Point of TOP-REAL 2; set q2 = AffineMap(1/A,-B/A,1/C,-D/C).q1; A3: the carrier of TOP-REAL 2 = REAL 2 by EUCLID:25; AffineMap(A,B,C,D).q2 = (AffineMap(A,B,C,D)*AffineMap(1/A,-B/A,1/C,-D/C)).q1 by FUNCT_2:21 .= (id REAL 2).q1 by A1,A2,Th34 .= q1 by A3,FUNCT_1:35; hence e in rng AffineMap(A,B,C,D) by FUNCT_2:6; end; theorem Th37: Ball(x,r)` is connected Subset of TOP-REAL 2 proof set C = Ball(x,r)`; per cases; suppose r <= 0; then Ball(x,r) = {} TOP-REAL 2 by TBSP_1:17; then C = [#] Euclid 2 \ {} by PRE_TOPC:17 .= the carrier of Euclid 2 by PRE_TOPC:12 .= the carrier of TOP-REAL 2 by TOPREAL3:13 .= [#] TOP-REAL 2 by PRE_TOPC:12; hence thesis by JORDAN2C:22; suppose A1: r > 0; A2: the carrier of TOP-REAL 2 = the carrier of Euclid 2 by TOPREAL3:13; then A3: the carrier of Euclid 2 = REAL 2 by EUCLID:25; reconsider y = |[0,0]| as Point of Euclid 2 by TOPREAL3:13; reconsider q = x as Point of TOP-REAL 2 by TOPREAL3:13; reconsider Q = Ball(x,r), J = Ball(y,1) as Subset of TOP-REAL 2 by A2; reconsider P = Q`, K = J` as Subset of TOP-REAL 2; K = Ball(y,1)` by TOPREAL3:13 .= (REAL 2)\ Ball(y,1) by A3,SUBSET_1:def 5 .= (REAL 2)\ {q1 : |.q1.| < 1 } by Th31; then A4: K is connected by JORDAN2C:61; A5: AffineMap(r,q`1,r,q`2) is one-to-one by A1,JGRAPH_2:54; AffineMap(r,q`1,r,q`2) is onto by A1,Th36; then A6: AffineMap(r,q`1,r,q`2) is bijective by A5,FUNCT_2:def 4; Q = AffineMap(r,q`1,r,q`2).:J by A1,Th35; then P = AffineMap(r,q`1,r,q`2).:K by A6,Th5; hence thesis by A2,A4,TOPREAL5:5; end; begin :: Minimal distance between subsets definition let n; let A,B be Subset of TOP-REAL n; func dist_min(A,B) -> Real means :Def1: ex A',B' being Subset of TopSpaceMetr Euclid n st A = A' & B = B' & it = min_dist_min(A',B'); existence proof TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then reconsider A'=A, B'=B as Subset of TopSpaceMetr Euclid n ; take min_dist_min(A',B'), A', B'; thus thesis; end; uniqueness; end; definition let M be non empty MetrSpace; let P,Q be non empty compact Subset of TopSpaceMetr M; redefine func min_dist_min(P,Q); commutativity proof let P,Q be non empty compact Subset of TopSpaceMetr M; consider y1,y2 being Point of M such that A1: y1 in Q and A2: y2 in P and A3: dist(y1,y2) = min_dist_min(Q,P) by WEIERSTR:36; consider x1,x2 being Point of M such that A4: x1 in P and A5: x2 in Q and A6: dist(x1,x2) = min_dist_min(P,Q) by WEIERSTR:36; A7: dist(x1,x2) <= dist(y1,y2) by A1,A2,A6,WEIERSTR:40; dist(y1,y2) <= dist(x1,x2) by A3,A4,A5,WEIERSTR:40; hence thesis by A3,A6,A7,AXIOMS:21; end; func max_dist_max(P,Q); commutativity proof let P,Q be non empty compact Subset of TopSpaceMetr M; consider y1,y2 being Point of M such that A8: y1 in Q and A9: y2 in P and A10: dist(y1,y2) = max_dist_max(Q,P) by WEIERSTR:39; consider x1,x2 being Point of M such that A11: x1 in P and A12: x2 in Q and A13: dist(x1,x2) = max_dist_max(P,Q) by WEIERSTR:39; A14: dist(x1,x2) <= dist(y1,y2) by A10,A11,A12,WEIERSTR:40; dist(y1,y2) <= dist(x1,x2) by A8,A9,A13,WEIERSTR:40; hence thesis by A10,A13,A14,AXIOMS:21; end; end; definition let n; let A,B be non empty compact Subset of TOP-REAL n; redefine func dist_min(A,B); commutativity proof let A,B be non empty compact Subset of TOP-REAL n; consider A',B' being Subset of TopSpaceMetr Euclid n such that A1: A = A' & B = B' and A2: dist_min(A,B) = min_dist_min(A',B') by Def1; TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then reconsider A',B' as non empty compact Subset of TopSpaceMetr Euclid n by A1; dist_min(A,B) = min_dist_min(B',A') by A2; hence thesis by A1,Def1; end; end; theorem Th38: for A,B being non empty Subset of TOP-REAL n holds dist_min(A,B) >= 0 proof let A,B be non empty Subset of TOP-REAL n; ex A',B' be Subset of TopSpaceMetr Euclid n st A = A' & B = B' & dist_min(A,B) = min_dist_min(A',B') by Def1; hence dist_min(A,B) >= 0 by Th11; end; theorem Th39: for A,B being compact Subset of TOP-REAL n st A meets B holds dist_min(A,B) = 0 proof let A,B be compact Subset of TOP-REAL n such that A1: A meets B; A2: TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; ex A',B' be Subset of TopSpaceMetr Euclid n st A = A' & B = B' & dist_min(A,B) = min_dist_min(A',B') by Def1; hence dist_min(A,B) = 0 by A1,A2,Th12; end; theorem Th40: for A,B being non empty Subset of TOP-REAL n st for p,q being Point of TOP-REAL n st p in A & q in B holds dist(p,q) >= r holds dist_min(A,B) >= r proof let A,B be non empty Subset of TOP-REAL n such that A1: for p,q being Point of TOP-REAL n st p in A & q in B holds dist(p,q) >= r; A2: for p,q being Point of Euclid n st p in A & q in B holds dist(p,q) >= r proof let a,b being Point of Euclid n such that A3: a in A & b in B; reconsider p =a, q = b as Point of TOP-REAL n by TOPREAL3:13; ex a, b being Point of Euclid n st p = a & q = b & dist(p,q) = dist(a,b) by GOBRD14:def 1; hence dist(a,b) >= r by A1,A3; end; ex A',B' be Subset of TopSpaceMetr Euclid n st A = A' & B = B' & dist_min(A,B) = min_dist_min(A',B') by Def1; hence dist_min(A,B) >= r by A2,Th13; end; theorem Th41: for D being Subset of TOP-REAL n, A,C being non empty Subset of TOP-REAL n st C c= D holds dist_min(A,D) <= dist_min(A,C) proof let D be Subset of TOP-REAL n; let A,C be non empty Subset of TOP-REAL n such that A1: C c= D; consider A',D' be Subset of TopSpaceMetr Euclid n such that A2: A = A' and A3: D = D' and A4: dist_min(A,D) = min_dist_min(A',D') by Def1; consider A'',C' be Subset of TopSpaceMetr Euclid n such that A5: A = A'' and A6: C = C' and A7: dist_min(A,C) = min_dist_min(A'',C') by Def1; reconsider f = dist_min A' as Function of the carrier of TopSpaceMetr Euclid n, REAL by TOPMETR:24; dom f = the carrier of TopSpaceMetr Euclid n by FUNCT_2:def 1; then reconsider X = f.:C' as non empty Subset of REAL by A6,RELAT_1:152; reconsider Y = f.:D' as Subset of REAL; A8: inf Y = lower_bound([#]((dist_min A').:D')) by WEIERSTR:def 3 .= lower_bound((dist_min A').:D') by WEIERSTR:def 5 .= min_dist_min(A',D') by WEIERSTR:def 9; A9: inf X = lower_bound([#]((dist_min A').:C')) by WEIERSTR:def 3 .= lower_bound((dist_min A').:C') by WEIERSTR:def 5 .= min_dist_min(A',C') by WEIERSTR:def 9; A10: Y is bounded_below proof take 0; let r be real number; assume r in Y; then ex c being Element of TopSpaceMetr Euclid n st c in D' & r = f.c by FUNCT_2:116; hence 0<=r by A2,Th9; end; f.:C c= f.:D by A1,RELAT_1:156; hence dist_min(A,D) <= dist_min(A,C) by A2,A3,A4,A5,A6,A7,A8,A9,A10,PSCOMP_1: 12; end; theorem Th42: for A,B being non empty compact Subset of TOP-REAL n ex p,q being Point of TOP-REAL n st p in A & q in B & dist_min(A,B) = dist(p,q) proof let A,B be non empty compact Subset of TOP-REAL n; consider A',B' being Subset of TopSpaceMetr Euclid n such that A1: A = A' and A2: B = B' and A3: dist_min(A,B) = min_dist_min(A',B') by Def1; TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then consider x1,x2 being Point of Euclid n such that A4: x1 in A' and A5: x2 in B' and A6: dist(x1,x2) = min_dist_min(A',B') by A1,A2,WEIERSTR:36; reconsider p = x1, q = x2 as Point of TOP-REAL n by TOPREAL3:13; take p,q; thus p in A & q in B by A1,A2,A4,A5; thus dist_min(A,B) = dist(p,q) by A3,A6,GOBRD14:def 1; end; theorem Th43: for p,q being Point of TOP-REAL n holds dist_min({p},{q}) = dist(p,q) proof let p,q be Point of TOP-REAL n; consider p',q' being Point of TOP-REAL n such that A1: p' in {p} & q' in {q} and A2: dist_min({p},{q}) = dist(p',q') by Th42; p = p' & q = q' by A1,TARSKI:def 1; hence dist_min({p},{q}) = dist(p,q) by A2; end; definition let n; let p be Point of TOP-REAL n; let B be Subset of TOP-REAL n; func dist(p,B) -> Real equals :Def2: dist_min({p},B); coherence; end; theorem Th44: for A being non empty Subset of TOP-REAL n, p being Point of TOP-REAL n holds dist(p,A) >= 0 proof let A be non empty Subset of TOP-REAL n, p be Point of TOP-REAL n; dist(p,A) = dist_min({p},A) by Def2; hence dist(p,A) >= 0 by Th38; end; theorem Th45: for A being compact Subset of TOP-REAL n, p being Point of TOP-REAL n st p in A holds dist(p,A) = 0 proof let A be compact Subset of TOP-REAL n, p be Point of TOP-REAL n; assume p in A; then A1: {p} meets A by ZFMISC_1:54; dist(p,A) = dist_min({p},A) by Def2; hence dist(p,A) = 0 by A1,Th39; end; theorem Th46: for A being non empty compact Subset of TOP-REAL n, p being Point of TOP-REAL n ex q being Point of TOP-REAL n st q in A & dist(p,A) = dist(p,q) proof let A be non empty compact Subset of TOP-REAL n; let p be Point of TOP-REAL n; consider q,p' being Point of TOP-REAL n such that A1: q in A and A2: p' in {p} and A3: dist_min(A,{p}) = dist(q,p') by Th42; take q; thus q in A by A1; thus dist(p,A) = dist_min({p},A) by Def2 .= dist(p,q) by A2,A3,TARSKI:def 1; end; theorem Th47: for C being non empty Subset of TOP-REAL n for D being Subset of TOP-REAL n st C c= D for q being Point of TOP-REAL n holds dist(q,D) <= dist(q,C) proof let C be non empty Subset of TOP-REAL n; let D be Subset of TOP-REAL n such that A1: C c= D; let q be Point of TOP-REAL n; dist(q,D) = dist_min({q},D) & dist(q,C) = dist_min({q},C) by Def2; hence dist(q,D) <= dist(q,C) by A1,Th41; end; theorem Th48: for A being non empty Subset of TOP-REAL n, p being Point of TOP-REAL n st for q being Point of TOP-REAL n st q in A holds dist(p,q) >= r holds dist(p,A) >= r proof let A be non empty Subset of TOP-REAL n, p' be Point of TOP-REAL n such that A1: for q being Point of TOP-REAL n st q in A holds dist(p',q) >= r; A2: dist(p',A) = dist_min({p'},A) by Def2; for p,q being Point of TOP-REAL n st p in {p'} & q in A holds dist(p,q) >= r proof let p,q be Point of TOP-REAL n such that A3: p in {p'} and A4: q in A; p = p' by A3,TARSKI:def 1; hence dist(p,q) >= r by A1,A4; end; hence thesis by A2,Th40; end; theorem Th49: for p,q being Point of TOP-REAL n holds dist(p,{q}) = dist(p,q) proof let p,q be Point of TOP-REAL n; dist(p,{q}) = dist_min({p},{q}) by Def2; hence thesis by Th43; end; theorem Th50: for A being non empty Subset of TOP-REAL n, p,q being Point of TOP-REAL n st q in A holds dist(p,A) <= dist(p,q) proof let A be non empty Subset of TOP-REAL n; let p,q be Point of TOP-REAL n; assume q in A; then {q} c= A by ZFMISC_1:37; then dist(p,A) <= dist(p,{q}) by Th47; hence dist(p,A) <= dist(p,q) by Th49; end; theorem Th51: for A being compact non empty Subset of TOP-REAL 2, B being open Subset of TOP-REAL 2 st A c= B for p being Point of TOP-REAL 2 st not p in B holds dist(p,B) < dist(p,A) proof let A be compact non empty Subset of TOP-REAL 2, B being open Subset of TOP-REAL 2 such that A1: A c= B; let p be Point of TOP-REAL 2 such that A2: not p in B; A3: dist(p,B) <= dist(p,A) by A1,Th47; assume dist(p,B) >= dist(p,A); then A4: dist(p,B) = dist(p,A) by A3,AXIOMS:21; consider q being Point of TOP-REAL 2 such that A5: q in A and A6: dist(p,A) = dist(p,q) by Th46; TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8; then reconsider P = B as open Subset of TopSpaceMetr Euclid 2; reconsider a = q as Point of Euclid 2 by TOPREAL3:13; A7: a in P by A1,A5; consider r being real number such that A8: r>0 and A9: Ball(a,r) c= P by A1,A5,TOPMETR:22; reconsider r as Element of REAL by XREAL_0:def 1; set s = r/(2*dist(p,q)), q' = (1-s)*q + s*p; A10: dist(p,q) > 0 by A2,A7,Th22; then A11: 2*dist(p,q) > 0 by REAL_2:122; then A12: 0 < s by A8,REAL_2:127; then dist(q,q') = 1 *r/(2*dist(p,q))*dist(p,q) by Th28 .= r/2/(dist(p,q)/1)*dist(p,q) by XCMPLX_1:85 .= r/2 by A10,XCMPLX_1:88; then A13: dist(q,q') < r/1 by A8,REAL_2:200; ex p1, q1 being Point of Euclid 2 st p1 = q & q1 = q' & dist(q,q') = dist(p1,q1) by GOBRD14:def 1; then A14: q' in Ball(a,r) by A13,METRIC_1:12; now assume A15: r > dist(p,q); ex p1, q1 being Point of Euclid 2 st p1 = p & q1 = q & dist(p,q) = dist(p1,q1) by GOBRD14:def 1; then p in Ball(a,r) by A15,METRIC_1:12; hence contradiction by A2,A9; end; then 1 *r < 2*dist(p,q) by A8,REAL_2:199; then s < 1 by A11,REAL_2:118; then A16: dist(p,q') = (1-s)*dist(p,q) by Th27; 1-s < 1-0 by A12,REAL_2:105; then dist(p,q') < dist(p,q) by A10,A16,REAL_2:145; hence contradiction by A4,A6,A9,A14,Th50; end; begin :: BDD & UBD theorem Th52: UBD C meets UBD D proof C is Bounded by JORDAN2C:73; then consider A being Subset of Euclid 2 such that A1: C=A and A2: A is bounded by JORDAN2C:def 2; consider r1 being Real, x1 being Point of Euclid 2 such that 0 < r1 and A3: A c= Ball(x1,r1) by A2,METRIC_6:def 10; D is Bounded by JORDAN2C:73; then consider B being Subset of Euclid 2 such that A4: D=B and A5: B is bounded by JORDAN2C:def 2; consider r2 being Real, x2 being Point of Euclid 2 such that 0 < r2 and A6: B c= Ball(x2,r2) by A5,METRIC_6:def 10; consider x3 being Point of Euclid 2, r3 being Real such that A7: Ball(x1,r1) \/ Ball(x2,r2) c= Ball(x3,r3) by WEIERSTR:1; Ball(x3,r3)` c= (Ball(x1,r1) \/ Ball(x2,r2))` by A7,SUBSET_1:31; then A8: Ball(x3,r3)` c= Ball(x1,r1)` /\ Ball(x2,r2)` by SUBSET_1:29; then A9: Ball(x3,r3)` c= Ball(x1,r1)` by XBOOLE_1:18; A10: Ball(x3,r3)` c= Ball(x2,r2)` by A8,XBOOLE_1:18; reconsider C' = Ball(x1,r1)`, D' = Ball(x2,r2)` as connected Subset of TOP-REAL 2 by Th37; Ball(x1,r1) is bounded by TBSP_1:19; then A11: Ball(x1,r1)` is not bounded by Th8; A12: now assume C' is Bounded; then consider X being Subset of Euclid 2 such that A13: X=C' and A14: X is bounded by JORDAN2C:def 2; thus contradiction by A11,A13,A14; end; Ball(x1,r1)` c= A` by A3,SUBSET_1:31; then Ball(x1,r1)` misses A by SUBSET_1:43; then C' c= UBD C by A1,A12,JORDAN1C:13; then A15: Ball(x3,r3)` c= UBD C by A9,XBOOLE_1:1; Ball(x2,r2) is bounded by TBSP_1:19; then A16: Ball(x2,r2)` is not bounded by Th8; A17: now assume D' is Bounded; then consider X being Subset of Euclid 2 such that A18: X=D' and A19: X is bounded by JORDAN2C:def 2; thus contradiction by A16,A18,A19; end; Ball(x2,r2)` c= B` by A6,SUBSET_1:31; then Ball(x2,r2)` misses B by SUBSET_1:43; then D' c= UBD D by A4,A17,JORDAN1C:13; then A20: Ball(x3,r3)` c= UBD D by A10,XBOOLE_1:1; Ball(x3,r3) is bounded by TBSP_1:19; then Ball(x3,r3)` is not bounded by Th8; then Ball(x3,r3)` <> {}Euclid 2 by TBSP_1:14; then Ball(x3,r3)` is non empty; hence thesis by A15,A20,XBOOLE_1:68; end; theorem Th53: q in UBD C & p in BDD C implies dist(q,C) < dist(q,p) proof assume that A1: q in UBD C and A2: p in BDD C and A3: dist(q,C) >= dist(q,p); now assume LSeg(p,q) meets C; then consider x being set such that A4: x in LSeg(p,q) and A5: x in C by XBOOLE_0:3; reconsider x as Point of TOP-REAL 2 by A4; A6: dist(q,C) <= dist(q,x) by A5,Th50; C misses BDD C by JORDAN1A:15; then x <> p by A2,A5,XBOOLE_0:3; then dist(q,x) < dist(q,p) by A4,Th30; hence contradiction by A3,A6,AXIOMS:22; end; then A7: LSeg(p,q) c= C` by PRE_TOPC:21; A8: UBD C is_a_component_of C` by JORDAN1C:12; q in LSeg(p,q) by TOPREAL1:6; then A9: LSeg(p,q) meets UBD C by A1,XBOOLE_0:3; A10: BDD C = union{B where B is Subset of TOP-REAL 2: B is_inside_component_of C} by JORDAN2C:def 5; then consider X being set such that A11: p in X and A12: X in {B where B is Subset of TOP-REAL 2: B is_inside_component_of C} by A2,TARSKI:def 4; consider B being Subset of TOP-REAL 2 such that A13: X = B and A14: B is_inside_component_of C by A12; A15: B is_a_component_of C` by A14,JORDAN2C:def 3; p in LSeg(p,q) by TOPREAL1:6; then LSeg(p,q) meets B by A11,A13,XBOOLE_0:3; then A16: UBD C = B by A7,A8,A9,A15,JORDAN9:3; A17: B c= BDD C by A10,A12,A13,ZFMISC_1:92; BDD C misses UBD C by JORDAN2C:28; then B misses UBD C by A17,XBOOLE_1:63; hence contradiction by A16,XBOOLE_1:66; end; definition let C; cluster BDD C -> non empty; coherence proof set n = ApproxIndex C, i = X-SpanStart(C,n)-'1, j = Y-SpanStart(C,n), B = cell(Gauge(C,n),i,j); A1: n is_sufficiently_large_for C by JORDAN11:def 1; then A2: B c= BDD C by JORDAN11:6; i<=len Gauge(C,n) & j<=width Gauge(C,n) by A1,JORDAN11:def 3,JORDAN1H:59; then B <> {} by JORDAN1A:45; hence thesis by A2,XBOOLE_1:3; end; end; theorem Th54: not p in BDD C implies dist(p,C) <= dist(p,BDD C) proof per cases; suppose p in C; then dist(p,C) = 0 by Th45; hence thesis by Th44; suppose not p in C; then p in C` by SUBSET_1:50; then A1: p in (BDD C) \/ (UBD C) by JORDAN2C:31; assume that A2: not p in BDD C and A3: dist(p,C) > dist(p,BDD C); A4: p in UBD C by A1,A2,XBOOLE_0:def 2; ex q st q in BDD C & dist(p,q) < dist(p,C) by A3,Th48; hence contradiction by A4,Th53; end; theorem Th55: not(C c= BDD D & D c= BDD C) proof assume that A1: C c= BDD D and A2: D c= BDD C; UBD C meets UBD D by Th52; then consider e being set such that A3: e in UBD C and A4: e in UBD D by XBOOLE_0:3; reconsider p = e as Point of TOP-REAL 2 by A3; UBD C misses BDD C by JORDAN2C:28; then A5: not p in BDD C by A3,XBOOLE_0:3; then A6: dist(p,BDD C) < dist(p,D) by A2,Th51; UBD D misses BDD D by JORDAN2C:28; then A7: not p in BDD D by A4,XBOOLE_0:3; then A8: dist(p,BDD D) < dist(p,C) by A1,Th51; dist(p,C) <= dist(p, BDD C) by A5,Th54; then dist(p, BDD D) < dist(p, BDD C) by A8,AXIOMS:22; then dist(p, BDD D) < dist(p,D) by A6,AXIOMS:22; hence contradiction by A7,Th54; end; theorem Th56: C c= BDD D implies D c= UBD C proof assume A1: C c= BDD D; D misses BDD D by JORDAN1A:15; then A2: C misses D by A1,XBOOLE_1:63; assume not D c= UBD C; then D c= BDD C by A2,Th19; hence contradiction by A1,Th55; end; begin :: Main definitions theorem L~Cage(C,n) c= UBD C proof C c= BDD L~Cage(C,n) by JORDAN10:12; hence thesis by Th56; end; definition let C; func Lower_Middle_Point C -> Point of TOP-REAL 2 equals :Def3: First_Point(Lower_Arc C,W-min C,E-max C, Vertical_Line((W-bound C+E-bound C)/2)); coherence; func Upper_Middle_Point C -> Point of TOP-REAL 2 equals :Def4: First_Point(Upper_Arc C,W-min C,E-max C, Vertical_Line((W-bound C+E-bound C)/2)); coherence; end; theorem Th58: Lower_Arc C meets Vertical_Line((W-bound C+E-bound C)/2) proof A1: W-bound C <= E-bound C by SPRECT_1:23; (W-min C)`1 = W-bound C by PSCOMP_1:84; then A2: (W-min C)`1<=(W-bound C +E-bound C)/2 by A1,JORDAN6:2; (E-max C)`1 = E-bound C by PSCOMP_1:104; then A3: (W-bound C +E-bound C)/2<=(E-max C)`1 by A1,JORDAN6:2; Lower_Arc C is_an_arc_of W-min C,E-max C by JORDAN6:65; hence Lower_Arc C meets Vertical_Line((W-bound C +E-bound C)/2) by A2,A3,JORDAN6:64; end; theorem Th59: Upper_Arc C meets Vertical_Line((W-bound C+E-bound C)/2) proof A1: W-bound C <= E-bound C by SPRECT_1:23; (W-min C)`1 = W-bound C by PSCOMP_1:84; then A2: (W-min C)`1<=(W-bound C +E-bound C)/2 by A1,JORDAN6:2; (E-max C)`1 = E-bound C by PSCOMP_1:104; then A3: (W-bound C +E-bound C)/2<=(E-max C)`1 by A1,JORDAN6:2; Upper_Arc C is_an_arc_of W-min C,E-max C by JORDAN6:65; hence Upper_Arc C meets Vertical_Line((W-bound C +E-bound C)/2) by A2,A3,JORDAN6:64; end; theorem (Lower_Middle_Point C)`1 = (W-bound C+E-bound C)/2 proof set L = Vertical_Line((W-bound C+E-bound C)/2), p = First_Point(Lower_Arc C,W-min C,E-max C,L); A1: Lower_Arc C meets L by Th58; L is closed by JORDAN6:33; then A2: Lower_Arc C /\ L is closed by TOPS_1:35; Lower_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:65; then p in Lower_Arc C /\ L by A1,A2,JORDAN5C:def 1; then p in L by XBOOLE_0:def 3; then p`1 = (W-bound C+E-bound C)/2 by JORDAN6:34; hence thesis by Def3; end; theorem (Upper_Middle_Point C)`1 = (W-bound C+E-bound C)/2 proof set L = Vertical_Line((W-bound C+E-bound C)/2), p = First_Point(Upper_Arc C,W-min C,E-max C,L); A1: Upper_Arc C meets L by Th59; L is closed by JORDAN6:33; then A2: Upper_Arc C /\ L is closed by TOPS_1:35; Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:65; then p in Upper_Arc C /\ L by A1,A2,JORDAN5C:def 1; then p in L by XBOOLE_0:def 3; then p`1 = (W-bound C+E-bound C)/2 by JORDAN6:34; hence thesis by Def4; end; theorem Lower_Middle_Point C in Lower_Arc C proof set L = Vertical_Line((W-bound C+E-bound C)/2), p = First_Point(Lower_Arc C,W-min C,E-max C,L); A1: Lower_Middle_Point C = p by Def3; A2: Lower_Arc C meets L by Th58; L is closed by JORDAN6:33; then A3: Lower_Arc C /\ L is closed by TOPS_1:35; Lower_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:65; then p in L /\ Lower_Arc C by A2,A3,JORDAN5C:def 1; hence Lower_Middle_Point C in Lower_Arc C by A1,XBOOLE_0:def 3; end; theorem Upper_Middle_Point C in Upper_Arc C proof set L = Vertical_Line((W-bound C+E-bound C)/2), p = First_Point(Upper_Arc C,W-min C,E-max C,L); A1: Upper_Middle_Point C = p by Def4; A2: Upper_Arc C meets L by Th59; L is closed by JORDAN6:33; then A3: Upper_Arc C /\ L is closed by TOPS_1:35; A4: Upper_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:65; then p = Last_Point(Upper_Arc C,E-max C,W-min C,L) by A2,A3,JORDAN5C:18; then p in L /\ Upper_Arc C by A2,A3,A4,JORDAN5C:def 2; hence Upper_Middle_Point C in Upper_Arc C by A1,XBOOLE_0:def 3; end;

Back to top