:: JORDAN1K semantic presentation begin theorem Th1: :: JORDAN1K:1 for X being set for Y being non empty set for f being Function of X,Y st f is onto holds for y being Element of Y ex x being set st ( x in X & y = f . x ) proof let X be set ; ::_thesis: for Y being non empty set for f being Function of X,Y st f is onto holds for y being Element of Y ex x being set st ( x in X & y = f . x ) let Y be non empty set ; ::_thesis: for f being Function of X,Y st f is onto holds for y being Element of Y ex x being set st ( x in X & y = f . x ) let f be Function of X,Y; ::_thesis: ( f is onto implies for y being Element of Y ex x being set st ( x in X & y = f . x ) ) assume f is onto ; ::_thesis: for y being Element of Y ex x being set st ( x in X & y = f . x ) then A1: rng f = Y by FUNCT_2:def_3; let y be Element of Y; ::_thesis: ex x being set st ( x in X & y = f . x ) thus ex x being set st ( x in X & y = f . x ) by A1, FUNCT_2:11; ::_thesis: verum end; theorem :: JORDAN1K:2 for X being set for Y being non empty set for f being Function of X,Y st f is onto holds for y being Element of Y ex x being Element of X st y = f . x proof let X be set ; ::_thesis: for Y being non empty set for f being Function of X,Y st f is onto holds for y being Element of Y ex x being Element of X st y = f . x let Y be non empty set ; ::_thesis: for f being Function of X,Y st f is onto holds for y being Element of Y ex x being Element of X st y = f . x let f be Function of X,Y; ::_thesis: ( f is onto implies for y being Element of Y ex x being Element of X st y = f . x ) assume A1: f is onto ; ::_thesis: for y being Element of Y ex x being Element of X st y = f . x let y be Element of Y; ::_thesis: ex x being Element of X st y = f . x 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 ; ::_thesis: verum end; theorem Th3: :: JORDAN1K:3 for X being set for Y being non empty set for f being Function of X,Y for A being Subset of X st f is onto holds (f .: A) ` c= f .: (A `) proof let X be set ; ::_thesis: for Y being non empty set for f being Function of X,Y for A being Subset of X st f is onto holds (f .: A) ` c= f .: (A `) let Y be non empty set ; ::_thesis: for f being Function of X,Y for A being Subset of X st f is onto holds (f .: A) ` c= f .: (A `) let f be Function of X,Y; ::_thesis: for A being Subset of X st f is onto holds (f .: A) ` c= f .: (A `) let A be Subset of X; ::_thesis: ( f is onto implies (f .: A) ` c= f .: (A `) ) assume A1: f is onto ; ::_thesis: (f .: A) ` c= f .: (A `) let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in (f .: A) ` or e in f .: (A `) ) assume A2: e in (f .: A) ` ; ::_thesis: 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__::_thesis:_not_x_in_A assume x in A ; ::_thesis: contradiction then y in f .: A by A4, FUNCT_2:35; hence contradiction by A2, XBOOLE_0:def_5; ::_thesis: verum end; then x in A ` by A3, SUBSET_1:29; hence e in f .: (A `) by A4, FUNCT_2:35; ::_thesis: verum end; theorem Th4: :: JORDAN1K:4 for X being set for Y being non empty set for f being Function of X,Y for A being Subset of X st f is one-to-one holds f .: (A `) c= (f .: A) ` proof let X be set ; ::_thesis: for Y being non empty set for f being Function of X,Y for A being Subset of X st f is one-to-one holds f .: (A `) c= (f .: A) ` let Y be non empty set ; ::_thesis: for f being Function of X,Y for A being Subset of X st f is one-to-one holds f .: (A `) c= (f .: A) ` let f be Function of X,Y; ::_thesis: for A being Subset of X st f is one-to-one holds f .: (A `) c= (f .: A) ` let A be Subset of X; ::_thesis: ( f is one-to-one implies f .: (A `) c= (f .: A) ` ) assume A1: f is one-to-one ; ::_thesis: f .: (A `) c= (f .: A) ` let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in f .: (A `) or e in (f .: A) ` ) assume A2: e in f .: (A `) ; ::_thesis: 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:64; assume not e in (f .: A) ` ; ::_thesis: contradiction then A6: ex x2 being set st ( x2 in X & x2 in A & y = f . x2 ) by FUNCT_2:64, SUBSET_1:29; not x1 in A by A4, XBOOLE_0:def_5; hence contradiction by A1, A3, A5, A6, FUNCT_2:19; ::_thesis: verum end; theorem Th5: :: JORDAN1K:5 for X being set for Y being non empty set for f being Function of X,Y for A being Subset of X st f is bijective holds (f .: A) ` = f .: (A `) proof let X be set ; ::_thesis: for Y being non empty set for f being Function of X,Y for A being Subset of X st f is bijective holds (f .: A) ` = f .: (A `) let Y be non empty set ; ::_thesis: for f being Function of X,Y for A being Subset of X st f is bijective holds (f .: A) ` = f .: (A `) let f be Function of X,Y; ::_thesis: for A being Subset of X st f is bijective holds (f .: A) ` = f .: (A `) let A be Subset of X; ::_thesis: ( f is bijective implies (f .: A) ` = f .: (A `) ) assume f is bijective ; ::_thesis: (f .: A) ` = f .: (A `) then ( (f .: A) ` c= f .: (A `) & f .: (A `) c= (f .: A) ` ) by Th3, Th4; hence (f .: A) ` = f .: (A `) by XBOOLE_0:def_10; ::_thesis: verum end; begin theorem Th6: :: JORDAN1K:6 for T being TopSpace for A being Subset of T holds ( A is_a_component_of {} T iff A is empty ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( A is_a_component_of {} T iff A is empty ) let A be Subset of T; ::_thesis: ( A is_a_component_of {} T iff A is empty ) thus ( A is_a_component_of {} T implies A is empty ) by SPRECT_1:5, XBOOLE_1:3; ::_thesis: ( A is empty implies A is_a_component_of {} T ) assume A1: A is empty ; ::_thesis: A is_a_component_of {} T then reconsider B = A as Subset of (T | ({} T)) by XBOOLE_1:2; for C being Subset of (T | ({} T)) st C is connected & B c= C holds B = C by A1, XBOOLE_1:3; then B is a_component by A1, CONNSP_1:def_5; hence A is_a_component_of {} T by CONNSP_1:def_6; ::_thesis: verum end; theorem Th7: :: JORDAN1K:7 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; ::_thesis: 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 let A, B, C be Subset of T; ::_thesis: ( A c= B & A is_a_component_of C & B is_a_component_of C implies A = B ) assume that A1: A c= B and A2: A is_a_component_of C and A3: B is_a_component_of C ; ::_thesis: A = B percases ( C = {} or not C is empty ) ; suppose C = {} ; ::_thesis: A = B then A4: C = {} T ; then A = {} by A2, Th6; hence A = B by A3, A4, Th6; ::_thesis: verum end; suppose not C is empty ; ::_thesis: A = B then A <> {} by A2, SPRECT_1:4; hence A = B by A1, A2, A3, GOBOARD9:1, XBOOLE_1:69; ::_thesis: verum end; end; end; theorem :: JORDAN1K:8 for n being Element of NAT st n >= 1 holds for P being Subset of (Euclid n) st P is bounded holds not P ` is bounded proof let n be Element of NAT ; ::_thesis: ( n >= 1 implies for P being Subset of (Euclid n) st P is bounded holds not P ` is bounded ) assume A1: n >= 1 ; ::_thesis: for P being Subset of (Euclid n) st P is bounded holds not P ` is bounded REAL n c= the carrier of (Euclid n) ; then reconsider W = REAL n as Subset of (Euclid n) ; let P be Subset of (Euclid n); ::_thesis: ( P is bounded implies not P ` is bounded ) A2: P \/ (P `) = [#] (Euclid n) by PRE_TOPC:2 .= W ; assume ( P is bounded & P ` is bounded ) ; ::_thesis: contradiction hence contradiction by A1, A2, JORDAN2C:33, TBSP_1:13; ::_thesis: verum end; theorem Th9: :: JORDAN1K:9 for M being non empty MetrSpace for C being non empty Subset of (TopSpaceMetr M) for p being Point of (TopSpaceMetr M) holds (dist_min C) . p >= 0 proof let M be non empty MetrSpace; ::_thesis: for C being non empty Subset of (TopSpaceMetr M) for p being Point of (TopSpaceMetr M) holds (dist_min C) . p >= 0 let C be non empty Subset of (TopSpaceMetr M); ::_thesis: for p being Point of (TopSpaceMetr M) holds (dist_min C) . p >= 0 let p be Point of (TopSpaceMetr M); ::_thesis: (dist_min C) . p >= 0 A1: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5; then reconsider x = p as Point of M ; set B = [#] ((dist x) .: C); A2: [#] ((dist x) .: C) = (dist x) .: C by WEIERSTR:def_1; A3: for r being real number st r in [#] ((dist x) .: C) holds 0 <= r proof let r be real number ; ::_thesis: ( r in [#] ((dist x) .: C) implies 0 <= r ) assume r in [#] ((dist x) .: C) ; ::_thesis: 0 <= r 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_6; reconsider y9 = y as Point of M by A1, A4; r = dist (x,y9) by A5, WEIERSTR:def_4; hence 0 <= r by METRIC_1:5; ::_thesis: verum end; dom (dist x) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1; then lower_bound ([#] ((dist x) .: C)) >= 0 by A2, A3, SEQ_4:43; then lower_bound ((dist x) .: C) >= 0 by WEIERSTR:def_3; hence (dist_min C) . p >= 0 by WEIERSTR:def_6; ::_thesis: verum end; theorem Th10: :: JORDAN1K:10 for r being Real for M being non empty MetrSpace for C being non empty Subset of (TopSpaceMetr M) for 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 r be Real; ::_thesis: for M being non empty MetrSpace for C being non empty Subset of (TopSpaceMetr M) for 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 let M be non empty MetrSpace; ::_thesis: for C being non empty Subset of (TopSpaceMetr M) for 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 let C be non empty Subset of (TopSpaceMetr M); ::_thesis: for 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 let p be Point of M; ::_thesis: ( ( for q being Point of M st q in C holds dist (p,q) >= r ) implies (dist_min C) . p >= r ) assume A1: for q being Point of M st q in C holds dist (p,q) >= r ; ::_thesis: (dist_min C) . p >= r set B = [#] ((dist p) .: C); A2: [#] ((dist p) .: C) = (dist p) .: C by WEIERSTR:def_1; A3: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5; A4: for s being real number st s in [#] ((dist p) .: C) holds r <= s proof let s be real number ; ::_thesis: ( s in [#] ((dist p) .: C) implies r <= s ) assume s in [#] ((dist p) .: C) ; ::_thesis: r <= s then consider y being set such that y in dom (dist p) and A5: y in C and A6: s = (dist p) . y by A2, FUNCT_1:def_6; reconsider y9 = y as Point of M by A3, A5; s = dist (p,y9) by A6, WEIERSTR:def_4; hence r <= s by A1, A5; ::_thesis: verum end; dom (dist p) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1; then lower_bound ([#] ((dist p) .: C)) >= r by A2, A4, SEQ_4:43; then lower_bound ((dist p) .: C) >= r by WEIERSTR:def_3; hence (dist_min C) . p >= r by WEIERSTR:def_6; ::_thesis: verum end; theorem Th11: :: JORDAN1K:11 for M being non empty MetrSpace for A, B being non empty Subset of (TopSpaceMetr M) holds min_dist_min (A,B) >= 0 proof let M be non empty MetrSpace; ::_thesis: for A, B being non empty Subset of (TopSpaceMetr M) holds min_dist_min (A,B) >= 0 let A, B be non empty Subset of (TopSpaceMetr M); ::_thesis: min_dist_min (A,B) >= 0 set X = [#] ((dist_min A) .: B); A1: [#] ((dist_min A) .: B) = (dist_min A) .: B by WEIERSTR:def_1; A2: for r being real number st r in [#] ((dist_min A) .: B) holds 0 <= r proof let r be real number ; ::_thesis: ( r in [#] ((dist_min A) .: B) implies 0 <= r ) assume r in [#] ((dist_min A) .: B) ; ::_thesis: 0 <= r 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_6; reconsider y = y as Point of (TopSpaceMetr M) by A3; (dist_min A) . y >= 0 by Th9; hence 0 <= r by A4; ::_thesis: verum end; dom (dist_min A) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1; then lower_bound ([#] ((dist_min A) .: B)) >= 0 by A1, A2, SEQ_4:43; then lower_bound ((dist_min A) .: B) >= 0 by WEIERSTR:def_3; hence min_dist_min (A,B) >= 0 by WEIERSTR:def_7; ::_thesis: verum end; theorem Th12: :: JORDAN1K:12 for M being non empty MetrSpace for A, B being compact Subset of (TopSpaceMetr M) st A meets B holds min_dist_min (A,B) = 0 proof let M be non empty MetrSpace; ::_thesis: for A, B being compact Subset of (TopSpaceMetr M) st A meets B holds min_dist_min (A,B) = 0 let A, B be compact Subset of (TopSpaceMetr M); ::_thesis: ( A meets B implies min_dist_min (A,B) = 0 ) assume A meets B ; ::_thesis: min_dist_min (A,B) = 0 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_5; then reconsider p = p as Point of M by A1; ( min_dist_min (A,B) >= 0 & min_dist_min (A,B) <= dist (p,p) ) by A1, A2, Th11, WEIERSTR:34; hence min_dist_min (A,B) = 0 by METRIC_1:1; ::_thesis: verum end; theorem Th13: :: JORDAN1K:13 for r being Real for M being non empty MetrSpace 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 r be Real; ::_thesis: for M being non empty MetrSpace 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 let M be non empty MetrSpace; ::_thesis: 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 let A, B be non empty Subset of (TopSpaceMetr M); ::_thesis: ( ( for p, q being Point of M st p in A & q in B holds dist (p,q) >= r ) implies min_dist_min (A,B) >= r ) assume A1: for p, q being Point of M st p in A & q in B holds dist (p,q) >= r ; ::_thesis: min_dist_min (A,B) >= r set X = [#] ((dist_min A) .: B); A2: [#] ((dist_min A) .: B) = (dist_min A) .: B by WEIERSTR:def_1; A3: for s being real number st s in [#] ((dist_min A) .: B) holds r <= s proof let s be real number ; ::_thesis: ( s in [#] ((dist_min A) .: B) implies r <= s ) assume s in [#] ((dist_min A) .: B) ; ::_thesis: r <= s 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_6; reconsider y = y as Point of (TopSpaceMetr M) by A4; reconsider p = y as Point of M by TOPMETR:12; for q being Point of M st q in A holds dist (p,q) >= r by A1, A4; hence r <= s by A5, Th10; ::_thesis: verum end; dom (dist_min A) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1; then lower_bound ([#] ((dist_min A) .: B)) >= r by A2, A3, SEQ_4:43; then lower_bound ((dist_min A) .: B) >= r by WEIERSTR:def_3; hence min_dist_min (A,B) >= r by WEIERSTR:def_7; ::_thesis: verum end; begin theorem Th14: :: JORDAN1K:14 for n being Element of NAT for P, Q being Subset of (TOP-REAL n) holds ( not P is_a_component_of Q ` or P is_inside_component_of Q or P is_outside_component_of Q ) proof let n be Element of NAT ; ::_thesis: for P, Q being Subset of (TOP-REAL n) holds ( not P is_a_component_of Q ` or P is_inside_component_of Q or P is_outside_component_of Q ) let P, Q be Subset of (TOP-REAL n); ::_thesis: ( not P is_a_component_of Q ` or P is_inside_component_of Q or P is_outside_component_of Q ) thus ( not P is_a_component_of Q ` or P is_inside_component_of Q or P is_outside_component_of Q ) by JORDAN2C:def_2, JORDAN2C:def_3; ::_thesis: verum end; theorem :: JORDAN1K:15 for n being Element of NAT st n >= 1 holds BDD ({} (TOP-REAL n)) = {} (TOP-REAL n) proof let n be Element of NAT ; ::_thesis: ( n >= 1 implies BDD ({} (TOP-REAL n)) = {} (TOP-REAL n) ) set X = { B where B is Subset of (TOP-REAL n) : B is_inside_component_of {} (TOP-REAL n) } ; assume n >= 1 ; ::_thesis: BDD ({} (TOP-REAL n)) = {} (TOP-REAL n) then A1: not [#] (TOP-REAL n) is bounded by JORDAN2C:35; now__::_thesis:_not__{__B_where_B_is_Subset_of_(TOP-REAL_n)_:_B_is_inside_component_of_{}_(TOP-REAL_n)__}__<>_{} [#] (TOP-REAL n) is a_component ; then A2: [#] TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is a_component by CONNSP_1:45; (TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:93; then A3: [#] (TOP-REAL n) is_a_component_of [#] (TOP-REAL n) by A2, CONNSP_1:def_6; assume { B where B is Subset of (TOP-REAL n) : B is_inside_component_of {} (TOP-REAL n) } <> {} ; ::_thesis: contradiction then consider x being set such that A4: x in { B where B is Subset of (TOP-REAL n) : B is_inside_component_of {} (TOP-REAL n) } by XBOOLE_0:def_1; consider B being Subset of (TOP-REAL n) such that x = B and A5: B is_inside_component_of {} (TOP-REAL n) by A4; B is_a_component_of ({} (TOP-REAL n)) ` by A5, JORDAN2C:def_2; then B = [#] (TOP-REAL n) by A3, Th7; hence contradiction by A1, A5, JORDAN2C:def_2; ::_thesis: verum end; hence BDD ({} (TOP-REAL n)) = {} (TOP-REAL n) by JORDAN2C:def_4, ZFMISC_1:2; ::_thesis: verum end; theorem :: JORDAN1K:16 for n being Element of NAT holds BDD ([#] (TOP-REAL n)) = {} (TOP-REAL n) proof let n be Element of NAT ; ::_thesis: BDD ([#] (TOP-REAL n)) = {} (TOP-REAL n) BDD ([#] (TOP-REAL n)) c= ([#] (TOP-REAL n)) ` by JORDAN2C:25; then BDD ([#] (TOP-REAL n)) c= {} (TOP-REAL n) by XBOOLE_1:37; hence BDD ([#] (TOP-REAL n)) = {} (TOP-REAL n) by XBOOLE_1:3; ::_thesis: verum end; theorem :: JORDAN1K:17 for n being Element of NAT st n >= 1 holds UBD ({} (TOP-REAL n)) = [#] (TOP-REAL n) proof let n be Element of NAT ; ::_thesis: ( n >= 1 implies UBD ({} (TOP-REAL n)) = [#] (TOP-REAL n) ) set X = { B where B is Subset of (TOP-REAL n) : B is_outside_component_of {} (TOP-REAL n) } ; assume n >= 1 ; ::_thesis: UBD ({} (TOP-REAL n)) = [#] (TOP-REAL n) then A1: not [#] (TOP-REAL n) is bounded by JORDAN2C:35; thus UBD ({} (TOP-REAL n)) c= [#] (TOP-REAL n) ; :: according to XBOOLE_0:def_10 ::_thesis: [#] (TOP-REAL n) c= UBD ({} (TOP-REAL n)) [#] (TOP-REAL n) is a_component ; then A2: [#] TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is a_component by CONNSP_1:45; (TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:93; then A3: [#] (TOP-REAL n) is_a_component_of [#] (TOP-REAL n) by A2, CONNSP_1:def_6; [#] (TOP-REAL n) = ({} (TOP-REAL n)) ` ; then [#] (TOP-REAL n) is_outside_component_of {} (TOP-REAL n) by A1, A3, JORDAN2C:def_3; then [#] (TOP-REAL n) in { B where B is Subset of (TOP-REAL n) : B is_outside_component_of {} (TOP-REAL n) } ; then [#] (TOP-REAL n) c= union { B where B is Subset of (TOP-REAL n) : B is_outside_component_of {} (TOP-REAL n) } by ZFMISC_1:74; hence [#] (TOP-REAL n) c= UBD ({} (TOP-REAL n)) by JORDAN2C:def_5; ::_thesis: verum end; theorem :: JORDAN1K:18 for n being Element of NAT holds UBD ([#] (TOP-REAL n)) = {} (TOP-REAL n) proof let n be Element of NAT ; ::_thesis: UBD ([#] (TOP-REAL n)) = {} (TOP-REAL n) UBD ([#] (TOP-REAL n)) c= ([#] (TOP-REAL n)) ` by JORDAN2C:26; then UBD ([#] (TOP-REAL n)) c= {} (TOP-REAL n) by XBOOLE_1:37; hence UBD ([#] (TOP-REAL n)) = {} (TOP-REAL n) by XBOOLE_1:3; ::_thesis: verum end; theorem :: JORDAN1K:19 for n being Element of NAT for P being connected Subset of (TOP-REAL n) for Q being Subset of (TOP-REAL n) holds ( not P misses Q or P c= UBD Q or P c= BDD Q ) proof let n be Element of NAT ; ::_thesis: for P being connected Subset of (TOP-REAL n) for Q being Subset of (TOP-REAL n) holds ( not P misses Q or P c= UBD Q or P c= BDD Q ) let P be connected Subset of (TOP-REAL n); ::_thesis: for Q being Subset of (TOP-REAL n) holds ( not P misses Q or P c= UBD Q or P c= BDD Q ) let Q be Subset of (TOP-REAL n); ::_thesis: ( not P misses Q or P c= UBD Q or P c= BDD Q ) assume A1: P misses Q ; ::_thesis: ( P c= UBD Q or P c= BDD Q ) percases ( P is empty or Q = [#] (TOP-REAL n) or ( not P is empty & Q <> [#] (TOP-REAL n) ) ) ; suppose P is empty ; ::_thesis: ( P c= UBD Q or P c= BDD Q ) hence ( P c= UBD Q or P c= BDD Q ) by XBOOLE_1:2; ::_thesis: verum end; suppose Q = [#] (TOP-REAL n) ; ::_thesis: ( P c= UBD Q or P c= BDD Q ) then P = {} by A1, XBOOLE_1:67; hence ( P c= UBD Q or P c= BDD Q ) by XBOOLE_1:2; ::_thesis: verum end; supposethat A2: not P is empty and A3: Q <> [#] (TOP-REAL n) ; ::_thesis: ( P c= UBD Q or P c= BDD Q ) (Q `) ` <> [#] (TOP-REAL n) by A3; then A4: Q ` <> {} (TOP-REAL n) ; P c= Q ` by A1, SUBSET_1:23; then consider C being Subset of (TOP-REAL n) such that A5: C is_a_component_of Q ` and A6: P c= C by A2, A4, GOBOARD9:3; ( C is_inside_component_of Q or C is_outside_component_of Q ) by A5, Th14; then ( C c= UBD Q or C c= BDD Q ) by JORDAN2C:22, JORDAN2C:23; hence ( P c= UBD Q or P c= BDD Q ) by A6, XBOOLE_1:1; ::_thesis: verum end; end; end; begin theorem Th20: :: JORDAN1K:20 for q being Point of (TOP-REAL 2) for r being Real holds dist (|[0,0]|,(r * q)) = (abs r) * (dist (|[0,0]|,q)) proof let q be Point of (TOP-REAL 2); ::_thesis: for r being Real holds dist (|[0,0]|,(r * q)) = (abs r) * (dist (|[0,0]|,q)) let r be Real; ::_thesis: dist (|[0,0]|,(r * q)) = (abs r) * (dist (|[0,0]|,q)) A1: ( r ^2 >= 0 & (q `1) ^2 >= 0 ) by XREAL_1:63; A2: (q `2) ^2 >= 0 by XREAL_1:63; A3: ( |[0,0]| `1 = 0 & |[0,0]| `2 = 0 ) by EUCLID:52; then A4: dist (|[0,0]|,q) = sqrt (((0 - (q `1)) ^2) + ((0 - (q `2)) ^2)) by TOPREAL6:92 .= sqrt (((q `1) ^2) + ((q `2) ^2)) ; thus dist (|[0,0]|,(r * q)) = sqrt (((0 - ((r * q) `1)) ^2) + ((0 - ((r * q) `2)) ^2)) by A3, TOPREAL6:92 .= sqrt ((((r * q) `1) ^2) + ((- ((r * q) `2)) ^2)) .= sqrt (((r * (q `1)) ^2) + (((r * q) `2) ^2)) by TOPREAL3:4 .= sqrt (((r ^2) * ((q `1) ^2)) + ((r * (q `2)) ^2)) by TOPREAL3:4 .= sqrt ((r ^2) * (((q `1) ^2) + ((q `2) ^2))) .= (sqrt (r ^2)) * (sqrt (((q `1) ^2) + ((q `2) ^2))) by A1, A2, SQUARE_1:29 .= (abs r) * (dist (|[0,0]|,q)) by A4, COMPLEX1:72 ; ::_thesis: verum end; theorem Th21: :: JORDAN1K:21 for q1, q, q2 being Point of (TOP-REAL 2) holds dist ((q1 + q),(q2 + q)) = dist (q1,q2) proof let q1, q, q2 be Point of (TOP-REAL 2); ::_thesis: dist ((q1 + q),(q2 + q)) = dist (q1,q2) A1: ((q1 + q) `1) - ((q2 + q) `1) = ((q1 `1) + (q `1)) - ((q2 + q) `1) by TOPREAL3:2 .= ((q1 `1) + (q `1)) - ((q2 `1) + (q `1)) by TOPREAL3:2 .= ((q1 `1) - (q2 `1)) + 0 ; A2: ((q1 + q) `2) - ((q2 + q) `2) = ((q1 `2) + (q `2)) - ((q2 + q) `2) by TOPREAL3:2 .= ((q1 `2) + (q `2)) - ((q2 `2) + (q `2)) by TOPREAL3:2 .= ((q1 `2) - (q2 `2)) + 0 ; thus dist ((q1 + q),(q2 + q)) = sqrt (((((q1 + q) `1) - ((q2 + q) `1)) ^2) + ((((q1 + q) `2) - ((q2 + q) `2)) ^2)) by TOPREAL6:92 .= dist (q1,q2) by A1, A2, TOPREAL6:92 ; ::_thesis: verum end; theorem Th22: :: JORDAN1K:22 for p, q being Point of (TOP-REAL 2) st p <> q holds dist (p,q) > 0 proof let p, q be Point of (TOP-REAL 2); ::_thesis: ( p <> q implies dist (p,q) > 0 ) ex p9, q9 being Point of (Euclid 2) st ( p9 = p & q9 = q & dist (p,q) = dist (p9,q9) ) by TOPREAL6:def_1; hence ( p <> q implies dist (p,q) > 0 ) by METRIC_1:7; ::_thesis: verum end; theorem Th23: :: JORDAN1K:23 for q1, q, q2 being Point of (TOP-REAL 2) holds dist ((q1 - q),(q2 - q)) = dist (q1,q2) proof let q1, q, q2 be Point of (TOP-REAL 2); ::_thesis: dist ((q1 - q),(q2 - q)) = dist (q1,q2) ( q1 - q = q1 + (- q) & q2 - q = q2 + (- q) ) by EUCLID:41; hence dist ((q1 - q),(q2 - q)) = dist (q1,q2) by Th21; ::_thesis: verum end; theorem Th24: :: JORDAN1K:24 for p, q being Point of (TOP-REAL 2) holds dist (p,q) = dist ((- p),(- q)) proof let p, q be Point of (TOP-REAL 2); ::_thesis: dist (p,q) = dist ((- p),(- q)) thus dist (p,q) = dist ((q - q),(p - q)) by Th23 .= dist ((q - q),(p + (- q))) by EUCLID:41 .= dist (|[0,0]|,(p + (- q))) by EUCLID:42, EUCLID:54 .= dist ((p - p),(p + (- q))) by EUCLID:42, EUCLID:54 .= dist ((p + (- p)),(p + (- q))) by EUCLID:41 .= dist ((- p),(- q)) by Th21 ; ::_thesis: verum end; theorem Th25: :: JORDAN1K:25 for q, q1, q2 being Point of (TOP-REAL 2) holds dist ((q - q1),(q - q2)) = dist (q1,q2) proof let q, q1, q2 be Point of (TOP-REAL 2); ::_thesis: dist ((q - q1),(q - q2)) = dist (q1,q2) ( - (q - q1) = q1 - q & - (q - q2) = q2 - q ) by EUCLID:44; hence dist ((q - q1),(q - q2)) = dist ((q1 - q),(q2 - q)) by Th24 .= dist (q1,q2) by Th23 ; ::_thesis: verum end; theorem Th26: :: JORDAN1K:26 for p, q being Point of (TOP-REAL 2) for r being Real holds dist ((r * p),(r * q)) = (abs r) * (dist (p,q)) proof let p, q be Point of (TOP-REAL 2); ::_thesis: for r being Real holds dist ((r * p),(r * q)) = (abs r) * (dist (p,q)) let r be Real; ::_thesis: dist ((r * p),(r * q)) = (abs r) * (dist (p,q)) 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:42, EUCLID:54 .= dist (|[0,0]|,(r * (p - q))) by EUCLID:49 .= (abs r) * (dist (|[0,0]|,(p - q))) by Th20 .= (abs r) * (dist ((p - p),(p - q))) by EUCLID:42, EUCLID:54 .= (abs r) * (dist (p,q)) by Th25 ; ::_thesis: verum end; theorem Th27: :: JORDAN1K:27 for p, q being Point of (TOP-REAL 2) for r being Real st r <= 1 holds dist (p,((r * p) + ((1 - r) * q))) = (1 - r) * (dist (p,q)) proof let p, q be Point of (TOP-REAL 2); ::_thesis: for r being Real st r <= 1 holds dist (p,((r * p) + ((1 - r) * q))) = (1 - r) * (dist (p,q)) let r be Real; ::_thesis: ( r <= 1 implies dist (p,((r * p) + ((1 - r) * q))) = (1 - r) * (dist (p,q)) ) assume r <= 1 ; ::_thesis: dist (p,((r * p) + ((1 - r) * q))) = (1 - r) * (dist (p,q)) then 1 + r <= 1 + 1 by XREAL_1:6; then 1 - r >= 1 - 1 by XREAL_1:21; then A1: abs (1 - r) = 1 - r by ABSVALUE:def_1; thus dist (p,((r * p) + ((1 - r) * q))) = dist (((r + (1 - r)) * p),((r * p) + ((1 - r) * q))) by EUCLID:29 .= dist (((r * p) + ((1 - r) * p)),((r * p) + ((1 - r) * q))) by EUCLID:33 .= dist (((1 - r) * p),((1 - r) * q)) by Th21 .= (1 - r) * (dist (p,q)) by A1, Th26 ; ::_thesis: verum end; theorem Th28: :: JORDAN1K:28 for q, p being Point of (TOP-REAL 2) for r being Real st 0 <= r holds dist (q,((r * p) + ((1 - r) * q))) = r * (dist (p,q)) proof let q, p be Point of (TOP-REAL 2); ::_thesis: for r being Real st 0 <= r holds dist (q,((r * p) + ((1 - r) * q))) = r * (dist (p,q)) let r be Real; ::_thesis: ( 0 <= r implies dist (q,((r * p) + ((1 - r) * q))) = r * (dist (p,q)) ) assume 0 <= r ; ::_thesis: dist (q,((r * p) + ((1 - r) * q))) = r * (dist (p,q)) then A1: abs r = r by ABSVALUE:def_1; thus dist (q,((r * p) + ((1 - r) * q))) = dist (((r * p) + ((1 - r) * q)),((r + (1 - r)) * q)) by EUCLID:29 .= dist (((r * q) + ((1 - r) * q)),((r * p) + ((1 - r) * q))) by EUCLID:33 .= dist ((r * q),(r * p)) by Th21 .= r * (dist (p,q)) by A1, Th26 ; ::_thesis: verum end; theorem Th29: :: JORDAN1K:29 for p, q1, q2 being Point of (TOP-REAL 2) st p in LSeg (q1,q2) holds (dist (q1,p)) + (dist (p,q2)) = dist (q1,q2) proof let p, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( p in LSeg (q1,q2) implies (dist (q1,p)) + (dist (p,q2)) = dist (q1,q2) ) assume p in LSeg (q1,q2) ; ::_thesis: (dist (q1,p)) + (dist (p,q2)) = dist (q1,q2) then consider r being Real such that A1: ( p = ((1 - r) * q1) + (r * q2) & 0 <= r & r <= 1 ) ; ( dist (q1,p) = r * (dist (q1,q2)) & dist (q2,p) = (1 - r) * (dist (q1,q2)) ) by A1, Th27, Th28; hence (dist (q1,p)) + (dist (p,q2)) = dist (q1,q2) ; ::_thesis: verum end; theorem :: JORDAN1K:30 for q1, q2, p being Point of (TOP-REAL 2) st q1 in LSeg (q2,p) & q1 <> q2 holds dist (q1,p) < dist (q2,p) proof let q1, q2, p be Point of (TOP-REAL 2); ::_thesis: ( q1 in LSeg (q2,p) & q1 <> q2 implies dist (q1,p) < dist (q2,p) ) assume that A1: q1 in LSeg (q2,p) and A2: q1 <> q2 ; ::_thesis: dist (q1,p) < dist (q2,p) (dist (q2,q1)) + (dist (q1,p)) = dist (q2,p) by A1, Th29; hence dist (q1,p) < dist (q2,p) by A2, Th22, XREAL_1:29; ::_thesis: verum end; theorem Th31: :: JORDAN1K:31 for r being Real for y being Point of (Euclid 2) st y = |[0,0]| holds Ball (y,r) = { q where q is Point of (TOP-REAL 2) : |.q.| < r } proof let r be Real; ::_thesis: for y being Point of (Euclid 2) st y = |[0,0]| holds Ball (y,r) = { q where q is Point of (TOP-REAL 2) : |.q.| < r } let y be Point of (Euclid 2); ::_thesis: ( y = |[0,0]| implies Ball (y,r) = { q where q is Point of (TOP-REAL 2) : |.q.| < r } ) set X = { q where q is Point of (TOP-REAL 2) : |.(|[0,0]| - q).| < r } ; set Y = { q where q is Point of (TOP-REAL 2) : |.q.| < r } ; A1: { q where q is Point of (TOP-REAL 2) : |.(|[0,0]| - q).| < r } c= { q where q is Point of (TOP-REAL 2) : |.q.| < r } proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { q where q is Point of (TOP-REAL 2) : |.(|[0,0]| - q).| < r } or u in { q where q is Point of (TOP-REAL 2) : |.q.| < r } ) assume u in { q where q is Point of (TOP-REAL 2) : |.(|[0,0]| - q).| < r } ; ::_thesis: u in { q where q is Point of (TOP-REAL 2) : |.q.| < r } then consider q being Point of (TOP-REAL 2) such that A2: ( u = q & |.(|[0,0]| - q).| < r ) ; |.(|[0,0]| - q).| = |.(q - |[0,0]|).| by TOPRNS_1:27 .= |.q.| by EUCLID:54, RLVECT_1:13 ; hence u in { q where q is Point of (TOP-REAL 2) : |.q.| < r } by A2; ::_thesis: verum end; A3: { q where q is Point of (TOP-REAL 2) : |.q.| < r } c= { q where q is Point of (TOP-REAL 2) : |.(|[0,0]| - q).| < r } proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { q where q is Point of (TOP-REAL 2) : |.q.| < r } or u in { q where q is Point of (TOP-REAL 2) : |.(|[0,0]| - q).| < r } ) assume u in { q where q is Point of (TOP-REAL 2) : |.q.| < r } ; ::_thesis: u in { q where q is Point of (TOP-REAL 2) : |.(|[0,0]| - q).| < r } then consider q being Point of (TOP-REAL 2) such that A4: ( u = q & |.q.| < r ) ; |.(|[0,0]| - q).| = |.(q - |[0,0]|).| by TOPRNS_1:27 .= |.q.| by EUCLID:54, RLVECT_1:13 ; hence u in { q where q is Point of (TOP-REAL 2) : |.(|[0,0]| - q).| < r } by A4; ::_thesis: verum end; assume y = |[0,0]| ; ::_thesis: Ball (y,r) = { q where q is Point of (TOP-REAL 2) : |.q.| < r } hence Ball (y,r) = { q where q is Point of (TOP-REAL 2) : |.(|[0,0]| - q).| < r } by JGRAPH_2:2 .= { q where q is Point of (TOP-REAL 2) : |.q.| < r } by A1, A3, XBOOLE_0:def_10 ; ::_thesis: verum end; begin theorem Th32: :: JORDAN1K:32 for p being Point of (TOP-REAL 2) for r, s1, s2 being Real holds (AffineMap (r,s1,r,s2)) . p = (r * p) + |[s1,s2]| proof let p be Point of (TOP-REAL 2); ::_thesis: for r, s1, s2 being Real holds (AffineMap (r,s1,r,s2)) . p = (r * p) + |[s1,s2]| let r, s1, s2 be Real; ::_thesis: (AffineMap (r,s1,r,s2)) . p = (r * p) + |[s1,s2]| 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:4 .= |[(((r * p) `1) + s1),(((r * p) `2) + s2)]| by TOPREAL3:4 .= |[((r * p) `1),((r * p) `2)]| + |[s1,s2]| by EUCLID:56 .= (r * p) + |[s1,s2]| by EUCLID:53 ; ::_thesis: verum end; theorem Th33: :: JORDAN1K:33 for q, p being Point of (TOP-REAL 2) for r being Real holds (AffineMap (r,(q `1),r,(q `2))) . p = (r * p) + q proof let q, p be Point of (TOP-REAL 2); ::_thesis: for r being Real holds (AffineMap (r,(q `1),r,(q `2))) . p = (r * p) + q let r be Real; ::_thesis: (AffineMap (r,(q `1),r,(q `2))) . p = (r * p) + q thus (AffineMap (r,(q `1),r,(q `2))) . p = (r * p) + |[(q `1),(q `2)]| by Th32 .= (r * p) + q by EUCLID:53 ; ::_thesis: verum end; theorem Th34: :: JORDAN1K:34 for s1, s2, t1, t2 being Real st s1 > 0 & s2 > 0 holds (AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2)))) = id (REAL 2) proof let s1, s2, t1, t2 be Real; ::_thesis: ( s1 > 0 & s2 > 0 implies (AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2)))) = id (REAL 2) ) the carrier of (TOP-REAL 2) = REAL 2 by EUCLID:22; then reconsider f = id (REAL 2) as Function of the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2) ; assume that A1: s1 > 0 and A2: s2 > 0 ; ::_thesis: (AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2)))) = id (REAL 2) now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_holds_((AffineMap_(s1,t1,s2,t2))_*_(AffineMap_((1_/_s1),(-_(t1_/_s1)),(1_/_s2),(-_(t2_/_s2)))))_._p_=_f_._p let p be Point of (TOP-REAL 2); ::_thesis: ((AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2))))) . p = f . p set q = |[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]|; A3: |[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]| `2 = ((1 / s2) * (p `2)) - (t2 / s2) by EUCLID:52; p in the carrier of (TOP-REAL 2) ; then A4: p in REAL 2 by EUCLID:22; A5: s1 * (1 / s1) = 1 by A1, XCMPLX_1:106; 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:15 .= (AffineMap (s1,t1,s2,t2)) . |[(((1 / s1) * (p `1)) + (- (t1 / s1))),(((1 / s2) * (p `2)) + (- (t2 / s2)))]| by JGRAPH_2:def_2 .= |[((s1 * (|[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]| `1)) + t1),((s2 * (|[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]| `2)) + t2)]| by JGRAPH_2:def_2 .= |[((s1 * (((1 / s1) * (p `1)) - (t1 / s1))) + t1),((s2 * (|[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]| `2)) + t2)]| by EUCLID:52 .= |[((((s1 * (1 / s1)) * (p `1)) - (s1 * (t1 / s1))) + t1),((s2 * (|[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]| `2)) + t2)]| .= |[(((1 * (p `1)) - (1 * t1)) + t1),((s2 * (|[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]| `2)) + t2)]| by A1, A5, XCMPLX_1:87 .= |[(p `1),(((s2 * ((1 / s2) * (p `2))) - (s2 * (t2 / s2))) + t2)]| by A3 .= |[(p `1),((((s2 * (1 / s2)) * (p `2)) - t2) + t2)]| by A2, XCMPLX_1:87 .= |[(p `1),(((1 * (p `2)) - (1 * t2)) + t2)]| by A2, XCMPLX_1:106 .= p by EUCLID:53 .= f . p by A4, FUNCT_1:18 ; ::_thesis: verum end; hence (AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2)))) = id (REAL 2) by FUNCT_2:63; ::_thesis: verum end; theorem Th35: :: JORDAN1K:35 for q being Point of (TOP-REAL 2) for r being Real for y, x being Point of (Euclid 2) st y = |[0,0]| & x = q & r > 0 holds (AffineMap (r,(q `1),r,(q `2))) .: (Ball (y,1)) = Ball (x,r) proof let q be Point of (TOP-REAL 2); ::_thesis: for r being Real for y, x being Point of (Euclid 2) st y = |[0,0]| & x = q & r > 0 holds (AffineMap (r,(q `1),r,(q `2))) .: (Ball (y,1)) = Ball (x,r) let r be Real; ::_thesis: for y, x being Point of (Euclid 2) st y = |[0,0]| & x = q & r > 0 holds (AffineMap (r,(q `1),r,(q `2))) .: (Ball (y,1)) = Ball (x,r) let y, x be Point of (Euclid 2); ::_thesis: ( y = |[0,0]| & x = q & r > 0 implies (AffineMap (r,(q `1),r,(q `2))) .: (Ball (y,1)) = Ball (x,r) ) assume that A1: y = |[0,0]| and A2: x = q and A3: r > 0 ; ::_thesis: (AffineMap (r,(q `1),r,(q `2))) .: (Ball (y,1)) = Ball (x,r) reconsider A = Ball (y,1), B = Ball (x,r) as Subset of (TOP-REAL 2) by TOPREAL3:8; A4: B c= (AffineMap (r,(q `1),r,(q `2))) .: A proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in B or u in (AffineMap (r,(q `1),r,(q `2))) .: A ) assume A5: u in B ; ::_thesis: u in (AffineMap (r,(q `1),r,(q `2))) .: A then reconsider q1 = u as Point of (TOP-REAL 2) ; reconsider x1 = q1 as Element of (Euclid 2) by TOPREAL3:8; set q2 = (AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1; consider z1, z2 being Point of (Euclid 2) such that A6: z1 = q and A7: z2 = (r * ((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1)) + q and A8: dist (q,((r * ((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1)) + q)) = dist (z1,z2) by TOPREAL6:def_1; consider z3, z4 being Point of (Euclid 2) such that A9: z3 = |[0,0]| and A10: z4 = (AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1 and A11: dist (|[0,0]|,((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1)) = dist (z3,z4) by TOPREAL6:def_1; z2 = (AffineMap (r,(q `1),r,(q `2))) . ((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1) by A7, Th33 .= ((AffineMap (r,(q `1),r,(q `2))) * (AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r))))) . q1 by FUNCT_2:15 .= (id (REAL 2)) . q1 by A3, Th34 .= x1 by FUNCT_1:18 ; then dist (x,x1) = dist ((|[0,0]| + q),((r * ((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1)) + q)) by A2, A6, A8, EUCLID:27, EUCLID:54 .= dist (|[0,0]|,(r * ((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1))) by Th21 .= (abs r) * (dist (|[0,0]|,((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1))) by Th20 .= r * (dist (y,z4)) by A1, A3, A9, A11, ABSVALUE:def_1 ; then r * (dist (y,z4)) < 1 * r by A5, METRIC_1:11; then dist (y,z4) < 1 by A3, XREAL_1:64; then A12: (AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1 in A by A10, METRIC_1:11; (AffineMap (r,(q `1),r,(q `2))) . ((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1) = ((AffineMap (r,(q `1),r,(q `2))) * (AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r))))) . q1 by FUNCT_2:15 .= (id (REAL 2)) . q1 by A3, Th34 .= (id (TOP-REAL 2)) . q1 by EUCLID:22 .= q1 by FUNCT_1:18 ; hence u in (AffineMap (r,(q `1),r,(q `2))) .: A by A12, FUNCT_2:35; ::_thesis: verum end; (AffineMap (r,(q `1),r,(q `2))) .: A c= B proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in (AffineMap (r,(q `1),r,(q `2))) .: A or u in B ) assume A13: u in (AffineMap (r,(q `1),r,(q `2))) .: A ; ::_thesis: u in B then reconsider q1 = u as Point of (TOP-REAL 2) ; consider q2 being Point of (TOP-REAL 2) such that A14: q2 in A and A15: q1 = (AffineMap (r,(q `1),r,(q `2))) . q2 by A13, FUNCT_2:65; reconsider x1 = q1, x2 = q2 as Element of (Euclid 2) by TOPREAL3:8; A16: dist (y,x2) < 1 by A14, METRIC_1:11; A17: ex z3, z4 being Point of (Euclid 2) st ( z3 = |[0,0]| & z4 = q2 & dist (|[0,0]|,q2) = dist (z3,z4) ) by TOPREAL6:def_1; A18: ex z1, z2 being Point of (Euclid 2) st ( z1 = q & z2 = (r * q2) + q & dist (q,((r * q2) + q)) = dist (z1,z2) ) by TOPREAL6:def_1; q1 = (r * q2) + q by A15, Th33; then dist (x,x1) = dist ((|[0,0]| + q),((r * q2) + q)) by A2, A18, EUCLID:27, EUCLID:54 .= dist (|[0,0]|,(r * q2)) by Th21 .= (abs r) * (dist (|[0,0]|,q2)) by Th20 .= r * (dist (y,x2)) by A1, A3, A17, ABSVALUE:def_1 ; then dist (x,x1) < r by A3, A16, XREAL_1:157; hence u in B by METRIC_1:11; ::_thesis: verum end; hence (AffineMap (r,(q `1),r,(q `2))) .: (Ball (y,1)) = Ball (x,r) by A4, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th36: :: JORDAN1K:36 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; ::_thesis: ( A > 0 & C > 0 implies AffineMap (A,B,C,D) is onto ) assume A1: ( A > 0 & C > 0 ) ; ::_thesis: AffineMap (A,B,C,D) is onto thus rng (AffineMap (A,B,C,D)) c= the carrier of (TOP-REAL 2) ; :: according to XBOOLE_0:def_10,FUNCT_2:def_3 ::_thesis: the carrier of (TOP-REAL 2) c= rng (AffineMap (A,B,C,D)) let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the carrier of (TOP-REAL 2) or e in rng (AffineMap (A,B,C,D)) ) assume e in the carrier of (TOP-REAL 2) ; ::_thesis: e in rng (AffineMap (A,B,C,D)) then reconsider q1 = e as Point of (TOP-REAL 2) ; set q2 = (AffineMap ((1 / A),(- (B / A)),(1 / C),(- (D / C)))) . q1; A2: the carrier of (TOP-REAL 2) = REAL 2 by EUCLID:22; (AffineMap (A,B,C,D)) . ((AffineMap ((1 / A),(- (B / A)),(1 / C),(- (D / C)))) . q1) = ((AffineMap (A,B,C,D)) * (AffineMap ((1 / A),(- (B / A)),(1 / C),(- (D / C))))) . q1 by FUNCT_2:15 .= (id (REAL 2)) . q1 by A1, Th34 .= q1 by A2, FUNCT_1:18 ; hence e in rng (AffineMap (A,B,C,D)) by FUNCT_2:4; ::_thesis: verum end; theorem :: JORDAN1K:37 for r being Real for x being Point of (Euclid 2) holds (Ball (x,r)) ` is connected Subset of (TOP-REAL 2) proof let r be Real; ::_thesis: for x being Point of (Euclid 2) holds (Ball (x,r)) ` is connected Subset of (TOP-REAL 2) let x be Point of (Euclid 2); ::_thesis: (Ball (x,r)) ` is connected Subset of (TOP-REAL 2) set C = (Ball (x,r)) ` ; percases ( r <= 0 or r > 0 ) ; suppose r <= 0 ; ::_thesis: (Ball (x,r)) ` is connected Subset of (TOP-REAL 2) then Ball (x,r) = {} (TOP-REAL 2) by TBSP_1:12; then A1: (Ball (x,r)) ` = [#] (TOP-REAL 2) by TOPREAL3:8; thus (Ball (x,r)) ` is connected Subset of (TOP-REAL 2) by A1; ::_thesis: verum end; supposeA2: r > 0 ; ::_thesis: (Ball (x,r)) ` is connected Subset of (TOP-REAL 2) reconsider q = x as Point of (TOP-REAL 2) by TOPREAL3:8; reconsider y = |[0,0]| as Point of (Euclid 2) by TOPREAL3:8; reconsider Q = Ball (x,r), J = Ball (y,1) as Subset of (TOP-REAL 2) by TOPREAL3:8; A3: Q = (AffineMap (r,(q `1),r,(q `2))) .: J by A2, Th35; reconsider P = Q ` , K = J ` as Subset of (TOP-REAL 2) ; A4: K = (REAL 2) \ (Ball (y,1)) by TOPREAL3:8 .= (REAL 2) \ { q1 where q1 is Point of (TOP-REAL 2) : |.q1.| < 1 } by Th31 ; ( AffineMap (r,(q `1),r,(q `2)) is one-to-one & AffineMap (r,(q `1),r,(q `2)) is onto ) by A2, Th36, JGRAPH_2:44; then ( the carrier of (TOP-REAL 2) = the carrier of (Euclid 2) & P = (AffineMap (r,(q `1),r,(q `2))) .: K ) by A3, Th5, TOPREAL3:8; hence (Ball (x,r)) ` is connected Subset of (TOP-REAL 2) by A4, JORDAN2C:53, TOPS_2:61; ::_thesis: verum end; end; end; begin definition let n be Element of NAT ; let A, B be Subset of (TOP-REAL n); func dist_min (A,B) -> Real means :Def1: :: JORDAN1K:def 1 ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st ( A = A9 & B = B9 & it = min_dist_min (A9,B9) ); existence ex b1 being Real ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st ( A = A9 & B = B9 & b1 = min_dist_min (A9,B9) ) proof TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8; then reconsider A9 = A, B9 = B as Subset of (TopSpaceMetr (Euclid n)) ; take min_dist_min (A9,B9) ; ::_thesis: ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st ( A = A9 & B = B9 & min_dist_min (A9,B9) = min_dist_min (A9,B9) ) take A9 ; ::_thesis: ex B9 being Subset of (TopSpaceMetr (Euclid n)) st ( A = A9 & B = B9 & min_dist_min (A9,B9) = min_dist_min (A9,B9) ) take B9 ; ::_thesis: ( A = A9 & B = B9 & min_dist_min (A9,B9) = min_dist_min (A9,B9) ) thus ( A = A9 & B = B9 & min_dist_min (A9,B9) = min_dist_min (A9,B9) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Real st ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st ( A = A9 & B = B9 & b1 = min_dist_min (A9,B9) ) & ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st ( A = A9 & B = B9 & b2 = min_dist_min (A9,B9) ) holds b1 = b2 ; end; :: deftheorem Def1 defines dist_min JORDAN1K:def_1_:_ for n being Element of NAT for A, B being Subset of (TOP-REAL n) for b4 being Real holds ( b4 = dist_min (A,B) iff ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st ( A = A9 & B = B9 & b4 = min_dist_min (A9,B9) ) ); definition let M be non empty MetrSpace; let P, Q be non empty compact Subset of (TopSpaceMetr M); :: original: min_dist_min redefine func min_dist_min (P,Q) -> Element of REAL ; commutativity for P, Q being non empty compact Subset of (TopSpaceMetr M) holds min_dist_min (P,Q) = min_dist_min (Q,P) proof let P, Q be non empty compact Subset of (TopSpaceMetr M); ::_thesis: min_dist_min (P,Q) = min_dist_min (Q,P) consider y1, y2 being Point of M such that A1: ( y1 in Q & y2 in P ) and A2: dist (y1,y2) = min_dist_min (Q,P) by WEIERSTR:30; consider x1, x2 being Point of M such that A3: ( x1 in P & x2 in Q ) and A4: dist (x1,x2) = min_dist_min (P,Q) by WEIERSTR:30; ( dist (x1,x2) <= dist (y1,y2) & dist (y1,y2) <= dist (x1,x2) ) by A1, A2, A3, A4, WEIERSTR:34; hence min_dist_min (P,Q) = min_dist_min (Q,P) by A2, A4, XXREAL_0:1; ::_thesis: verum end; :: original: max_dist_max redefine func max_dist_max (P,Q) -> Element of REAL ; commutativity for P, Q being non empty compact Subset of (TopSpaceMetr M) holds max_dist_max (P,Q) = max_dist_max (Q,P) proof let P, Q be non empty compact Subset of (TopSpaceMetr M); ::_thesis: max_dist_max (P,Q) = max_dist_max (Q,P) consider y1, y2 being Point of M such that A5: ( y1 in Q & y2 in P ) and A6: dist (y1,y2) = max_dist_max (Q,P) by WEIERSTR:33; consider x1, x2 being Point of M such that A7: ( x1 in P & x2 in Q ) and A8: dist (x1,x2) = max_dist_max (P,Q) by WEIERSTR:33; ( dist (x1,x2) <= dist (y1,y2) & dist (y1,y2) <= dist (x1,x2) ) by A5, A6, A7, A8, WEIERSTR:34; hence max_dist_max (P,Q) = max_dist_max (Q,P) by A6, A8, XXREAL_0:1; ::_thesis: verum end; end; definition let n be Element of NAT ; let A, B be non empty compact Subset of (TOP-REAL n); :: original: dist_min redefine func dist_min (A,B) -> Real; commutativity for A, B being non empty compact Subset of (TOP-REAL n) holds dist_min (A,B) = dist_min (B,A) proof let A, B be non empty compact Subset of (TOP-REAL n); ::_thesis: dist_min (A,B) = dist_min (B,A) consider A9, B9 being Subset of (TopSpaceMetr (Euclid n)) such that A1: ( A = A9 & B = B9 ) and A2: dist_min (A,B) = min_dist_min (A9,B9) by Def1; TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8; then reconsider A9 = A9, B9 = B9 as non empty compact Subset of (TopSpaceMetr (Euclid n)) by A1, COMPTS_1:23; dist_min (A,B) = min_dist_min (B9,A9) by A2; hence dist_min (A,B) = dist_min (B,A) by A1, Def1; ::_thesis: verum end; end; theorem Th38: :: JORDAN1K:38 for n being Element of NAT for A, B being non empty Subset of (TOP-REAL n) holds dist_min (A,B) >= 0 proof let n be Element of NAT ; ::_thesis: for A, B being non empty Subset of (TOP-REAL n) holds dist_min (A,B) >= 0 let A, B be non empty Subset of (TOP-REAL n); ::_thesis: dist_min (A,B) >= 0 ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st ( A = A9 & B = B9 & dist_min (A,B) = min_dist_min (A9,B9) ) by Def1; hence dist_min (A,B) >= 0 by Th11; ::_thesis: verum end; theorem Th39: :: JORDAN1K:39 for n being Element of NAT for A, B being compact Subset of (TOP-REAL n) st A meets B holds dist_min (A,B) = 0 proof let n be Element of NAT ; ::_thesis: for A, B being compact Subset of (TOP-REAL n) st A meets B holds dist_min (A,B) = 0 let A, B be compact Subset of (TOP-REAL n); ::_thesis: ( A meets B implies dist_min (A,B) = 0 ) assume A1: A meets B ; ::_thesis: dist_min (A,B) = 0 consider A9, B9 being Subset of (TopSpaceMetr (Euclid n)) such that A2: ( A = A9 & B = B9 ) and A3: dist_min (A,B) = min_dist_min (A9,B9) by Def1; TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8; then ( A9 is compact & B9 is compact ) by A2, COMPTS_1:23; hence dist_min (A,B) = 0 by A1, A2, A3, Th12; ::_thesis: verum end; theorem Th40: :: JORDAN1K:40 for n being Element of NAT for r being Real 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 n be Element of NAT ; ::_thesis: for r being Real 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 let r be Real; ::_thesis: 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 let A, B be non empty Subset of (TOP-REAL n); ::_thesis: ( ( for p, q being Point of (TOP-REAL n) st p in A & q in B holds dist (p,q) >= r ) implies dist_min (A,B) >= r ) assume A1: for p, q being Point of (TOP-REAL n) st p in A & q in B holds dist (p,q) >= r ; ::_thesis: dist_min (A,B) >= 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 be Point of (Euclid n); ::_thesis: ( a in A & b in B implies dist (a,b) >= r ) assume A3: ( a in A & b in B ) ; ::_thesis: dist (a,b) >= r reconsider p = a, q = b as Point of (TOP-REAL n) by TOPREAL3:8; ex a, b being Point of (Euclid n) st ( p = a & q = b & dist (p,q) = dist (a,b) ) by TOPREAL6:def_1; hence dist (a,b) >= r by A1, A3; ::_thesis: verum end; ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st ( A = A9 & B = B9 & dist_min (A,B) = min_dist_min (A9,B9) ) by Def1; hence dist_min (A,B) >= r by A2, Th13; ::_thesis: verum end; theorem Th41: :: JORDAN1K:41 for n being Element of NAT for D being Subset of (TOP-REAL n) for 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 n be Element of NAT ; ::_thesis: for D being Subset of (TOP-REAL n) for A, C being non empty Subset of (TOP-REAL n) st C c= D holds dist_min (A,D) <= dist_min (A,C) let D be Subset of (TOP-REAL n); ::_thesis: for A, C being non empty Subset of (TOP-REAL n) st C c= D holds dist_min (A,D) <= dist_min (A,C) let A, C be non empty Subset of (TOP-REAL n); ::_thesis: ( C c= D implies dist_min (A,D) <= dist_min (A,C) ) assume A1: C c= D ; ::_thesis: dist_min (A,D) <= dist_min (A,C) consider A9, D9 being Subset of (TopSpaceMetr (Euclid n)) such that A2: A = A9 and A3: ( D = D9 & dist_min (A,D) = min_dist_min (A9,D9) ) by Def1; reconsider f = dist_min A9 as Function of the carrier of (TopSpaceMetr (Euclid n)),REAL by TOPMETR:17; reconsider Y = f .: D9 as Subset of REAL ; A4: Y is bounded_below proof take 0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of Y let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in Y or 0 <= r ) assume r in Y ; ::_thesis: 0 <= r then ex c being Element of (TopSpaceMetr (Euclid n)) st ( c in D9 & r = f . c ) by FUNCT_2:65; hence 0 <= r by A2, Th9; ::_thesis: verum end; A5: lower_bound Y = lower_bound ([#] ((dist_min A9) .: D9)) by WEIERSTR:def_1 .= lower_bound ((dist_min A9) .: D9) by WEIERSTR:def_3 .= min_dist_min (A9,D9) by WEIERSTR:def_7 ; consider A99, C9 being Subset of (TopSpaceMetr (Euclid n)) such that A6: A = A99 and A7: C = C9 and A8: dist_min (A,C) = min_dist_min (A99,C9) by Def1; dom f = the carrier of (TopSpaceMetr (Euclid n)) by FUNCT_2:def_1; then reconsider X = f .: C9 as non empty Subset of REAL by A7; lower_bound X = lower_bound ([#] ((dist_min A9) .: C9)) by WEIERSTR:def_1 .= lower_bound ((dist_min A9) .: C9) by WEIERSTR:def_3 .= min_dist_min (A9,C9) by WEIERSTR:def_7 ; hence dist_min (A,D) <= dist_min (A,C) by A1, A2, A3, A6, A7, A8, A5, A4, RELAT_1:123, SEQ_4:47; ::_thesis: verum end; theorem Th42: :: JORDAN1K:42 for n being Element of NAT 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 n be Element of NAT ; ::_thesis: 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) ) let A, B be non empty compact Subset of (TOP-REAL n); ::_thesis: ex p, q being Point of (TOP-REAL n) st ( p in A & q in B & dist_min (A,B) = dist (p,q) ) consider A9, B9 being Subset of (TopSpaceMetr (Euclid n)) such that A1: ( A = A9 & B = B9 ) and A2: dist_min (A,B) = min_dist_min (A9,B9) by Def1; TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8; then ( A9 is compact & B9 is compact ) by A1, COMPTS_1:23; then consider x1, x2 being Point of (Euclid n) such that A3: ( x1 in A9 & x2 in B9 ) and A4: dist (x1,x2) = min_dist_min (A9,B9) by A1, WEIERSTR:30; reconsider p = x1, q = x2 as Point of (TOP-REAL n) by TOPREAL3:8; take p ; ::_thesis: ex q being Point of (TOP-REAL n) st ( p in A & q in B & dist_min (A,B) = dist (p,q) ) take q ; ::_thesis: ( p in A & q in B & dist_min (A,B) = dist (p,q) ) thus ( p in A & q in B ) by A1, A3; ::_thesis: dist_min (A,B) = dist (p,q) thus dist_min (A,B) = dist (p,q) by A2, A4, TOPREAL6:def_1; ::_thesis: verum end; theorem Th43: :: JORDAN1K:43 for n being Element of NAT for p, q being Point of (TOP-REAL n) holds dist_min ({p},{q}) = dist (p,q) proof let n be Element of NAT ; ::_thesis: for p, q being Point of (TOP-REAL n) holds dist_min ({p},{q}) = dist (p,q) let p, q be Point of (TOP-REAL n); ::_thesis: dist_min ({p},{q}) = dist (p,q) consider p9, q9 being Point of (TOP-REAL n) such that A1: p9 in {p} and A2: ( q9 in {q} & dist_min ({p},{q}) = dist (p9,q9) ) by Th42; p = p9 by A1, TARSKI:def_1; hence dist_min ({p},{q}) = dist (p,q) by A2, TARSKI:def_1; ::_thesis: verum end; definition let n be Element of NAT ; let p be Point of (TOP-REAL n); let B be Subset of (TOP-REAL n); func dist (p,B) -> Real equals :: JORDAN1K:def 2 dist_min ({p},B); coherence dist_min ({p},B) is Real ; end; :: deftheorem defines dist JORDAN1K:def_2_:_ for n being Element of NAT for p being Point of (TOP-REAL n) for B being Subset of (TOP-REAL n) holds dist (p,B) = dist_min ({p},B); theorem :: JORDAN1K:44 for n being Element of NAT for A being non empty Subset of (TOP-REAL n) for p being Point of (TOP-REAL n) holds dist (p,A) >= 0 by Th38; theorem :: JORDAN1K:45 for n being Element of NAT for A being compact Subset of (TOP-REAL n) for p being Point of (TOP-REAL n) st p in A holds dist (p,A) = 0 by Th39, ZFMISC_1:48; theorem Th46: :: JORDAN1K:46 for n being Element of NAT for A being non empty compact Subset of (TOP-REAL n) for 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 n be Element of NAT ; ::_thesis: for A being non empty compact Subset of (TOP-REAL n) for 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) ) let A be non empty compact Subset of (TOP-REAL n); ::_thesis: for 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) ) let p be Point of (TOP-REAL n); ::_thesis: ex q being Point of (TOP-REAL n) st ( q in A & dist (p,A) = dist (p,q) ) consider q, p9 being Point of (TOP-REAL n) such that A1: q in A and A2: ( p9 in {p} & dist_min (A,{p}) = dist (q,p9) ) by Th42; take q ; ::_thesis: ( q in A & dist (p,A) = dist (p,q) ) thus q in A by A1; ::_thesis: dist (p,A) = dist (p,q) thus dist (p,A) = dist (p,q) by A2, TARSKI:def_1; ::_thesis: verum end; theorem :: JORDAN1K:47 for n being Element of NAT for C being non empty Subset of (TOP-REAL n) for D being Subset of (TOP-REAL n) st C c= D holds for q being Point of (TOP-REAL n) holds dist (q,D) <= dist (q,C) by Th41; theorem :: JORDAN1K:48 for n being Element of NAT for r being Real for A being non empty Subset of (TOP-REAL n) for 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 n be Element of NAT ; ::_thesis: for r being Real for A being non empty Subset of (TOP-REAL n) for 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 let r be Real; ::_thesis: for A being non empty Subset of (TOP-REAL n) for 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 let A be non empty Subset of (TOP-REAL n); ::_thesis: for 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 let p9 be Point of (TOP-REAL n); ::_thesis: ( ( for q being Point of (TOP-REAL n) st q in A holds dist (p9,q) >= r ) implies dist (p9,A) >= r ) assume A1: for q being Point of (TOP-REAL n) st q in A holds dist (p9,q) >= r ; ::_thesis: dist (p9,A) >= r for p, q being Point of (TOP-REAL n) st p in {p9} & q in A holds dist (p,q) >= r proof let p, q be Point of (TOP-REAL n); ::_thesis: ( p in {p9} & q in A implies dist (p,q) >= r ) assume that A2: p in {p9} and A3: q in A ; ::_thesis: dist (p,q) >= r p = p9 by A2, TARSKI:def_1; hence dist (p,q) >= r by A1, A3; ::_thesis: verum end; hence dist (p9,A) >= r by Th40; ::_thesis: verum end; theorem :: JORDAN1K:49 for n being Element of NAT for p, q being Point of (TOP-REAL n) holds dist (p,{q}) = dist (p,q) by Th43; theorem Th50: :: JORDAN1K:50 for n being Element of NAT for A being non empty Subset of (TOP-REAL n) for p, q being Point of (TOP-REAL n) st q in A holds dist (p,A) <= dist (p,q) proof let n be Element of NAT ; ::_thesis: for A being non empty Subset of (TOP-REAL n) for p, q being Point of (TOP-REAL n) st q in A holds dist (p,A) <= dist (p,q) let A be non empty Subset of (TOP-REAL n); ::_thesis: for p, q being Point of (TOP-REAL n) st q in A holds dist (p,A) <= dist (p,q) let p, q be Point of (TOP-REAL n); ::_thesis: ( q in A implies dist (p,A) <= dist (p,q) ) assume q in A ; ::_thesis: dist (p,A) <= dist (p,q) then {q} c= A by ZFMISC_1:31; then dist (p,A) <= dist (p,{q}) by Th41; hence dist (p,A) <= dist (p,q) by Th43; ::_thesis: verum end; theorem :: JORDAN1K:51 for A being non empty compact Subset of (TOP-REAL 2) for B being open Subset of (TOP-REAL 2) st A c= B holds for p being Point of (TOP-REAL 2) st not p in B holds dist (p,B) < dist (p,A) proof let A be non empty compact Subset of (TOP-REAL 2); ::_thesis: for B being open Subset of (TOP-REAL 2) st A c= B holds for p being Point of (TOP-REAL 2) st not p in B holds dist (p,B) < dist (p,A) let B be open Subset of (TOP-REAL 2); ::_thesis: ( A c= B implies for p being Point of (TOP-REAL 2) st not p in B holds dist (p,B) < dist (p,A) ) assume A1: A c= B ; ::_thesis: for p being Point of (TOP-REAL 2) st not p in B holds dist (p,B) < dist (p,A) TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def_8; then reconsider P = B as open Subset of (TopSpaceMetr (Euclid 2)) by PRE_TOPC:30; let p be Point of (TOP-REAL 2); ::_thesis: ( not p in B implies dist (p,B) < dist (p,A) ) assume A2: not p in B ; ::_thesis: dist (p,B) < dist (p,A) assume A3: dist (p,B) >= dist (p,A) ; ::_thesis: contradiction dist (p,B) <= dist (p,A) by A1, Th41; then A4: dist (p,B) = dist (p,A) by A3, XXREAL_0:1; consider q being Point of (TOP-REAL 2) such that A5: q in A and A6: dist (p,A) = dist (p,q) by Th46; reconsider a = q as Point of (Euclid 2) by TOPREAL3:8; consider r being real number such that A7: r > 0 and A8: Ball (a,r) c= P by A1, A5, TOPMETR:15; reconsider r = r as Element of REAL by XREAL_0:def_1; set s = r / (2 * (dist (p,q))); set q9 = ((1 - (r / (2 * (dist (p,q))))) * q) + ((r / (2 * (dist (p,q)))) * p); a in P by A1, A5; then A9: dist (p,q) > 0 by A2, Th22; then A10: 2 * (dist (p,q)) > 0 by XREAL_1:129; then 0 < r / (2 * (dist (p,q))) by A7, XREAL_1:139; then A11: 1 - (r / (2 * (dist (p,q)))) < 1 - 0 by XREAL_1:10; A12: ex p1, q1 being Point of (Euclid 2) st ( p1 = q & q1 = ((1 - (r / (2 * (dist (p,q))))) * q) + ((r / (2 * (dist (p,q)))) * p) & dist (q,(((1 - (r / (2 * (dist (p,q))))) * q) + ((r / (2 * (dist (p,q)))) * p))) = dist (p1,q1) ) by TOPREAL6:def_1; dist (q,(((1 - (r / (2 * (dist (p,q))))) * q) + ((r / (2 * (dist (p,q)))) * p))) = ((1 * r) / (2 * (dist (p,q)))) * (dist (p,q)) by A7, A9, Th28 .= ((r / 2) / ((dist (p,q)) / 1)) * (dist (p,q)) by XCMPLX_1:84 .= r / 2 by A9, XCMPLX_1:87 ; then dist (q,(((1 - (r / (2 * (dist (p,q))))) * q) + ((r / (2 * (dist (p,q)))) * p))) < r / 1 by A7, XREAL_1:76; then A13: ((1 - (r / (2 * (dist (p,q))))) * q) + ((r / (2 * (dist (p,q)))) * p) in Ball (a,r) by A12, METRIC_1:11; now__::_thesis:_not_r_>_dist_(p,q) A14: ex p1, q1 being Point of (Euclid 2) st ( p1 = p & q1 = q & dist (p,q) = dist (p1,q1) ) by TOPREAL6:def_1; assume r > dist (p,q) ; ::_thesis: contradiction then p in Ball (a,r) by A14, METRIC_1:11; hence contradiction by A2, A8; ::_thesis: verum end; then 1 * r < 2 * (dist (p,q)) by A7, XREAL_1:98; then r / (2 * (dist (p,q))) < 1 by A10, XREAL_1:191; then dist (p,(((1 - (r / (2 * (dist (p,q))))) * q) + ((r / (2 * (dist (p,q)))) * p))) = (1 - (r / (2 * (dist (p,q))))) * (dist (p,q)) by Th27; hence contradiction by A4, A6, A8, A9, A13, A11, Th50, XREAL_1:157; ::_thesis: verum end;