:: METRIC_1 semantic presentation

definition

attr a₁ is strict;
struct MetrStruct -> 1-sorted ;
aggr MetrStruct(# carrier, distance #) -> MetrStruct ;
sel distance c₁ -> Function of [:the carrier of a₁,the carrier of a₁:], REAL ;

end;

registration

cluster non empty strict MetrStruct ;
existence

proof end;

end;

definition

let c₁, c₂ be set ;
let c₃ be PartFunc of [:c₁,c₂:], REAL ;
let c₄ be Element of c₁;
let c₅ be Element of c₂;
redefine func . as c₃ . c₄,c₅ -> Real;
coherence

proof end;

end;

definition

let c₁ be MetrStruct ;
let c₂, c₃ be Element of c₁;
func dist c₂,c₃ -> Real equals :: METRIC_1:def 1
the distance of a₁ . a₂,a₃;
coherence ;

end;

:: deftheorem Def1 defines dist METRIC_1:def 1 :

definition

func Empty^2-to-zero -> Function of [:{{} },{{} }:], REAL equals :: METRIC_1:def 2
[:{{} },{{} }:] --> 0;
coherence

proof end;

end;

:: deftheorem Def2 defines Empty^2-to-zero METRIC_1:def 2 :

Lemma1: [{} ,{} ] in [:{{} },{{} }:]
by ZFMISC_1:34;

E2: Empty^2-to-zero . {} ,{} = Empty^2-to-zero . [{} ,{} ]
.= 0 by Lemma1, FUNCOP_1:13 ;

Lemma3: for b₁, b₂ being Element of {{} } holds
( Empty^2-to-zero . b₁,b₂ = 0 iff b₁ = b₂ )

proof end;

Lemma4: for b₁, b₂ being Element of {{} } holds Empty^2-to-zero . b₁,b₂ = Empty^2-to-zero . b₂,b₁

proof end;

Lemma5: for b₁, b₂, b₃ being Element of {{} } holds Empty^2-to-zero . b₁,b₃ <= (Empty^2-to-zero . b₁,b₂) + (Empty^2-to-zero . b₂,b₃)

proof end;

definition

let c₁ be set ;
let c₂ be PartFunc of [:c₁,c₁:], REAL ;
attr a₂ is Reflexive means :Def3: :: METRIC_1:def 3
for b₁ being Element of a₁ holds a₂ . b₁,b₁ = 0;
attr a₂ is discerning means :Def4: :: METRIC_1:def 4
for b₁, b₂ being Element of a₁ st a₂ . b₁,b₂ = 0 holds
b₁ = b₂;
attr a₂ is symmetric means :Def5: :: METRIC_1:def 5
for b₁, b₂ being Element of a₁ holds a₂ . b₁,b₂ = a₂ . b₂,b₁;
attr a₂ is triangle means :Def6: :: METRIC_1:def 6
for b₁, b₂, b₃ being Element of a₁ holds a₂ . b₁,b₃ <= (a₂ . b₁,b₂) + (a₂ . b₂,b₃);

end;

:: deftheorem Def3 defines Reflexive METRIC_1:def 3 :

:: deftheorem Def4 defines discerning METRIC_1:def 4 :

:: deftheorem Def5 defines symmetric METRIC_1:def 5 :

:: deftheorem Def6 defines triangle METRIC_1:def 6 :

definition

let c₁ be MetrStruct ;
attr a₁ is Reflexive means :Def7: :: METRIC_1:def 7
the distance of a₁ is Reflexive;
attr a₁ is discerning means :Def8: :: METRIC_1:def 8
the distance of a₁ is discerning;
attr a₁ is symmetric means :Def9: :: METRIC_1:def 9
the distance of a₁ is symmetric;
attr a₁ is triangle means :Def10: :: METRIC_1:def 10
the distance of a₁ is triangle;

end;

:: deftheorem Def7 defines Reflexive METRIC_1:def 7 :

:: deftheorem Def8 defines discerning METRIC_1:def 8 :

:: deftheorem Def9 defines symmetric METRIC_1:def 9 :

:: deftheorem Def10 defines triangle METRIC_1:def 10 :

registration

cluster non empty strict Reflexive discerning symmetric triangle MetrStruct ;
existence

proof end;

end;

definition

mode MetrSpace is Reflexive discerning symmetric triangle MetrStruct ;

end;

theorem Th1: :: METRIC_1:1

for b₁ being MetrStruct holds
( ( for b₂ being Element of b₁ holds dist b₂,b₂ = 0 ) iff b₁ is Reflexive )

proof end;

theorem Th2: :: METRIC_1:2

for b₁ being MetrStruct holds
( ( for b₂, b₃ being Element of b₁ st dist b₂,b₃ = 0 holds
b₂ = b₃ ) iff b₁ is discerning )

proof end;

theorem Th3: :: METRIC_1:3

for b₁ being MetrStruct holds
( ( for b₂, b₃ being Element of b₁ holds dist b₂,b₃ = dist b₃,b₂ ) iff b₁ is symmetric )

proof end;

theorem Th4: :: METRIC_1:4

for b₁ being MetrStruct holds
( ( for b₂, b₃, b₄ being Element of b₁ holds dist b₂,b₄ <= (dist b₂,b₃) + (dist b₃,b₄) ) iff b₁ is triangle )

proof end;

definition

let c₁ be symmetric MetrStruct ;
let c₂, c₃ be Element of c₁;
redefine func dist as dist c₂,c₃ -> Real;
commutativity by Th3;

end;

theorem Th5: :: METRIC_1:5

for b₁ being Reflexive symmetric triangle MetrStruct
for b₂, b₃ being Element of b₁ holds 0 <= dist b₂,b₃

proof end;

theorem Th6: :: METRIC_1:6

for b₁ being MetrStruct st ( for b₂, b₃, b₄ being Element of b₁ holds
( ( dist b₂,b₃ = 0 implies b₂ = b₃ ) & ( b₂ = b₃ implies dist b₂,b₃ = 0 ) & dist b₂,b₃ = dist b₃,b₂ & dist b₂,b₄ <= (dist b₂,b₃) + (dist b₃,b₄) ) ) holds
b₁ is MetrSpace

proof end;

definition

let c₁ be set ;
func discrete_dist c₁ -> Function of [:a₁,a₁:], REAL means :Def11: :: METRIC_1:def 11
for b₁, b₂ being Element of a₁ holds
( a₂ . b₁,b₁ = 0 & ( b₁ <> b₂ implies a₂ . b₁,b₂ = 1 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines discrete_dist METRIC_1:def 11 :

definition

let c₁ be set ;
func DiscreteSpace c₁ -> strict MetrStruct equals :: METRIC_1:def 12
MetrStruct(# a₁,(discrete_dist a₁) #);
coherence ;

end;

:: deftheorem Def12 defines DiscreteSpace METRIC_1:def 12 :

registration

let c₁ be non empty set ;
cluster DiscreteSpace a₁ -> non empty strict ;
coherence by STRUCT_0:def 1;

end;

registration

let c₁ be set ;
cluster DiscreteSpace a₁ -> strict Reflexive discerning symmetric triangle ;
coherence

proof end;

end;

definition

func real_dist -> Function of [:REAL ,REAL :], REAL means :Def13: :: METRIC_1:def 13
for b₁, b₂ being Element of REAL holds a₁ . b₁,b₂ = abs (b₁ - b₂);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines real_dist METRIC_1:def 13 :

theorem Th7: :: METRIC_1:7

canceled;

theorem Th8: :: METRIC_1:8

canceled;

theorem Th9: :: METRIC_1:9

for b₁, b₂ being Element of REAL holds
( real_dist . b₁,b₂ = 0 iff b₁ = b₂ )

proof end;

theorem Th10: :: METRIC_1:10

for b₁, b₂ being Element of REAL holds real_dist . b₁,b₂ = real_dist . b₂,b₁

proof end;

theorem Th11: :: METRIC_1:11

for b₁, b₂, b₃ being Element of REAL holds real_dist . b₁,b₂ <= (real_dist . b₁,b₃) + (real_dist . b₃,b₂)

proof end;

definition

func RealSpace -> strict MetrStruct equals :: METRIC_1:def 14
MetrStruct(# REAL ,real_dist #);
coherence ;

end;

:: deftheorem Def14 defines RealSpace METRIC_1:def 14 :

registration

cluster RealSpace -> non empty strict ;
coherence by STRUCT_0:def 1;

end;

registration

cluster RealSpace -> non empty strict Reflexive discerning symmetric triangle ;
coherence

proof end;

end;

definition

let c₁ be MetrStruct ;
let c₂ be Element of c₁;
let c₃ be real number ;
func Ball c₂,c₃ -> Subset of a₁ means :Def15: :: METRIC_1:def 15
ex b₁ being non empty MetrStruct ex b₂ being Element of b₁ st
( b₁ = a₁ & b₂ = a₂ & a₄ = { b₃ where B is Element of b₁ : dist b₂,b₃ < a₃ } ) if not a₁ is empty
otherwise a₄ is empty;
existence

proof end;

correctness ;

end;

:: deftheorem Def15 defines Ball METRIC_1:def 15 :

definition

let c₁ be MetrStruct ;
let c₂ be Element of c₁;
let c₃ be real number ;
func cl_Ball c₂,c₃ -> Subset of a₁ means :Def16: :: METRIC_1:def 16
ex b₁ being non empty MetrStruct ex b₂ being Element of b₁ st
( b₁ = a₁ & b₂ = a₂ & a₄ = { b₃ where B is Element of b₁ : dist b₂,b₃ <= a₃ } ) if not a₁ is empty
otherwise a₄ is empty;
existence

proof end;

correctness ;

end;

:: deftheorem Def16 defines cl_Ball METRIC_1:def 16 :

definition

let c₁ be MetrStruct ;
let c₂ be Element of c₁;
let c₃ be real number ;
func Sphere c₂,c₃ -> Subset of a₁ means :Def17: :: METRIC_1:def 17
ex b₁ being non empty MetrStruct ex b₂ being Element of b₁ st
( b₁ = a₁ & b₂ = a₂ & a₄ = { b₃ where B is Element of b₁ : dist b₂,b₃ = a₃ } ) if not a₁ is empty
otherwise a₄ is empty;
existence

proof end;

correctness ;

end;

:: deftheorem Def17 defines Sphere METRIC_1:def 17 :

Lemma26: for b₁ being real number
for b₂ being non empty MetrStruct
for b₃ being Element of b₂ holds Ball b₃,b₁ = { b₄ where B is Element of b₂ : dist b₃,b₄ < b₁ }

proof end;

Lemma27: for b₁ being real number
for b₂ being non empty MetrStruct
for b₃ being Element of b₂ holds cl_Ball b₃,b₁ = { b₄ where B is Element of b₂ : dist b₃,b₄ <= b₁ }

proof end;

Lemma28: for b₁ being real number
for b₂ being non empty MetrStruct
for b₃ being Element of b₂ holds Sphere b₃,b₁ = { b₄ where B is Element of b₂ : dist b₃,b₄ = b₁ }

proof end;

theorem Th12: :: METRIC_1:12

for b₁ being real number
for b₂ being MetrStruct
for b₃, b₄ being Element of b₂ holds
( b₄ in Ball b₃,b₁ iff ( not b₂ is empty & dist b₃,b₄ < b₁ ) )

proof end;

theorem Th13: :: METRIC_1:13

for b₁ being real number
for b₂ being MetrStruct
for b₃, b₄ being Element of b₂ holds
( b₄ in cl_Ball b₃,b₁ iff ( not b₂ is empty & dist b₃,b₄ <= b₁ ) )

proof end;

theorem Th14: :: METRIC_1:14

for b₁ being real number
for b₂ being MetrStruct
for b₃, b₄ being Element of b₂ holds
( b₄ in Sphere b₃,b₁ iff ( not b₂ is empty & dist b₃,b₄ = b₁ ) )

proof end;

theorem Th15: :: METRIC_1:15

for b₁ being real number
for b₂ being MetrStruct
for b₃ being Element of b₂ holds Ball b₃,b₁ c= cl_Ball b₃,b₁

proof end;

theorem Th16: :: METRIC_1:16

for b₁ being real number
for b₂ being MetrStruct
for b₃ being Element of b₂ holds Sphere b₃,b₁ c= cl_Ball b₃,b₁

proof end;

theorem Th17: :: METRIC_1:17

for b₁ being real number
for b₂ being MetrStruct
for b₃ being Element of b₂ holds (Sphere b₃,b₁) \/ (Ball b₃,b₁) = cl_Ball b₃,b₁

proof end;

theorem Th18: :: METRIC_1:18

for b₁ being real number
for b₂ being non empty MetrStruct
for b₃ being Element of b₂ holds Ball b₃,b₁ = { b₄ where B is Element of b₂ : dist b₃,b₄ < b₁ } by Lemma26;

theorem Th19: :: METRIC_1:19

for b₁ being real number
for b₂ being non empty MetrStruct
for b₃ being Element of b₂ holds cl_Ball b₃,b₁ = { b₄ where B is Element of b₂ : dist b₃,b₄ <= b₁ } by Lemma27;

theorem Th20: :: METRIC_1:20

for b₁ being real number
for b₂ being non empty MetrStruct
for b₃ being Element of b₂ holds Sphere b₃,b₁ = { b₄ where B is Element of b₂ : dist b₃,b₄ = b₁ } by Lemma28;