:: VECTMETR semantic presentation

definition

let V be non empty MetrStruct ;
attr V is convex means :Def1: :: VECTMETR:def 1
for x, y being Element of V
for r being Real st 0 <= r & r <= 1 holds
ex z being Element of V st
( dist x,z = r * (dist x,y) & dist z,y = (1 - r) * (dist x,y) );

end;

:: deftheorem Def1 defines convex VECTMETR:def 1 :

definition

let V be non empty MetrStruct ;
attr V is internal means :: VECTMETR:def 2
for x, y being Element of V
for p, q being Real st p > 0 & q > 0 holds
ex f being FinSequence of the carrier of V st
( f /. 1 = x & f /. (len f) = y & ( for i being Nat st 1 <= i & i <= (len f) - 1 holds
dist (f /. i),(f /. (i + 1)) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Nat st 1 <= i & i <= len F holds
F /. i = dist (f /. i),(f /. (i + 1)) ) holds
abs ((dist x,y) - (Sum F)) < q ) );

end;

:: deftheorem defines internal VECTMETR:def 2 :

theorem Th1: :: VECTMETR:1

for V being non empty MetrSpace st V is convex holds
for x, y being Element of V
for p being Real st p > 0 holds
ex f being FinSequence of the carrier of V st
( f /. 1 = x & f /. (len f) = y & ( for i being Nat st 1 <= i & i <= (len f) - 1 holds
dist (f /. i),(f /. (i + 1)) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Nat st 1 <= i & i <= len F holds
F /. i = dist (f /. i),(f /. (i + 1)) ) holds
dist x,y = Sum F ) )

proof end;

registration

cluster non empty convex -> non empty internal MetrStruct ;
coherence

proof end;

end;

registration

cluster non empty convex internal MetrStruct ;
existence

proof end;

end;

definition

mode Geometry is non empty Reflexive discerning symmetric triangle internal MetrStruct ;

end;

definition

let V be non empty MetrStruct ;
let f be Function of V,V;
attr f is isometric means :Def3: :: VECTMETR:def 3
( rng f = the carrier of V & ( for x, y being Element of V holds dist x,y = dist (f . x),(f . y) ) );

end;

:: deftheorem Def3 defines isometric VECTMETR:def 3 :

definition

let V be non empty MetrStruct ;
func ISOM V -> set means :Def4: :: VECTMETR:def 4
for x being set holds
( x in it iff ex f being Function of V,V st
( f = x & f is isometric ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines ISOM VECTMETR:def 4 :

definition

let V be non empty MetrStruct ;
:: original: ISOM
redefine func ISOM V -> Subset of (Funcs the carrier of V,the carrier of V);
coherence

proof end;

end;

theorem Th2: :: VECTMETR:2

for V being non empty Reflexive discerning MetrStruct
for f being Function of V,V st f is isometric holds
f is one-to-one

proof end;

registration

let V be non empty Reflexive discerning MetrStruct ;
cluster isometric -> one-to-one Relation of the carrier of V,the carrier of V;
coherence by Th2;

end;

registration

let V be non empty MetrStruct ;
cluster isometric Relation of the carrier of V,the carrier of V;
existence

proof end;

end;

theorem Th3: :: VECTMETR:3

for V being non empty Reflexive discerning MetrStruct
for f being isometric Function of V,V holds f " is isometric

proof end;

theorem Th4: :: VECTMETR:4

for V being non empty MetrStruct
for f, g being isometric Function of V,V holds f * g is isometric

proof end;

theorem Th5: :: VECTMETR:5

for V being non empty MetrStruct holds id V is isometric

proof end;

registration

let V be non empty MetrStruct ;
cluster ISOM V -> non empty ;
coherence

proof end;

end;

definition

attr c₁ is strict;
struct RLSMetrStruct -> RLSStruct , MetrStruct ;
aggr RLSMetrStruct(# carrier, distance, Zero, add, Mult #) -> RLSMetrStruct ;

end;

registration

cluster non empty strict RLSMetrStruct ;
existence

proof end;

end;

registration

let X be non empty set ;
let F be Function of [:X,X:], REAL ;
let O be Element of X;
let B be BinOp of X;
let G be Function of [:REAL ,X:],X;
cluster RLSMetrStruct(# X,F,O,B,G #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

definition

let V be non empty RLSMetrStruct ;
attr V is homogeneous means :Def5: :: VECTMETR:def 5
for r being Real
for v, w being Element of V holds dist (r * v),(r * w) = (abs r) * (dist v,w);

end;

:: deftheorem Def5 defines homogeneous VECTMETR:def 5 :

definition

let V be non empty RLSMetrStruct ;
attr V is translatible means :Def6: :: VECTMETR:def 6
for u, w, v being Element of V holds dist v,w = dist (v + u),(w + u);

end;

:: deftheorem Def6 defines translatible VECTMETR:def 6 :

definition

let V be non empty RLSMetrStruct ;
let v be Element of V;
func Norm v -> Real equals :: VECTMETR:def 7
dist (0. V),v;
coherence ;

end;

:: deftheorem defines Norm VECTMETR:def 7 :

registration

cluster non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like Reflexive discerning symmetric triangle strict homogeneous translatible RLSMetrStruct ;
existence

proof end;

end;

definition

mode RealLinearMetrSpace is non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like Reflexive discerning symmetric triangle homogeneous translatible RLSMetrStruct ;

end;

theorem :: VECTMETR:6

for V being non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like homogeneous RLSMetrStruct
for r being Real
for v being Element of V holds Norm (r * v) = (abs r) * (Norm v)

proof end;

theorem :: VECTMETR:7

for V being non empty Abelian add-associative right_zeroed right_complementable triangle translatible RLSMetrStruct
for v, w being Element of V holds Norm (v + w) <= (Norm v) + (Norm w)

proof end;

theorem :: VECTMETR:8

for V being non empty add-associative right_zeroed right_complementable translatible RLSMetrStruct
for v, w being Element of V holds dist v,w = Norm (w - v)

proof end;

definition

let n be Nat;
func RLMSpace n -> strict RealLinearMetrSpace means :Def8: :: VECTMETR:def 8
( the carrier of it = REAL n & the distance of it = Pitag_dist n & the Zero of it = 0* n & ( for x, y being Element of REAL n holds the add of it . x,y = x + y ) & ( for x being Element of REAL n
for r being Element of REAL holds the Mult of it . r,x = r * x ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines RLMSpace VECTMETR:def 8 :

theorem :: VECTMETR:9

for n being Nat
for f being isometric Function of (RLMSpace n),(RLMSpace n) holds rng f = REAL n

proof end;

definition

let n be Nat;
func IsomGroup n -> strict HGrStr means :Def9: :: VECTMETR:def 9
( the carrier of it = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds
the mult of it . f,g = f * g ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines IsomGroup VECTMETR:def 9 :

registration

let n be Nat;
cluster IsomGroup n -> non empty strict ;
coherence

proof end;

end;

registration

let n be Nat;
cluster IsomGroup n -> non empty strict Group-like associative ;
coherence

proof end;

end;

theorem Th10: :: VECTMETR:10

for n being Nat holds 1. (IsomGroup n) = id (RLMSpace n)

proof end;

theorem Th11: :: VECTMETR:11

for n being Nat
for f being Element of (IsomGroup n)
for g being Function of (RLMSpace n),(RLMSpace n) st f = g holds
f " = g "

proof end;

definition

let n be Nat;
let G be Subgroup of IsomGroup n;
func SubIsomGroupRel G -> Relation of the carrier of (RLMSpace n) means :Def10: :: VECTMETR:def 10
for A, B being Element of (RLMSpace n) holds
( [A,B] in it iff ex f being Function st
( f in the carrier of G & f . A = B ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines SubIsomGroupRel VECTMETR:def 10 :

registration

let n be Nat;
let G be Subgroup of IsomGroup n;
cluster SubIsomGroupRel G -> symmetric transitive total ;
coherence

proof end;

end;