metric spaces 1new

《metric spaces 1new》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、FORMALIZEDMATHEMATICSVol.1,No.3,May–August1990Universit´eCatholiquedeLouvainMetricSpaces1StanislawaKanasAdamLeckoTechnicalUniversityinRzesz´owTechnicalUniversityinRzesz´owDepartmentofMathematicsDepartmentofMathematicsMariuszStartekTechnicalUniversityinRzesz´owDepartmentofMathematicsSummar

2、y.Inthispaperwedefinethemetricspaces.Twoexam-plesofmetricspacesaregiven.Wedefinethediscretemetricandthemetricontherealaxis.Moreovertheopenball,thecloseballandthesphereinmetricspacesareintroduced.Wealsoprovesometheoremsconcerningtheseconcepts.MMLIdentifier:METRIC1.Thepapers[3],[7],[2],[1],[5]

3、,[6],and[4]providethenotationandterminologyforthispaper.Weconsidermetricstructureswhicharesystemshacarrier,adistanceiwherethecarrierisanon-emptysetandthedistanceisafunctionfrom[:thecarrier,thecarrier:]into.InthesequelMwillbeametricstructure.LetusconsiderM.ApointofMisanelementofthecarrier

4、ofM.Nextwestateaproposition(1)ForeveryelementxofthecarrierofMholdsxisapointofM.LetusconsiderM,andleta,bbeelementsofthecarrierofM.Thefunctorρ(a,b)yieldingarealnumber,isdefinedby:ρ(a,b)=(thedistanceofM)(a,b).Wenowstateaproposition(2)Forallelementsx,yofthecarrierofMholdsρ(x,y)=(thedistanceofM

5、)(x,y).1SupportedbyRPBP.III.24-B.5c1990FondationPhilippeleHodey607ISSN0777–4028608StanislawaKanasetal.Inthesequelxwillbearbitrary.Letusconsiderx.Then{x}isanon-emptyset.Thefunction{[∅,∅]}7→0from[:{∅},{∅}:]intoisdefinedby:{[∅,∅]}7→0=[:{∅},{∅}:]7−→0.Nextwestateaproposition(3){[∅,∅]}7→0=[:{∅}

6、,{∅}:]7−→0.Ametricstructureissaidtobeametricspaceif:forallelementsa,b,cofthecarrierofitholdsρ(a,b)=0ifandonlyifa=bbutρ(a,b)=ρ(b,a)andρ(a,c)≤ρ(a,b)+ρ(b,c).Wenowstatethreepropositions:(4)ForeveryMbeingametricstructureholdsMisametricspaceifandonlyifforallelementsa,b,cofthecarrierofMholdsρ(a,

7、b)=0ifandonlyifa=bbutρ(a,b)=ρ(b,a)andρ(a,c)≤ρ(a,b)+ρ(b,c).(5)ForeverymetricspaceMandforallelementsa,bofthecarrierofMholdsρ(a,b)=ρ(b,a).(6)ForeverymetricspaceMandforallelementsa,b,cofthecarrierofMholdsρ(a,c)≤ρ(a,b)+ρ(b,c).InthesequelPMdenotesametricspaceandp1,p2denot