:: METRIC_1 semantic presentation begin definition attrc1 is strict ; struct MetrStruct -> 1-sorted ; aggrMetrStruct(# carrier, distance #) -> MetrStruct ; sel distance c1 -> Function of [: the carrier of c1, the carrier of c1:],REAL; end; registration cluster non empty strict for MetrStruct ; existence ex b1 being MetrStruct st ( not b1 is empty & b1 is strict ) proof set A = the non empty set ; set r = the Function of [: the non empty set , the non empty set :],REAL; take MetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) ; ::_thesis: ( not MetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) is empty & MetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) is strict ) thus not the carrier of MetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: MetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) is strict thus MetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) is strict ; ::_thesis: verum end; end; definition let A, B be set ; let f be PartFunc of [:A,B:],REAL; let a be Element of A; let b be Element of B; :: original: . redefine funcf . (a,b) -> Real; coherence f . (a,b) is Real proof percases ( [a,b] in dom f or not [a,b] in dom f ) ; suppose [a,b] in dom f ; ::_thesis: f . (a,b) is Real hence f . (a,b) is Real by PARTFUN1:4; ::_thesis: verum end; suppose not [a,b] in dom f ; ::_thesis: f . (a,b) is Real then f . (a,b) = 0 by FUNCT_1:def_2; hence f . (a,b) is Real ; ::_thesis: verum end; end; end; end; definition let M be MetrStruct ; let a, b be Element of M; func dist (a,b) -> Real equals :: METRIC_1:def 1 the distance of M . (a,b); coherence the distance of M . (a,b) is Real ; end; :: deftheorem defines dist METRIC_1:def_1_:_ for M being MetrStruct for a, b being Element of M holds dist (a,b) = the distance of M . (a,b); notation synonym Empty^2-to-zero for op2 ; end; definition :: original: Empty^2-to-zero redefine func Empty^2-to-zero -> Function of [:1,1:],REAL; coherence Empty^2-to-zero is Function of [:1,1:],REAL proof 0 in REAL ; then ( op2 is Function of [:1,1:],1 & 1 c= REAL ) by CARD_1:49, ZFMISC_1:31; hence Empty^2-to-zero is Function of [:1,1:],REAL by FUNCT_2:7; ::_thesis: verum end; end; Lm1: op2 . ({},{}) = 0 proof [{},{}] in [:{{}},{{}}:] by ZFMISC_1:28; hence op2 . ({},{}) = {} by FUNCT_2:50; ::_thesis: verum end; Lm2: for x, y being Element of 1 holds ( op2 . (x,y) = 0 iff x = y ) proof let x, y be Element of 1; ::_thesis: ( op2 . (x,y) = 0 iff x = y ) x = {} by CARD_1:49, TARSKI:def_1; hence ( op2 . (x,y) = 0 iff x = y ) by CARD_1:49, TARSKI:def_1; ::_thesis: verum end; Lm3: for x, y being Element of 1 holds op2 . (x,y) = op2 . (y,x) proof let x, y be Element of 1; ::_thesis: op2 . (x,y) = op2 . (y,x) ( x = {} & y = {} ) by CARD_1:49, TARSKI:def_1; hence op2 . (x,y) = op2 . (y,x) ; ::_thesis: verum end; registration cluster Empty^2-to-zero -> natural-valued for Function; coherence for b1 being Function st b1 = op2 holds b1 is natural-valued ; end; registration let f be natural-valued Function; let x, y be set ; clusterf . (x,y) -> natural ; coherence f . (x,y) is natural ; end; Lm4: for x, y, z being Element of 1 holds op2 . (x,z) <= (op2 . (x,y)) + (op2 . (y,z)) proof let x, y, z be Element of 1; ::_thesis: op2 . (x,z) <= (op2 . (x,y)) + (op2 . (y,z)) ( x = {} & y = {} ) by CARD_1:49, TARSKI:def_1; hence op2 . (x,z) <= (op2 . (x,y)) + (op2 . (y,z)) by Lm1; ::_thesis: verum end; definition let A be set ; let f be PartFunc of [:A,A:],REAL; attrf is Reflexive means :Def2: :: METRIC_1:def 2 for a being Element of A holds f . (a,a) = 0 ; attrf is discerning means :Def3: :: METRIC_1:def 3 for a, b being Element of A st f . (a,b) = 0 holds a = b; attrf is symmetric means :Def4: :: METRIC_1:def 4 for a, b being Element of A holds f . (a,b) = f . (b,a); attrf is triangle means :Def5: :: METRIC_1:def 5 for a, b, c being Element of A holds f . (a,c) <= (f . (a,b)) + (f . (b,c)); end; :: deftheorem Def2 defines Reflexive METRIC_1:def_2_:_ for A being set for f being PartFunc of [:A,A:],REAL holds ( f is Reflexive iff for a being Element of A holds f . (a,a) = 0 ); :: deftheorem Def3 defines discerning METRIC_1:def_3_:_ for A being set for f being PartFunc of [:A,A:],REAL holds ( f is discerning iff for a, b being Element of A st f . (a,b) = 0 holds a = b ); :: deftheorem Def4 defines symmetric METRIC_1:def_4_:_ for A being set for f being PartFunc of [:A,A:],REAL holds ( f is symmetric iff for a, b being Element of A holds f . (a,b) = f . (b,a) ); :: deftheorem Def5 defines triangle METRIC_1:def_5_:_ for A being set for f being PartFunc of [:A,A:],REAL holds ( f is triangle iff for a, b, c being Element of A holds f . (a,c) <= (f . (a,b)) + (f . (b,c)) ); definition let M be MetrStruct ; attrM is Reflexive means :Def6: :: METRIC_1:def 6 the distance of M is Reflexive ; attrM is discerning means :Def7: :: METRIC_1:def 7 the distance of M is discerning ; attrM is symmetric means :Def8: :: METRIC_1:def 8 the distance of M is symmetric ; attrM is triangle means :Def9: :: METRIC_1:def 9 the distance of M is triangle ; end; :: deftheorem Def6 defines Reflexive METRIC_1:def_6_:_ for M being MetrStruct holds ( M is Reflexive iff the distance of M is Reflexive ); :: deftheorem Def7 defines discerning METRIC_1:def_7_:_ for M being MetrStruct holds ( M is discerning iff the distance of M is discerning ); :: deftheorem Def8 defines symmetric METRIC_1:def_8_:_ for M being MetrStruct holds ( M is symmetric iff the distance of M is symmetric ); :: deftheorem Def9 defines triangle METRIC_1:def_9_:_ for M being MetrStruct holds ( M is triangle iff the distance of M is triangle ); registration cluster non empty strict Reflexive discerning symmetric triangle for MetrStruct ; existence ex b1 being MetrStruct st ( b1 is strict & b1 is Reflexive & b1 is discerning & b1 is symmetric & b1 is triangle & not b1 is empty ) proof reconsider M = MetrStruct(# 1,Empty^2-to-zero #) as non empty strict MetrStruct ; take M ; ::_thesis: ( M is strict & M is Reflexive & M is discerning & M is symmetric & M is triangle & not M is empty ) A1: the distance of M is discerning proof let a, b be Element of M; :: according to METRIC_1:def_3 ::_thesis: ( the distance of M . (a,b) = 0 implies a = b ) assume the distance of M . (a,b) = 0 ; ::_thesis: a = b hence a = b by Lm2; ::_thesis: verum end; A2: the distance of M is symmetric proof let a, b be Element of M; :: according to METRIC_1:def_4 ::_thesis: the distance of M . (a,b) = the distance of M . (b,a) thus the distance of M . (a,b) = the distance of M . (b,a) by Lm3; ::_thesis: verum end; A3: the distance of M is triangle proof let a, b, c be Element of M; :: according to METRIC_1:def_5 ::_thesis: the distance of M . (a,c) <= ( the distance of M . (a,b)) + ( the distance of M . (b,c)) thus the distance of M . (a,c) <= ( the distance of M . (a,b)) + ( the distance of M . (b,c)) by Lm4; ::_thesis: verum end; the distance of M is Reflexive proof let a be Element of M; :: according to METRIC_1:def_2 ::_thesis: the distance of M . (a,a) = 0 thus the distance of M . (a,a) = 0 by Lm2; ::_thesis: verum end; hence ( M is strict & M is Reflexive & M is discerning & M is symmetric & M is triangle & not M is empty ) by A1, A2, A3, Def6, Def7, Def8, Def9; ::_thesis: verum end; end; definition mode MetrSpace is Reflexive discerning symmetric triangle MetrStruct ; end; theorem Th1: :: METRIC_1:1 for M being MetrStruct holds ( ( for a being Element of M holds dist (a,a) = 0 ) iff M is Reflexive ) proof let M be MetrStruct ; ::_thesis: ( ( for a being Element of M holds dist (a,a) = 0 ) iff M is Reflexive ) hereby ::_thesis: ( M is Reflexive implies for a being Element of M holds dist (a,a) = 0 ) assume A1: for a being Element of M holds dist (a,a) = 0 ; ::_thesis: M is Reflexive the distance of M is Reflexive proof let a be Element of M; :: according to METRIC_1:def_2 ::_thesis: the distance of M . (a,a) = 0 the distance of M . (a,a) = dist (a,a) .= 0 by A1 ; hence the distance of M . (a,a) = 0 ; ::_thesis: verum end; hence M is Reflexive by Def6; ::_thesis: verum end; assume M is Reflexive ; ::_thesis: for a being Element of M holds dist (a,a) = 0 then the distance of M is Reflexive by Def6; hence for a being Element of M holds dist (a,a) = 0 by Def2; ::_thesis: verum end; theorem Th2: :: METRIC_1:2 for M being MetrStruct holds ( ( for a, b being Element of M st dist (a,b) = 0 holds a = b ) iff M is discerning ) proof let M be MetrStruct ; ::_thesis: ( ( for a, b being Element of M st dist (a,b) = 0 holds a = b ) iff M is discerning ) hereby ::_thesis: ( M is discerning implies for a, b being Element of M st dist (a,b) = 0 holds a = b ) assume A1: for a, b being Element of M st dist (a,b) = 0 holds a = b ; ::_thesis: M is discerning the distance of M is discerning proof let a, b be Element of M; :: according to METRIC_1:def_3 ::_thesis: ( the distance of M . (a,b) = 0 implies a = b ) assume the distance of M . (a,b) = 0 ; ::_thesis: a = b then dist (a,b) = 0 ; hence a = b by A1; ::_thesis: verum end; hence M is discerning by Def7; ::_thesis: verum end; assume M is discerning ; ::_thesis: for a, b being Element of M st dist (a,b) = 0 holds a = b then the distance of M is discerning by Def7; hence for a, b being Element of M st dist (a,b) = 0 holds a = b by Def3; ::_thesis: verum end; theorem Th3: :: METRIC_1:3 for M being MetrStruct st ( for a, b being Element of M holds dist (a,b) = dist (b,a) ) holds M is symmetric proof let M be MetrStruct ; ::_thesis: ( ( for a, b being Element of M holds dist (a,b) = dist (b,a) ) implies M is symmetric ) assume A1: for a, b being Element of M holds dist (a,b) = dist (b,a) ; ::_thesis: M is symmetric the distance of M is symmetric proof let a, b be Element of M; :: according to METRIC_1:def_4 ::_thesis: the distance of M . (a,b) = the distance of M . (b,a) thus the distance of M . (a,b) = dist (a,b) .= dist (b,a) by A1 .= the distance of M . (b,a) ; ::_thesis: verum end; hence M is symmetric by Def8; ::_thesis: verum end; theorem Th4: :: METRIC_1:4 for M being MetrStruct holds ( ( for a, b, c being Element of M holds dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) iff M is triangle ) proof let M be MetrStruct ; ::_thesis: ( ( for a, b, c being Element of M holds dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) iff M is triangle ) hereby ::_thesis: ( M is triangle implies for a, b, c being Element of M holds dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) assume A1: for a, b, c being Element of M holds dist (a,c) <= (dist (a,b)) + (dist (b,c)) ; ::_thesis: M is triangle the distance of M is triangle proof let a, b, c be Element of M; :: according to METRIC_1:def_5 ::_thesis: the distance of M . (a,c) <= ( the distance of M . (a,b)) + ( the distance of M . (b,c)) A2: the distance of M . (b,c) = dist (b,c) ; ( the distance of M . (a,b) = dist (a,b) & the distance of M . (a,c) = dist (a,c) ) ; hence the distance of M . (a,c) <= ( the distance of M . (a,b)) + ( the distance of M . (b,c)) by A1, A2; ::_thesis: verum end; hence M is triangle by Def9; ::_thesis: verum end; assume A3: M is triangle ; ::_thesis: for a, b, c being Element of M holds dist (a,c) <= (dist (a,b)) + (dist (b,c)) let a, b, c be Element of M; ::_thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c)) the distance of M is triangle by A3, Def9; hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) by Def5; ::_thesis: verum end; definition let M be symmetric MetrStruct ; let a, b be Element of M; :: original: dist redefine func dist (a,b) -> Real; commutativity for a, b being Element of M holds dist (a,b) = dist (b,a) proof the distance of M is symmetric by Def8; hence for a, b being Element of M holds dist (a,b) = dist (b,a) by Def4; ::_thesis: verum end; end; theorem Th5: :: METRIC_1:5 for M being Reflexive symmetric triangle MetrStruct for a, b being Element of M holds 0 <= dist (a,b) proof let M be Reflexive symmetric triangle MetrStruct ; ::_thesis: for a, b being Element of M holds 0 <= dist (a,b) let a, b be Element of M; ::_thesis: 0 <= dist (a,b) A1: (1 / 2) * (dist (a,a)) = (1 / 2) * 0 by Th1; ( dist (a,a) <= (dist (a,b)) + (dist (b,a)) & dist (a,b) = (1 / 2) * ((1 * (dist (a,b))) + (1 * (dist (a,b)))) ) by Th4; hence 0 <= dist (a,b) by A1, XREAL_1:64; ::_thesis: verum end; theorem Th6: :: METRIC_1:6 for M being MetrStruct st ( for a, b, c being Element of M holds ( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) ) holds M is MetrSpace proof let M be MetrStruct ; ::_thesis: ( ( for a, b, c being Element of M holds ( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) ) implies M is MetrSpace ) assume A1: for a, b, c being Element of M holds ( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) ; ::_thesis: M is MetrSpace A2: the distance of M is symmetric proof let a, b be Element of M; :: according to METRIC_1:def_4 ::_thesis: the distance of M . (a,b) = the distance of M . (b,a) the distance of M . (a,b) = dist (a,b) .= dist (b,a) by A1 .= the distance of M . (b,a) ; hence the distance of M . (a,b) = the distance of M . (b,a) ; ::_thesis: verum end; A3: the distance of M is triangle proof let a, b, c be Element of M; :: according to METRIC_1:def_5 ::_thesis: the distance of M . (a,c) <= ( the distance of M . (a,b)) + ( the distance of M . (b,c)) A4: the distance of M . (b,c) = dist (b,c) ; ( the distance of M . (a,c) = dist (a,c) & the distance of M . (a,b) = dist (a,b) ) ; hence the distance of M . (a,c) <= ( the distance of M . (a,b)) + ( the distance of M . (b,c)) by A1, A4; ::_thesis: verum end; A5: the distance of M is discerning proof let a, b be Element of M; :: according to METRIC_1:def_3 ::_thesis: ( the distance of M . (a,b) = 0 implies a = b ) assume the distance of M . (a,b) = 0 ; ::_thesis: a = b then dist (a,b) = 0 ; hence a = b by A1; ::_thesis: verum end; the distance of M is Reflexive proof let a be Element of M; :: according to METRIC_1:def_2 ::_thesis: the distance of M . (a,a) = 0 the distance of M . (a,a) = dist (a,a) .= 0 by A1 ; hence the distance of M . (a,a) = 0 ; ::_thesis: verum end; hence M is MetrSpace by A5, A2, A3, Def6, Def7, Def8, Def9; ::_thesis: verum end; theorem Th7: :: METRIC_1:7 for M being MetrSpace for x, y being Element of M st x <> y holds 0 < dist (x,y) proof let M be MetrSpace; ::_thesis: for x, y being Element of M st x <> y holds 0 < dist (x,y) let x, y be Element of M; ::_thesis: ( x <> y implies 0 < dist (x,y) ) A1: dist (x,y) >= 0 by Th5; assume x <> y ; ::_thesis: 0 < dist (x,y) then dist (x,y) <> 0 by Th2; hence 0 < dist (x,y) by A1, XXREAL_0:1; ::_thesis: verum end; definition let A be set ; func discrete_dist A -> Function of [:A,A:],REAL means :Def10: :: METRIC_1:def 10 for x, y being Element of A holds ( it . (x,x) = 0 & ( x <> y implies it . (x,y) = 1 ) ); existence ex b1 being Function of [:A,A:],REAL st for x, y being Element of A holds ( b1 . (x,x) = 0 & ( x <> y implies b1 . (x,y) = 1 ) ) proof percases ( A is empty or not A is empty ) ; supposeA1: A is empty ; ::_thesis: ex b1 being Function of [:A,A:],REAL st for x, y being Element of A holds ( b1 . (x,x) = 0 & ( x <> y implies b1 . (x,y) = 1 ) ) then [:A,A:] = {} by ZFMISC_1:90; then reconsider f = {} as Function of [:A,A:],REAL by RELSET_1:12; take f ; ::_thesis: for x, y being Element of A holds ( f . (x,x) = 0 & ( x <> y implies f . (x,y) = 1 ) ) let x, y be Element of A; ::_thesis: ( f . (x,x) = 0 & ( x <> y implies f . (x,y) = 1 ) ) thus f . (x,x) = 0 ; ::_thesis: ( x <> y implies f . (x,y) = 1 ) x = {} by A1, SUBSET_1:def_1 .= y by A1, SUBSET_1:def_1 ; hence ( x <> y implies f . (x,y) = 1 ) ; ::_thesis: verum end; supposeA2: not A is empty ; ::_thesis: ex b1 being Function of [:A,A:],REAL st for x, y being Element of A holds ( b1 . (x,x) = 0 & ( x <> y implies b1 . (x,y) = 1 ) ) ( {0,1} c= REAL & rng (chi (([:A,A:] \ (id A)),[:A,A:])) c= {0,1} ) by FUNCT_3:39, ZFMISC_1:32; then A3: rng (chi (([:A,A:] \ (id A)),[:A,A:])) c= REAL by XBOOLE_1:1; dom (chi (([:A,A:] \ (id A)),[:A,A:])) = [:A,A:] by FUNCT_3:def_3; then reconsider char = chi (([:A,A:] \ (id A)),[:A,A:]) as Function of [:A,A:],REAL by A3, RELSET_1:4; take char ; ::_thesis: for x, y being Element of A holds ( char . (x,x) = 0 & ( x <> y implies char . (x,y) = 1 ) ) let x, y be Element of A; ::_thesis: ( char . (x,x) = 0 & ( x <> y implies char . (x,y) = 1 ) ) [:A,A:] \ ([:A,A:] \ (id A)) = [:A,A:] /\ (id A) by XBOOLE_1:48 .= id A by XBOOLE_1:28 ; then [x,x] in [:A,A:] \ ([:A,A:] \ (id A)) by A2, RELAT_1:def_10; hence char . (x,x) = 0 by FUNCT_3:37; ::_thesis: ( x <> y implies char . (x,y) = 1 ) assume x <> y ; ::_thesis: char . (x,y) = 1 then A4: not [x,y] in id A by RELAT_1:def_10; [x,y] in [:A,A:] by A2, ZFMISC_1:def_2; then [x,y] in [:A,A:] \ (id A) by A4, XBOOLE_0:def_5; hence char . (x,y) = 1 by FUNCT_3:def_3; ::_thesis: verum end; end; end; uniqueness for b1, b2 being Function of [:A,A:],REAL st ( for x, y being Element of A holds ( b1 . (x,x) = 0 & ( x <> y implies b1 . (x,y) = 1 ) ) ) & ( for x, y being Element of A holds ( b2 . (x,x) = 0 & ( x <> y implies b2 . (x,y) = 1 ) ) ) holds b1 = b2 proof let f, f9 be Function of [:A,A:],REAL; ::_thesis: ( ( for x, y being Element of A holds ( f . (x,x) = 0 & ( x <> y implies f . (x,y) = 1 ) ) ) & ( for x, y being Element of A holds ( f9 . (x,x) = 0 & ( x <> y implies f9 . (x,y) = 1 ) ) ) implies f = f9 ) assume that A5: for x, y being Element of A holds ( f . (x,x) = 0 & ( x <> y implies f . (x,y) = 1 ) ) and A6: for x, y being Element of A holds ( f9 . (x,x) = 0 & ( x <> y implies f9 . (x,y) = 1 ) ) ; ::_thesis: f = f9 now__::_thesis:_for_x,_y_being_Element_of_A_holds_f_._(x,y)_=_f9_._(x,y) let x, y be Element of A; ::_thesis: f . (x,y) = f9 . (x,y) now__::_thesis:_f_._(x,y)_=_f9_._(x,y) percases ( x = y or x <> y ) ; supposeA7: x = y ; ::_thesis: f . (x,y) = f9 . (x,y) hence f . (x,y) = 0 by A5 .= f9 . (x,y) by A6, A7 ; ::_thesis: verum end; supposeA8: x <> y ; ::_thesis: f . (x,y) = f9 . (x,y) hence f . (x,y) = 1 by A5 .= f9 . (x,y) by A6, A8 ; ::_thesis: verum end; end; end; hence f . (x,y) = f9 . (x,y) ; ::_thesis: verum end; hence f = f9 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def10 defines discrete_dist METRIC_1:def_10_:_ for A being set for b2 being Function of [:A,A:],REAL holds ( b2 = discrete_dist A iff for x, y being Element of A holds ( b2 . (x,x) = 0 & ( x <> y implies b2 . (x,y) = 1 ) ) ); definition let A be set ; func DiscreteSpace A -> strict MetrStruct equals :: METRIC_1:def 11 MetrStruct(# A,(discrete_dist A) #); coherence MetrStruct(# A,(discrete_dist A) #) is strict MetrStruct ; end; :: deftheorem defines DiscreteSpace METRIC_1:def_11_:_ for A being set holds DiscreteSpace A = MetrStruct(# A,(discrete_dist A) #); registration let A be non empty set ; cluster DiscreteSpace A -> non empty strict ; coherence not DiscreteSpace A is empty ; end; registration let A be set ; cluster DiscreteSpace A -> strict Reflexive discerning symmetric triangle ; coherence ( DiscreteSpace A is Reflexive & DiscreteSpace A is discerning & DiscreteSpace A is symmetric & DiscreteSpace A is triangle ) proof set M = MetrStruct(# A,(discrete_dist A) #); A1: the distance of MetrStruct(# A,(discrete_dist A) #) is discerning proof let a, b be Element of MetrStruct(# A,(discrete_dist A) #); :: according to METRIC_1:def_3 ::_thesis: ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = 0 implies a = b ) assume the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = 0 ; ::_thesis: a = b hence a = b by Def10; ::_thesis: verum end; A2: the distance of MetrStruct(# A,(discrete_dist A) #) is symmetric proof let a, b be Element of MetrStruct(# A,(discrete_dist A) #); :: according to METRIC_1:def_4 ::_thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = the distance of MetrStruct(# A,(discrete_dist A) #) . (b,a) now__::_thesis:_the_distance_of_MetrStruct(#_A,(discrete_dist_A)_#)_._(a,b)_=_the_distance_of_MetrStruct(#_A,(discrete_dist_A)_#)_._(b,a) percases ( a <> b or a = b ) ; supposeA3: a <> b ; ::_thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = the distance of MetrStruct(# A,(discrete_dist A) #) . (b,a) hence the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = 1 by Def10 .= the distance of MetrStruct(# A,(discrete_dist A) #) . (b,a) by A3, Def10 ; ::_thesis: verum end; suppose a = b ; ::_thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = the distance of MetrStruct(# A,(discrete_dist A) #) . (b,a) hence the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = the distance of MetrStruct(# A,(discrete_dist A) #) . (b,a) ; ::_thesis: verum end; end; end; hence the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = the distance of MetrStruct(# A,(discrete_dist A) #) . (b,a) ; ::_thesis: verum end; A4: the distance of MetrStruct(# A,(discrete_dist A) #) is triangle proof let a, b, c be Element of MetrStruct(# A,(discrete_dist A) #); :: according to METRIC_1:def_5 ::_thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c)) A5: ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = 0 iff a = b ) by Def10; percases ( ( a = b & a = c ) or ( a = b & a <> c ) or ( a = c & a <> b ) or ( b = c & a <> c ) or ( a <> b & a <> c & b <> c ) ) ; suppose ( a = b & a = c ) ; ::_thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c)) hence the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c)) by A5; ::_thesis: verum end; suppose ( a = b & a <> c ) ; ::_thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c)) hence the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c)) by A5; ::_thesis: verum end; supposeA6: ( a = c & a <> b ) ; ::_thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c)) then A7: the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c) = 1 by Def10; ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) = 0 & the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = 1 ) by A6, Def10; hence the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c)) by A7; ::_thesis: verum end; supposeA8: ( b = c & a <> c ) ; ::_thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c)) then the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c) = 0 by Def10; hence the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c)) by A8; ::_thesis: verum end; supposeA9: ( a <> b & a <> c & b <> c ) ; ::_thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c)) then A10: the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c) = 1 by Def10; ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) = 1 & the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = 1 ) by A9, Def10; hence the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c)) by A10; ::_thesis: verum end; end; end; the distance of MetrStruct(# A,(discrete_dist A) #) is Reflexive proof let a be Element of MetrStruct(# A,(discrete_dist A) #); :: according to METRIC_1:def_2 ::_thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,a) = 0 thus the distance of MetrStruct(# A,(discrete_dist A) #) . (a,a) = 0 by Def10; ::_thesis: verum end; hence ( DiscreteSpace A is Reflexive & DiscreteSpace A is discerning & DiscreteSpace A is symmetric & DiscreteSpace A is triangle ) by A1, A2, A4, Def6, Def7, Def8, Def9; ::_thesis: verum end; end; definition func real_dist -> Function of [:REAL,REAL:],REAL means :Def12: :: METRIC_1:def 12 for x, y being Element of REAL holds it . (x,y) = abs (x - y); existence ex b1 being Function of [:REAL,REAL:],REAL st for x, y being Element of REAL holds b1 . (x,y) = abs (x - y) proof deffunc H1( Element of REAL , Element of REAL ) -> Element of REAL = abs (\$1 - \$2); consider F being Function of [:REAL,REAL:],REAL such that A1: for x, y being Element of REAL holds F . (x,y) = H1(x,y) from BINOP_1:sch_4(); take F ; ::_thesis: for x, y being Element of REAL holds F . (x,y) = abs (x - y) let x, y be Element of REAL ; ::_thesis: F . (x,y) = abs (x - y) thus F . (x,y) = abs (x - y) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of [:REAL,REAL:],REAL st ( for x, y being Element of REAL holds b1 . (x,y) = abs (x - y) ) & ( for x, y being Element of REAL holds b2 . (x,y) = abs (x - y) ) holds b1 = b2 proof let F1, F2 be Function of [:REAL,REAL:],REAL; ::_thesis: ( ( for x, y being Element of REAL holds F1 . (x,y) = abs (x - y) ) & ( for x, y being Element of REAL holds F2 . (x,y) = abs (x - y) ) implies F1 = F2 ) assume that A2: for x, y being Element of REAL holds F1 . (x,y) = abs (x - y) and A3: for x, y being Element of REAL holds F2 . (x,y) = abs (x - y) ; ::_thesis: F1 = F2 for x, y being Element of REAL holds F1 . (x,y) = F2 . (x,y) proof let x, y be Element of REAL ; ::_thesis: F1 . (x,y) = F2 . (x,y) thus F1 . (x,y) = abs (x - y) by A2 .= F2 . (x,y) by A3 ; ::_thesis: verum end; hence F1 = F2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def12 defines real_dist METRIC_1:def_12_:_ for b1 being Function of [:REAL,REAL:],REAL holds ( b1 = real_dist iff for x, y being Element of REAL holds b1 . (x,y) = abs (x - y) ); theorem Th8: :: METRIC_1:8 for x, y being Element of REAL holds ( real_dist . (x,y) = 0 iff x = y ) proof let x, y be Element of REAL ; ::_thesis: ( real_dist . (x,y) = 0 iff x = y ) thus ( real_dist . (x,y) = 0 implies x = y ) ::_thesis: ( x = y implies real_dist . (x,y) = 0 ) proof assume real_dist . (x,y) = 0 ; ::_thesis: x = y then 0 = abs (x - y) by Def12; then x - y = 0 by ABSVALUE:2; hence x = y ; ::_thesis: verum end; assume x = y ; ::_thesis: real_dist . (x,y) = 0 then abs (x - y) = 0 by ABSVALUE:2; hence real_dist . (x,y) = 0 by Def12; ::_thesis: verum end; theorem Th9: :: METRIC_1:9 for x, y being Element of REAL holds real_dist . (x,y) = real_dist . (y,x) proof let x, y be Element of REAL ; ::_thesis: real_dist . (x,y) = real_dist . (y,x) thus real_dist . (x,y) = abs (x - y) by Def12 .= abs (- (x - y)) by COMPLEX1:52 .= abs (y - x) .= real_dist . (y,x) by Def12 ; ::_thesis: verum end; theorem Th10: :: METRIC_1:10 for x, y, z being Element of REAL holds real_dist . (x,y) <= (real_dist . (x,z)) + (real_dist . (z,y)) proof let x, y, z be Element of REAL ; ::_thesis: real_dist . (x,y) <= (real_dist . (x,z)) + (real_dist . (z,y)) abs (x - y) = abs ((x - z) + (z - y)) ; then A1: abs (x - y) <= (abs (x - z)) + (abs (z - y)) by COMPLEX1:56; ( real_dist . (x,y) = abs (x - y) & real_dist . (x,z) = abs (x - z) ) by Def12; hence real_dist . (x,y) <= (real_dist . (x,z)) + (real_dist . (z,y)) by A1, Def12; ::_thesis: verum end; definition func RealSpace -> strict MetrStruct equals :: METRIC_1:def 13 MetrStruct(# REAL,real_dist #); coherence MetrStruct(# REAL,real_dist #) is strict MetrStruct ; end; :: deftheorem defines RealSpace METRIC_1:def_13_:_ RealSpace = MetrStruct(# REAL,real_dist #); registration cluster RealSpace -> non empty strict ; coherence not RealSpace is empty ; end; registration cluster RealSpace -> strict Reflexive discerning symmetric triangle ; coherence ( RealSpace is Reflexive & RealSpace is discerning & RealSpace is symmetric & RealSpace is triangle ) proof reconsider M = MetrStruct(# REAL,real_dist #) as non empty MetrStruct ; for a, b, c being Element of M holds ( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) by Th8, Th9, Th10; hence ( RealSpace is Reflexive & RealSpace is discerning & RealSpace is symmetric & RealSpace is triangle ) by Th6; ::_thesis: verum end; end; definition let M be MetrStruct ; let p be Element of M; let r be real number ; func Ball (p,r) -> Subset of M means :Def14: :: METRIC_1:def 14 it = { q where q is Element of M : dist (p,q) < r } if not M is empty otherwise it is empty ; existence ( ( not M is empty implies ex b1 being Subset of M st b1 = { q where q is Element of M : dist (p,q) < r } ) & ( M is empty implies ex b1 being Subset of M st b1 is empty ) ) proof reconsider X = {} as Subset of M by XBOOLE_1:2; thus ( not M is empty implies ex X being Subset of M st X = { q where q is Element of M : dist (p,q) < r } ) ::_thesis: ( M is empty implies ex b1 being Subset of M st b1 is empty ) proof assume not M is empty ; ::_thesis: ex X being Subset of M st X = { q where q is Element of M : dist (p,q) < r } then reconsider M9 = M as non empty MetrStruct ; reconsider p9 = p as Element of M9 ; defpred S1[ Element of M9] means dist (p9,\$1) < r; set X = { q where q is Element of M9 : S1[q] } ; { q where q is Element of M9 : S1[q] } c= the carrier of M9 from FRAENKEL:sch_10(); then reconsider X = { q where q is Element of M9 : S1[q] } as Subset of M ; take X ; ::_thesis: X = { q where q is Element of M : dist (p,q) < r } thus X = { q where q is Element of M : dist (p,q) < r } ; ::_thesis: verum end; assume M is empty ; ::_thesis: ex b1 being Subset of M st b1 is empty take X ; ::_thesis: X is empty thus X is empty ; ::_thesis: verum end; correctness consistency for b1 being Subset of M holds verum; uniqueness for b1, b2 being Subset of M holds ( ( not M is empty & b1 = { q where q is Element of M : dist (p,q) < r } & b2 = { q where q is Element of M : dist (p,q) < r } implies b1 = b2 ) & ( M is empty & b1 is empty & b2 is empty implies b1 = b2 ) ); ; end; :: deftheorem Def14 defines Ball METRIC_1:def_14_:_ for M being MetrStruct for p being Element of M for r being real number for b4 being Subset of M holds ( ( not M is empty implies ( b4 = Ball (p,r) iff b4 = { q where q is Element of M : dist (p,q) < r } ) ) & ( M is empty implies ( b4 = Ball (p,r) iff b4 is empty ) ) ); definition let M be MetrStruct ; let p be Element of M; let r be real number ; func cl_Ball (p,r) -> Subset of M means :Def15: :: METRIC_1:def 15 it = { q where q is Element of M : dist (p,q) <= r } if not M is empty otherwise it is empty ; existence ( ( not M is empty implies ex b1 being Subset of M st b1 = { q where q is Element of M : dist (p,q) <= r } ) & ( M is empty implies ex b1 being Subset of M st b1 is empty ) ) proof reconsider X = {} as Subset of M by XBOOLE_1:2; thus ( not M is empty implies ex X being Subset of M st X = { q where q is Element of M : dist (p,q) <= r } ) ::_thesis: ( M is empty implies ex b1 being Subset of M st b1 is empty ) proof assume not M is empty ; ::_thesis: ex X being Subset of M st X = { q where q is Element of M : dist (p,q) <= r } then reconsider M9 = M as non empty MetrStruct ; reconsider p9 = p as Element of M9 ; defpred S1[ Element of M9] means dist (p9,\$1) <= r; set X = { q where q is Element of M9 : S1[q] } ; { q where q is Element of M9 : S1[q] } c= the carrier of M9 from FRAENKEL:sch_10(); then reconsider X = { q where q is Element of M9 : S1[q] } as Subset of M ; take X ; ::_thesis: X = { q where q is Element of M : dist (p,q) <= r } thus X = { q where q is Element of M : dist (p,q) <= r } ; ::_thesis: verum end; assume M is empty ; ::_thesis: ex b1 being Subset of M st b1 is empty take X ; ::_thesis: X is empty thus X is empty ; ::_thesis: verum end; correctness consistency for b1 being Subset of M holds verum; uniqueness for b1, b2 being Subset of M holds ( ( not M is empty & b1 = { q where q is Element of M : dist (p,q) <= r } & b2 = { q where q is Element of M : dist (p,q) <= r } implies b1 = b2 ) & ( M is empty & b1 is empty & b2 is empty implies b1 = b2 ) ); ; end; :: deftheorem Def15 defines cl_Ball METRIC_1:def_15_:_ for M being MetrStruct for p being Element of M for r being real number for b4 being Subset of M holds ( ( not M is empty implies ( b4 = cl_Ball (p,r) iff b4 = { q where q is Element of M : dist (p,q) <= r } ) ) & ( M is empty implies ( b4 = cl_Ball (p,r) iff b4 is empty ) ) ); definition let M be MetrStruct ; let p be Element of M; let r be real number ; func Sphere (p,r) -> Subset of M means :Def16: :: METRIC_1:def 16 it = { q where q is Element of M : dist (p,q) = r } if not M is empty otherwise it is empty ; existence ( ( not M is empty implies ex b1 being Subset of M st b1 = { q where q is Element of M : dist (p,q) = r } ) & ( M is empty implies ex b1 being Subset of M st b1 is empty ) ) proof reconsider X = {} as Subset of M by XBOOLE_1:2; thus ( not M is empty implies ex X being Subset of M st X = { q where q is Element of M : dist (p,q) = r } ) ::_thesis: ( M is empty implies ex b1 being Subset of M st b1 is empty ) proof assume not M is empty ; ::_thesis: ex X being Subset of M st X = { q where q is Element of M : dist (p,q) = r } then reconsider M9 = M as non empty MetrStruct ; reconsider p9 = p as Element of M9 ; defpred S1[ Element of M9] means dist (p9,\$1) = r; set X = { q where q is Element of M9 : S1[q] } ; { q where q is Element of M9 : S1[q] } c= the carrier of M9 from FRAENKEL:sch_10(); then reconsider X = { q where q is Element of M9 : S1[q] } as Subset of M ; take X ; ::_thesis: X = { q where q is Element of M : dist (p,q) = r } thus X = { q where q is Element of M : dist (p,q) = r } ; ::_thesis: verum end; assume M is empty ; ::_thesis: ex b1 being Subset of M st b1 is empty take X ; ::_thesis: X is empty thus X is empty ; ::_thesis: verum end; correctness consistency for b1 being Subset of M holds verum; uniqueness for b1, b2 being Subset of M holds ( ( not M is empty & b1 = { q where q is Element of M : dist (p,q) = r } & b2 = { q where q is Element of M : dist (p,q) = r } implies b1 = b2 ) & ( M is empty & b1 is empty & b2 is empty implies b1 = b2 ) ); ; end; :: deftheorem Def16 defines Sphere METRIC_1:def_16_:_ for M being MetrStruct for p being Element of M for r being real number for b4 being Subset of M holds ( ( not M is empty implies ( b4 = Sphere (p,r) iff b4 = { q where q is Element of M : dist (p,q) = r } ) ) & ( M is empty implies ( b4 = Sphere (p,r) iff b4 is empty ) ) ); theorem Th11: :: METRIC_1:11 for r being real number for M being MetrStruct for p, x being Element of M holds ( x in Ball (p,r) iff ( not M is empty & dist (p,x) < r ) ) proof let r be real number ; ::_thesis: for M being MetrStruct for p, x being Element of M holds ( x in Ball (p,r) iff ( not M is empty & dist (p,x) < r ) ) let M be MetrStruct ; ::_thesis: for p, x being Element of M holds ( x in Ball (p,r) iff ( not M is empty & dist (p,x) < r ) ) let p, x be Element of M; ::_thesis: ( x in Ball (p,r) iff ( not M is empty & dist (p,x) < r ) ) hereby ::_thesis: ( not M is empty & dist (p,x) < r implies x in Ball (p,r) ) assume A1: x in Ball (p,r) ; ::_thesis: ( not M is empty & dist (p,x) < r ) then reconsider M9 = M as non empty MetrStruct ; reconsider p9 = p as Element of M9 ; x in { q where q is Element of M9 : dist (p9,q) < r } by A1, Def14; then ex q being Element of M st ( x = q & dist (p,q) < r ) ; hence ( not M is empty & dist (p,x) < r ) by A1; ::_thesis: verum end; assume not M is empty ; ::_thesis: ( not dist (p,x) < r or x in Ball (p,r) ) then reconsider M9 = M as non empty MetrStruct ; reconsider p9 = p as Element of M9 ; assume dist (p,x) < r ; ::_thesis: x in Ball (p,r) then x in { q where q is Element of M9 : dist (p9,q) < r } ; hence x in Ball (p,r) by Def14; ::_thesis: verum end; theorem Th12: :: METRIC_1:12 for r being real number for M being MetrStruct for p, x being Element of M holds ( x in cl_Ball (p,r) iff ( not M is empty & dist (p,x) <= r ) ) proof let r be real number ; ::_thesis: for M being MetrStruct for p, x being Element of M holds ( x in cl_Ball (p,r) iff ( not M is empty & dist (p,x) <= r ) ) let M be MetrStruct ; ::_thesis: for p, x being Element of M holds ( x in cl_Ball (p,r) iff ( not M is empty & dist (p,x) <= r ) ) let p, x be Element of M; ::_thesis: ( x in cl_Ball (p,r) iff ( not M is empty & dist (p,x) <= r ) ) hereby ::_thesis: ( not M is empty & dist (p,x) <= r implies x in cl_Ball (p,r) ) assume A1: x in cl_Ball (p,r) ; ::_thesis: ( not M is empty & dist (p,x) <= r ) then reconsider M9 = M as non empty MetrStruct ; reconsider p9 = p as Element of M9 ; x in { q where q is Element of M9 : dist (p9,q) <= r } by A1, Def15; then ex q being Element of M st ( x = q & dist (p,q) <= r ) ; hence ( not M is empty & dist (p,x) <= r ) by A1; ::_thesis: verum end; assume not M is empty ; ::_thesis: ( not dist (p,x) <= r or x in cl_Ball (p,r) ) then reconsider M9 = M as non empty MetrStruct ; reconsider p9 = p as Element of M9 ; assume dist (p,x) <= r ; ::_thesis: x in cl_Ball (p,r) then x in { q where q is Element of M9 : dist (p9,q) <= r } ; hence x in cl_Ball (p,r) by Def15; ::_thesis: verum end; theorem Th13: :: METRIC_1:13 for r being real number for M being MetrStruct for p, x being Element of M holds ( x in Sphere (p,r) iff ( not M is empty & dist (p,x) = r ) ) proof let r be real number ; ::_thesis: for M being MetrStruct for p, x being Element of M holds ( x in Sphere (p,r) iff ( not M is empty & dist (p,x) = r ) ) let M be MetrStruct ; ::_thesis: for p, x being Element of M holds ( x in Sphere (p,r) iff ( not M is empty & dist (p,x) = r ) ) let p, x be Element of M; ::_thesis: ( x in Sphere (p,r) iff ( not M is empty & dist (p,x) = r ) ) hereby ::_thesis: ( not M is empty & dist (p,x) = r implies x in Sphere (p,r) ) assume A1: x in Sphere (p,r) ; ::_thesis: ( not M is empty & dist (p,x) = r ) then reconsider M9 = M as non empty MetrStruct ; reconsider p9 = p as Element of M9 ; x in { q where q is Element of M9 : dist (p9,q) = r } by A1, Def16; then ex q being Element of M st ( x = q & dist (p,q) = r ) ; hence ( not M is empty & dist (p,x) = r ) by A1; ::_thesis: verum end; assume not M is empty ; ::_thesis: ( not dist (p,x) = r or x in Sphere (p,r) ) then reconsider M9 = M as non empty MetrStruct ; reconsider p9 = p as Element of M9 ; assume dist (p,x) = r ; ::_thesis: x in Sphere (p,r) then x in { q where q is Element of M9 : dist (p9,q) = r } ; hence x in Sphere (p,r) by Def16; ::_thesis: verum end; theorem Th14: :: METRIC_1:14 for r being real number for M being MetrStruct for p being Element of M holds Ball (p,r) c= cl_Ball (p,r) proof let r be real number ; ::_thesis: for M being MetrStruct for p being Element of M holds Ball (p,r) c= cl_Ball (p,r) let M be MetrStruct ; ::_thesis: for p being Element of M holds Ball (p,r) c= cl_Ball (p,r) let p be Element of M; ::_thesis: Ball (p,r) c= cl_Ball (p,r) percases ( not M is empty or M is empty ) ; supposeA1: not M is empty ; ::_thesis: Ball (p,r) c= cl_Ball (p,r) now__::_thesis:_for_x_being_Element_of_M_st_x_in_Ball_(p,r)_holds_ x_in_cl_Ball_(p,r) let x be Element of M; ::_thesis: ( x in Ball (p,r) implies x in cl_Ball (p,r) ) assume x in Ball (p,r) ; ::_thesis: x in cl_Ball (p,r) then dist (p,x) <= r by Th11; then x in { q where q is Element of M : dist (p,q) <= r } ; hence x in cl_Ball (p,r) by A1, Def15; ::_thesis: verum end; hence Ball (p,r) c= cl_Ball (p,r) by SUBSET_1:2; ::_thesis: verum end; supposeA2: M is empty ; ::_thesis: Ball (p,r) c= cl_Ball (p,r) then Ball (p,r) is empty by Def14; hence Ball (p,r) c= cl_Ball (p,r) by A2, Def15; ::_thesis: verum end; end; end; theorem Th15: :: METRIC_1:15 for r being real number for M being MetrStruct for p being Element of M holds Sphere (p,r) c= cl_Ball (p,r) proof let r be real number ; ::_thesis: for M being MetrStruct for p being Element of M holds Sphere (p,r) c= cl_Ball (p,r) let M be MetrStruct ; ::_thesis: for p being Element of M holds Sphere (p,r) c= cl_Ball (p,r) let p be Element of M; ::_thesis: Sphere (p,r) c= cl_Ball (p,r) percases ( not M is empty or M is empty ) ; supposeA1: not M is empty ; ::_thesis: Sphere (p,r) c= cl_Ball (p,r) now__::_thesis:_for_x_being_Element_of_M_st_x_in_Sphere_(p,r)_holds_ x_in_cl_Ball_(p,r) let x be Element of M; ::_thesis: ( x in Sphere (p,r) implies x in cl_Ball (p,r) ) assume x in Sphere (p,r) ; ::_thesis: x in cl_Ball (p,r) then dist (p,x) = r by Th13; then x in { q where q is Element of M : dist (p,q) <= r } ; hence x in cl_Ball (p,r) by Def15, A1; ::_thesis: verum end; hence Sphere (p,r) c= cl_Ball (p,r) by SUBSET_1:2; ::_thesis: verum end; supposeA2: M is empty ; ::_thesis: Sphere (p,r) c= cl_Ball (p,r) then Sphere (p,r) is empty by Def16; hence Sphere (p,r) c= cl_Ball (p,r) by A2, Def15; ::_thesis: verum end; end; end; theorem :: METRIC_1:16 for r being real number for M being MetrStruct for p being Element of M holds (Sphere (p,r)) \/ (Ball (p,r)) = cl_Ball (p,r) proof let r be real number ; ::_thesis: for M being MetrStruct for p being Element of M holds (Sphere (p,r)) \/ (Ball (p,r)) = cl_Ball (p,r) let M be MetrStruct ; ::_thesis: for p being Element of M holds (Sphere (p,r)) \/ (Ball (p,r)) = cl_Ball (p,r) let p be Element of M; ::_thesis: (Sphere (p,r)) \/ (Ball (p,r)) = cl_Ball (p,r) ( Sphere (p,r) c= cl_Ball (p,r) & Ball (p,r) c= cl_Ball (p,r) ) by Th14, Th15; hence (Sphere (p,r)) \/ (Ball (p,r)) c= cl_Ball (p,r) by XBOOLE_1:8; :: according to XBOOLE_0:def_10 ::_thesis: cl_Ball (p,r) c= (Sphere (p,r)) \/ (Ball (p,r)) percases ( not M is empty or M is empty ) ; supposeA1: not M is empty ; ::_thesis: cl_Ball (p,r) c= (Sphere (p,r)) \/ (Ball (p,r)) now__::_thesis:_for_x_being_Element_of_M_st_x_in_cl_Ball_(p,r)_holds_ x_in_(Sphere_(p,r))_\/_(Ball_(p,r)) let x be Element of M; ::_thesis: ( x in cl_Ball (p,r) implies x in (Sphere (p,r)) \/ (Ball (p,r)) ) assume x in cl_Ball (p,r) ; ::_thesis: x in (Sphere (p,r)) \/ (Ball (p,r)) then A2: dist (p,x) <= r by Th12; now__::_thesis:_(_(_dist_(p,x)_<_r_&_x_in_Ball_(p,r)_)_or_(_dist_(p,x)_=_r_&_x_in_Sphere_(p,r)_)_) percases ( dist (p,x) < r or dist (p,x) = r ) by A2, XXREAL_0:1; case dist (p,x) < r ; ::_thesis: x in Ball (p,r) hence x in Ball (p,r) by A1, Th11; ::_thesis: verum end; case dist (p,x) = r ; ::_thesis: x in Sphere (p,r) hence x in Sphere (p,r) by A1, Th13; ::_thesis: verum end; end; end; hence x in (Sphere (p,r)) \/ (Ball (p,r)) by XBOOLE_0:def_3; ::_thesis: verum end; hence cl_Ball (p,r) c= (Sphere (p,r)) \/ (Ball (p,r)) by SUBSET_1:2; ::_thesis: verum end; supposeA3: M is empty ; ::_thesis: cl_Ball (p,r) c= (Sphere (p,r)) \/ (Ball (p,r)) then ( Ball (p,r) is empty & cl_Ball (p,r) is empty ) by Def14, Def15; hence cl_Ball (p,r) c= (Sphere (p,r)) \/ (Ball (p,r)) by A3, Def16; ::_thesis: verum end; end; end; theorem :: METRIC_1:17 for r being real number for M being non empty MetrStruct for p being Element of M holds Ball (p,r) = { q where q is Element of M : dist (p,q) < r } by Def14; theorem :: METRIC_1:18 for r being real number for M being non empty MetrStruct for p being Element of M holds cl_Ball (p,r) = { q where q is Element of M : dist (p,q) <= r } by Def15; theorem :: METRIC_1:19 for r being real number for M being non empty MetrStruct for p being Element of M holds Sphere (p,r) = { q where q is Element of M : dist (p,q) = r } by Def16; begin theorem :: METRIC_1:20 for x being set holds Empty^2-to-zero . (x,x) = 0 proof let x be set ; ::_thesis: Empty^2-to-zero . (x,x) = 0 percases ( [x,x] in [:1,1:] or not [x,x] in [:1,1:] ) ; suppose [x,x] in [:1,1:] ; ::_thesis: Empty^2-to-zero . (x,x) = 0 hence Empty^2-to-zero . (x,x) = 0 by CARD_1:49, FUNCT_2:50; ::_thesis: verum end; suppose not [x,x] in [:1,1:] ; ::_thesis: Empty^2-to-zero . (x,x) = 0 then not [x,x] in dom Empty^2-to-zero by FUNCT_2:def_1; hence Empty^2-to-zero . (x,x) = 0 by FUNCT_1:def_2; ::_thesis: verum end; end; end; theorem Th21: :: METRIC_1:21 for x, y being Element of 1 st x <> y holds 0 < Empty^2-to-zero . (x,y) proof let x, y be Element of 1; ::_thesis: ( x <> y implies 0 < Empty^2-to-zero . (x,y) ) x = {} by CARD_1:49, TARSKI:def_1; hence ( x <> y implies 0 < Empty^2-to-zero . (x,y) ) by CARD_1:49, TARSKI:def_1; ::_thesis: verum end; theorem Th22: :: METRIC_1:22 for x, y being Element of 1 holds Empty^2-to-zero . (x,y) = Empty^2-to-zero . (y,x) by Lm3; theorem Th23: :: METRIC_1:23 for x, y, z being Element of 1 holds Empty^2-to-zero . (x,z) <= (Empty^2-to-zero . (x,y)) + (Empty^2-to-zero . (y,z)) by Lm4; theorem Th24: :: METRIC_1:24 for x, y, z being Element of 1 holds Empty^2-to-zero . (x,z) <= max ((Empty^2-to-zero . (x,y)),(Empty^2-to-zero . (y,z))) proof let x, y, z be Element of 1; ::_thesis: Empty^2-to-zero . (x,z) <= max ((Empty^2-to-zero . (x,y)),(Empty^2-to-zero . (y,z))) A1: z = {} by CARD_1:49, TARSKI:def_1; ( x = {} & y = {} ) by CARD_1:49, TARSKI:def_1; hence Empty^2-to-zero . (x,z) <= max ((Empty^2-to-zero . (x,y)),(Empty^2-to-zero . (y,z))) by A1; ::_thesis: verum end; set M0 = MetrStruct(# 1,Empty^2-to-zero #); definition let A be non empty set ; let f be Function of [:A,A:],REAL; attrf is Discerning means :Def17: :: METRIC_1:def 17 for a, b being Element of A st a <> b holds 0 < f . (a,b); end; :: deftheorem Def17 defines Discerning METRIC_1:def_17_:_ for A being non empty set for f being Function of [:A,A:],REAL holds ( f is Discerning iff for a, b being Element of A st a <> b holds 0 < f . (a,b) ); definition let M be non empty MetrStruct ; attrM is Discerning means :Def18: :: METRIC_1:def 18 the distance of M is Discerning ; end; :: deftheorem Def18 defines Discerning METRIC_1:def_18_:_ for M being non empty MetrStruct holds ( M is Discerning iff the distance of M is Discerning ); theorem Th25: :: METRIC_1:25 for M being non empty MetrStruct holds ( ( for a, b being Element of M st a <> b holds 0 < dist (a,b) ) iff M is Discerning ) proof let M be non empty MetrStruct ; ::_thesis: ( ( for a, b being Element of M st a <> b holds 0 < dist (a,b) ) iff M is Discerning ) hereby ::_thesis: ( M is Discerning implies for a, b being Element of M st a <> b holds 0 < dist (a,b) ) assume A1: for a, b being Element of M st a <> b holds 0 < dist (a,b) ; ::_thesis: M is Discerning the distance of M is Discerning proof let a, b be Element of M; :: according to METRIC_1:def_17 ::_thesis: ( a <> b implies 0 < the distance of M . (a,b) ) assume a <> b ; ::_thesis: 0 < the distance of M . (a,b) then 0 < dist (a,b) by A1; hence 0 < the distance of M . (a,b) ; ::_thesis: verum end; hence M is Discerning by Def18; ::_thesis: verum end; assume M is Discerning ; ::_thesis: for a, b being Element of M st a <> b holds 0 < dist (a,b) then the distance of M is Discerning by Def18; hence for a, b being Element of M st a <> b holds 0 < dist (a,b) by Def17; ::_thesis: verum end; registration cluster MetrStruct(# 1,Empty^2-to-zero #) -> non empty ; coherence not MetrStruct(# 1,Empty^2-to-zero #) is empty ; end; registration cluster MetrStruct(# 1,Empty^2-to-zero #) -> Reflexive symmetric triangle Discerning ; coherence ( MetrStruct(# 1,Empty^2-to-zero #) is Reflexive & MetrStruct(# 1,Empty^2-to-zero #) is symmetric & MetrStruct(# 1,Empty^2-to-zero #) is Discerning & MetrStruct(# 1,Empty^2-to-zero #) is triangle ) proof A1: for x being Element of MetrStruct(# 1,Empty^2-to-zero #) holds dist (x,x) = 0 by Lm2; A2: for x, y being Element of MetrStruct(# 1,Empty^2-to-zero #) holds dist (x,y) = dist (y,x) by Th22; A3: for x, y being Element of MetrStruct(# 1,Empty^2-to-zero #) st x <> y holds 0 < dist (x,y) by Th21; for x, y, z being Element of MetrStruct(# 1,Empty^2-to-zero #) holds dist (x,z) <= (dist (x,y)) + (dist (y,z)) by Th23; hence ( MetrStruct(# 1,Empty^2-to-zero #) is Reflexive & MetrStruct(# 1,Empty^2-to-zero #) is symmetric & MetrStruct(# 1,Empty^2-to-zero #) is Discerning & MetrStruct(# 1,Empty^2-to-zero #) is triangle ) by A2, A1, A3, Th25, Th1, Th3, Th4; ::_thesis: verum end; end; definition let M be non empty MetrStruct ; attrM is ultra means :Def19: :: METRIC_1:def 19 for a, b, c being Element of M holds dist (a,c) <= max ((dist (a,b)),(dist (b,c))); end; :: deftheorem Def19 defines ultra METRIC_1:def_19_:_ for M being non empty MetrStruct holds ( M is ultra iff for a, b, c being Element of M holds dist (a,c) <= max ((dist (a,b)),(dist (b,c))) ); registration cluster non empty strict Reflexive symmetric triangle Discerning ultra for MetrStruct ; existence ex b1 being non empty MetrStruct st ( b1 is strict & b1 is ultra & b1 is Reflexive & b1 is symmetric & b1 is Discerning & b1 is triangle ) proof take M0 = MetrStruct(# 1,Empty^2-to-zero #); ::_thesis: ( M0 is strict & M0 is ultra & M0 is Reflexive & M0 is symmetric & M0 is Discerning & M0 is triangle ) M0 is ultra proof let x, y, z be Element of M0; :: according to METRIC_1:def_19 ::_thesis: dist (x,z) <= max ((dist (x,y)),(dist (y,z))) thus dist (x,z) <= max ((dist (x,y)),(dist (y,z))) by Th24; ::_thesis: verum end; hence ( M0 is strict & M0 is ultra & M0 is Reflexive & M0 is symmetric & M0 is Discerning & M0 is triangle ) ; ::_thesis: verum end; end; theorem Th26: :: METRIC_1:26 for M being non empty Reflexive Discerning MetrStruct for a, b being Element of M holds 0 <= dist (a,b) proof let M be non empty Reflexive Discerning MetrStruct ; ::_thesis: for a, b being Element of M holds 0 <= dist (a,b) let a, b be Element of M; ::_thesis: 0 <= dist (a,b) now__::_thesis:_0_<=_dist_(a,b) percases ( a = b or a <> b ) ; suppose a = b ; ::_thesis: 0 <= dist (a,b) hence 0 <= dist (a,b) by Th1; ::_thesis: verum end; suppose a <> b ; ::_thesis: 0 <= dist (a,b) hence 0 <= dist (a,b) by Th25; ::_thesis: verum end; end; end; hence 0 <= dist (a,b) ; ::_thesis: verum end; definition mode PseudoMetricSpace is non empty Reflexive symmetric triangle MetrStruct ; mode SemiMetricSpace is non empty Reflexive symmetric Discerning MetrStruct ; mode NonSymmetricMetricSpace is non empty Reflexive triangle Discerning MetrStruct ; mode UltraMetricSpace is non empty Reflexive symmetric Discerning ultra MetrStruct ; end; registration cluster non empty Reflexive discerning symmetric triangle -> non empty Discerning for MetrStruct ; coherence for b1 being non empty MetrSpace holds b1 is Discerning proof let M be non empty MetrSpace; ::_thesis: M is Discerning for a, b being Element of M st a <> b holds 0 < dist (a,b) by Th7; hence M is Discerning by Th25; ::_thesis: verum end; end; registration cluster non empty Reflexive symmetric Discerning ultra -> discerning triangle for MetrStruct ; coherence for b1 being UltraMetricSpace holds ( b1 is triangle & b1 is discerning ) proof let M be UltraMetricSpace; ::_thesis: ( M is triangle & M is discerning ) now__::_thesis:_for_x,_y,_z_being_Element_of_M_holds_ (_(_dist_(x,y)_=_0_implies_x_=_y_)_&_(_x_=_y_implies_dist_(x,y)_=_0_)_&_dist_(x,y)_=_dist_(y,x)_&_dist_(x,z)_<=_(dist_(x,y))_+_(dist_(y,z))_) let x, y, z be Element of M; ::_thesis: ( ( dist (x,y) = 0 implies x = y ) & ( x = y implies dist (x,y) = 0 ) & dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) ) thus ( dist (x,y) = 0 iff x = y ) by Th25, Th1; ::_thesis: ( dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) ) thus dist (x,y) = dist (y,x) ; ::_thesis: dist (x,z) <= (dist (x,y)) + (dist (y,z)) ( 0 <= dist (x,y) & 0 <= dist (y,z) ) by Th26; then A1: max ((dist (x,y)),(dist (y,z))) <= (dist (x,y)) + (dist (y,z)) by SQUARE_1:2; dist (x,z) <= max ((dist (x,y)),(dist (y,z))) by Def19; hence dist (x,z) <= (dist (x,y)) + (dist (y,z)) by A1, XXREAL_0:2; ::_thesis: verum end; hence ( M is triangle & M is discerning ) by Th6; ::_thesis: verum end; end; definition func Set_to_zero -> Function of [:2,2:],REAL equals :: METRIC_1:def 20 [:2,2:] --> 0; coherence [:2,2:] --> 0 is Function of [:2,2:],REAL ; end; :: deftheorem defines Set_to_zero METRIC_1:def_20_:_ Set_to_zero = [:2,2:] --> 0; theorem Th27: :: METRIC_1:27 for x, y being Element of 2 holds Set_to_zero . (x,y) = 0 proof let x, y be Element of 2; ::_thesis: Set_to_zero . (x,y) = 0 A1: [x,y] in [:2,2:] by ZFMISC_1:87; thus Set_to_zero . (x,y) = Set_to_zero . [x,y] .= 0 by A1, FUNCOP_1:7 ; ::_thesis: verum end; theorem Th28: :: METRIC_1:28 for x, y being Element of 2 holds Set_to_zero . (x,y) = Set_to_zero . (y,x) proof let x, y be Element of 2; ::_thesis: Set_to_zero . (x,y) = Set_to_zero . (y,x) Set_to_zero . (x,y) = 0 by Th27 .= Set_to_zero . (y,x) by Th27 ; hence Set_to_zero . (x,y) = Set_to_zero . (y,x) ; ::_thesis: verum end; theorem Th29: :: METRIC_1:29 for x, y, z being Element of 2 holds Set_to_zero . (x,z) <= (Set_to_zero . (x,y)) + (Set_to_zero . (y,z)) proof let x, y, z be Element of 2; ::_thesis: Set_to_zero . (x,z) <= (Set_to_zero . (x,y)) + (Set_to_zero . (y,z)) ( Set_to_zero . (x,y) = 0 & Set_to_zero . (y,z) = 0 ) by Th27; hence Set_to_zero . (x,z) <= (Set_to_zero . (x,y)) + (Set_to_zero . (y,z)) by Th27; ::_thesis: verum end; definition func ZeroSpace -> MetrStruct equals :: METRIC_1:def 21 MetrStruct(# 2,Set_to_zero #); coherence MetrStruct(# 2,Set_to_zero #) is MetrStruct ; end; :: deftheorem defines ZeroSpace METRIC_1:def_21_:_ ZeroSpace = MetrStruct(# 2,Set_to_zero #); registration cluster ZeroSpace -> non empty strict ; coherence ( ZeroSpace is strict & not ZeroSpace is empty ) ; end; registration cluster ZeroSpace -> Reflexive symmetric triangle ; coherence ( ZeroSpace is Reflexive & ZeroSpace is symmetric & ZeroSpace is triangle ) proof set M = MetrStruct(# 2,Set_to_zero #); A1: for x, y, z being Element of MetrStruct(# 2,Set_to_zero #) holds ( dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) ) by Th28, Th29; for x being Element of MetrStruct(# 2,Set_to_zero #) holds dist (x,x) = 0 by Th27; hence ( ZeroSpace is Reflexive & ZeroSpace is symmetric & ZeroSpace is triangle ) by A1, Th1, Th3, Th4; ::_thesis: verum end; end; definition let S be MetrStruct ; let p, q, r be Element of S; predq is_between p,r means :Def22: :: METRIC_1:def 22 ( p <> q & p <> r & q <> r & dist (p,r) = (dist (p,q)) + (dist (q,r)) ); end; :: deftheorem Def22 defines is_between METRIC_1:def_22_:_ for S being MetrStruct for p, q, r being Element of S holds ( q is_between p,r iff ( p <> q & p <> r & q <> r & dist (p,r) = (dist (p,q)) + (dist (q,r)) ) ); theorem :: METRIC_1:30 for S being non empty Reflexive symmetric triangle MetrStruct for p, q, r being Element of S st q is_between p,r holds q is_between r,p proof let S be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for p, q, r being Element of S st q is_between p,r holds q is_between r,p let p, q, r be Element of S; ::_thesis: ( q is_between p,r implies q is_between r,p ) assume A1: q is_between p,r ; ::_thesis: q is_between r,p hence ( r <> q & r <> p & q <> p ) by Def22; :: according to METRIC_1:def_22 ::_thesis: dist (r,p) = (dist (r,q)) + (dist (q,p)) dist (p,r) = (dist (p,q)) + (dist (q,r)) by A1, Def22; hence dist (r,p) = (dist (r,q)) + (dist (q,p)) ; ::_thesis: verum end; theorem :: METRIC_1:31 for S being MetrSpace for p, q, r being Element of S st q is_between p,r holds ( not p is_between q,r & not r is_between p,q ) proof let S be MetrSpace; ::_thesis: for p, q, r being Element of S st q is_between p,r holds ( not p is_between q,r & not r is_between p,q ) let p, q, r be Element of S; ::_thesis: ( q is_between p,r implies ( not p is_between q,r & not r is_between p,q ) ) assume A1: q is_between p,r ; ::_thesis: ( not p is_between q,r & not r is_between p,q ) then A2: dist (p,r) = (dist (p,q)) + (dist (q,r)) by Def22; A3: p <> q by A1, Def22; thus not p is_between q,r ::_thesis: not r is_between p,q proof assume p is_between q,r ; ::_thesis: contradiction then dist (p,r) = (dist (p,q)) + ((dist (q,p)) + (dist (p,r))) by A2, Def22; hence contradiction by A3, Th7; ::_thesis: verum end; assume r is_between p,q ; ::_thesis: contradiction then A4: dist (p,q) = ((dist (p,q)) + (dist (q,r))) + (dist (r,q)) by A2, Def22; q <> r by A1, Def22; hence contradiction by A4, Th7; ::_thesis: verum end; theorem :: METRIC_1:32 for S being MetrSpace for p, q, r, s being Element of S st q is_between p,r & r is_between p,s holds ( q is_between p,s & r is_between q,s ) proof let S be MetrSpace; ::_thesis: for p, q, r, s being Element of S st q is_between p,r & r is_between p,s holds ( q is_between p,s & r is_between q,s ) let p, q, r, s be Element of S; ::_thesis: ( q is_between p,r & r is_between p,s implies ( q is_between p,s & r is_between q,s ) ) assume A1: q is_between p,r ; ::_thesis: ( not r is_between p,s or ( q is_between p,s & r is_between q,s ) ) then A2: p <> q by Def22; assume A3: r is_between p,s ; ::_thesis: ( q is_between p,s & r is_between q,s ) then A4: ( p <> s & r <> s ) by Def22; dist (p,r) = (dist (p,q)) + (dist (q,r)) by A1, Def22; then A5: dist (p,s) = ((dist (p,q)) + (dist (q,r))) + (dist (r,s)) by A3, Def22; ( dist (p,s) <= (dist (p,q)) + (dist (q,s)) & (dist (p,q)) + (dist (q,s)) <= ((dist (q,r)) + (dist (r,s))) + (dist (p,q)) ) by Th4, XREAL_1:6; then A6: (dist (p,q)) + (dist (q,s)) = (dist (p,q)) + ((dist (q,r)) + (dist (r,s))) by A5, XXREAL_0:1; A7: q <> r by A1, Def22; then q <> s by A5, Th7; hence ( q is_between p,s & r is_between q,s ) by A2, A7, A4, A5, A6, Def22; ::_thesis: verum end; definition let M be non empty MetrStruct ; let p, r be Element of M; func open_dist_Segment (p,r) -> Subset of M equals :: METRIC_1:def 23 { q where q is Element of M : q is_between p,r } ; coherence { q where q is Element of M : q is_between p,r } is Subset of M proof defpred S1[ Element of M] means \$1 is_between p,r; { q where q is Element of M : S1[q] } c= the carrier of M from FRAENKEL:sch_10(); hence { q where q is Element of M : q is_between p,r } is Subset of M ; ::_thesis: verum end; end; :: deftheorem defines open_dist_Segment METRIC_1:def_23_:_ for M being non empty MetrStruct for p, r being Element of M holds open_dist_Segment (p,r) = { q where q is Element of M : q is_between p,r } ; theorem :: METRIC_1:33 for M being non empty MetrSpace for p, r, x being Element of M holds ( x in open_dist_Segment (p,r) iff x is_between p,r ) proof let M be non empty MetrSpace; ::_thesis: for p, r, x being Element of M holds ( x in open_dist_Segment (p,r) iff x is_between p,r ) let p, r, x be Element of M; ::_thesis: ( x in open_dist_Segment (p,r) iff x is_between p,r ) ( x in open_dist_Segment (p,r) implies x is_between p,r ) proof assume x in open_dist_Segment (p,r) ; ::_thesis: x is_between p,r then ex q being Element of M st ( x = q & q is_between p,r ) ; hence x is_between p,r ; ::_thesis: verum end; hence ( x in open_dist_Segment (p,r) iff x is_between p,r ) ; ::_thesis: verum end; definition let M be non empty MetrStruct ; let p, r be Element of M; func close_dist_Segment (p,r) -> Subset of M equals :: METRIC_1:def 24 { q where q is Element of M : q is_between p,r } \/ {p,r}; coherence { q where q is Element of M : q is_between p,r } \/ {p,r} is Subset of M proof defpred S1[ Element of M] means \$1 is_between p,r; A1: {p,r} c= the carrier of M by ZFMISC_1:32; { q where q is Element of M : S1[q] } c= the carrier of M from FRAENKEL:sch_10(); hence { q where q is Element of M : q is_between p,r } \/ {p,r} is Subset of M by A1, XBOOLE_1:8; ::_thesis: verum end; end; :: deftheorem defines close_dist_Segment METRIC_1:def_24_:_ for M being non empty MetrStruct for p, r being Element of M holds close_dist_Segment (p,r) = { q where q is Element of M : q is_between p,r } \/ {p,r}; theorem :: METRIC_1:34 for M being non empty MetrStruct for p, r, x being Element of M holds ( x in close_dist_Segment (p,r) iff ( x is_between p,r or x = p or x = r ) ) proof let M be non empty MetrStruct ; ::_thesis: for p, r, x being Element of M holds ( x in close_dist_Segment (p,r) iff ( x is_between p,r or x = p or x = r ) ) let p, r, x be Element of M; ::_thesis: ( x in close_dist_Segment (p,r) iff ( x is_between p,r or x = p or x = r ) ) A1: ( not x in close_dist_Segment (p,r) or x is_between p,r or x = p or x = r ) proof assume x in close_dist_Segment (p,r) ; ::_thesis: ( x is_between p,r or x = p or x = r ) then ( x in { q where q is Element of M : q is_between p,r } or x in {p,r} ) by XBOOLE_0:def_3; then ( ex q being Element of M st ( x = q & q is_between p,r ) or x = p or x = r ) by TARSKI:def_2; hence ( x is_between p,r or x = p or x = r ) ; ::_thesis: verum end; now__::_thesis:_(_(_x_is_between_p,r_or_x_=_p_or_x_=_r_)_implies_x_in_close_dist_Segment_(p,r)_) assume ( x is_between p,r or x = p or x = r ) ; ::_thesis: x in close_dist_Segment (p,r) then ( x in { q where q is Element of M : q is_between p,r } or x in {p,r} ) by TARSKI:def_2; hence x in close_dist_Segment (p,r) by XBOOLE_0:def_3; ::_thesis: verum end; hence ( x in close_dist_Segment (p,r) iff ( x is_between p,r or x = p or x = r ) ) by A1; ::_thesis: verum end;