:: Real Linear-Metric Space and Isometric Functions
::  by Robert Milewski
::
:: Received November 3, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, METRIC_1, CONVEX1, SUBSET_1, REAL_1, CARD_1,
      XXREAL_0, RELAT_1, ARYTM_1, FINSEQ_1, STRUCT_0, PARTFUN1, ARYTM_3,
      COMPLEX1, CARD_3, ZFMISC_1, BINTREE1, TREES_2, FUNCT_1, TREES_4,
      ORDINAL4, CAT_1, TREES_1, POWER, INT_1, NAT_1, FINSEQ_2, MARGREL1,
      EUCLID, XBOOLEAN, MCART_1, BINTREE2, ABIAN, TARSKI, RELAT_2, FUNCT_2,
      RLVECT_1, ALGSTR_0, BINOP_1, UNIALG_1, SUPINF_2, PRE_TOPC, GROUP_1,
      GROUP_2, VECTMETR, FUNCT_7, XCMPLX_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS,
      MCART_1, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, RELAT_2, XXREAL_0, INT_1,
      NAT_1, NAT_D, POWER, ABIAN, SERIES_1, RELAT_1, RELSET_1, MARGREL1,
      BINOP_1, DOMAIN_1, FUNCT_1, PARTFUN1, FUNCT_2, STRUCT_0, ALGSTR_0,
      PRE_TOPC, FINSEQ_1, FINSEQ_2, FINSEQ_4, BINARITH, TREES_1, TREES_2,
      TREES_4, BINTREE1, BINTREE2, RVSUM_1, RLVECT_1, GROUP_1, GROUP_2, TOPS_2,
      METRIC_1, EUCLID;
 constructors REAL_1, NAT_D, FINSEQOP, FINSEQ_4, FINSOP_1, SERIES_1, REALSET1,
      BINARITH, ABIAN, TOPS_2, GROUP_2, EUCLID, BINTREE2, RVSUM_1, RELSET_1,
      XTUPLE_0, BINOP_1, BINOP_2, NUMBERS;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS,
      XXREAL_0, NAT_1, FINSEQ_1, BINOP_2, MARGREL1, FINSEQ_2, TREES_2,
      STRUCT_0, METRIC_1, GROUP_2, BINTREE1, BINTREE2, VALUED_0, XREAL_0,
      RELAT_1, INT_1, EUCLID, ORDINAL1, CARD_1, XTUPLE_0;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin  :: Convex and Internal Metric Spaces

definition
  let V be non empty MetrStruct;
  attr V is convex means
:: VECTMETR:def 1

  for x,y be Element of V for r be Real st 0 <= r & r <= 1
  ex z be Element of V st dist(x,z) = r * dist(x,y) &
     dist(z,y) = (1 - r) * dist(x,y);
end;

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

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

registration
  cluster convex -> internal for non empty MetrSpace;
end;

registration
  cluster convex for non empty MetrSpace;
end;

begin  :: Isometric Functions

definition
  let V be non empty MetrStruct;
  let f be Function of V,V;
  attr f is isometric means
:: VECTMETR:def 3

  for x,y be Element of V holds dist(x,y) = dist(f.x,f.y);
end;

registration
  let V be non empty MetrStruct;
  cluster id(V) -> onto isometric;
end;

theorem :: VECTMETR:2
  for V be non empty MetrStruct holds id(V) is onto isometric;

registration
  let V be non empty MetrStruct;
  cluster onto isometric for Function of V,V;
end;

definition
  let V be non empty MetrStruct;
  func ISOM(V) -> set means
:: VECTMETR:def 4

  for x be object holds x in it iff x is onto isometric Function of V,V;
end;

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

registration
  let V be discerning Reflexive non empty MetrStruct;
  cluster isometric -> one-to-one for Function of V,V;
end;

registration
  let V be discerning Reflexive non empty MetrStruct;
  let f be onto isometric Function of V,V;
  cluster f" -> onto isometric;
end;

registration
  let V be non empty MetrStruct;
  let f,g be onto isometric Function of V,V;
  cluster f*g -> onto isometric for Function of V,V;
end;

registration
  let V be non empty MetrStruct;
  cluster ISOM V -> non empty;
end;

begin  :: Real Linear-Metric Spaces

definition
  struct(RLSStruct,MetrStruct) RLSMetrStruct (# carrier -> set, distance ->
Function of [:the carrier,the carrier:],REAL, ZeroF -> Element of the carrier,
    addF -> BinOp of the carrier, Mult -> Function of [:REAL, the carrier:],the
    carrier #);
end;

registration
  cluster non empty strict for RLSMetrStruct;
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;
end;

definition
  let V be non empty RLSMetrStruct;
  attr V is homogeneous means
:: VECTMETR:def 5

  for r be Real for v,w be Element of V
  holds dist(r*v,r*w) = |.r.| * dist(v,w);
end;

definition
  let V be non empty RLSMetrStruct;
  attr V is translatible means
:: VECTMETR:def 6

  for u,w,v be Element of V holds dist(v,w) = dist(v+u,w+u);
end;

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);
end;

registration
  cluster strict Abelian add-associative right_zeroed right_complementable
    vector-distributive scalar-distributive scalar-associative scalar-unital
    Reflexive discerning symmetric triangle homogeneous
    translatible for non empty RLSMetrStruct;
end;

definition
  mode RealLinearMetrSpace is Abelian add-associative right_zeroed
    right_complementable vector-distributive scalar-distributive
    scalar-associative scalar-unital Reflexive discerning symmetric
    triangle homogeneous translatible non empty RLSMetrStruct;
end;

::$CT 3

theorem :: VECTMETR:6
  for V be homogeneous Abelian add-associative right_zeroed
  right_complementable vector-distributive scalar-distributive
  scalar-associative scalar-unital non empty RLSMetrStruct for r be
  Real for v be Element of V holds Norm (r * v) = |.r.| * Norm v;

theorem :: VECTMETR:7
  for V be translatible Abelian add-associative right_zeroed
right_complementable triangle non empty RLSMetrStruct for v,w be Element of V
  holds Norm (v + w) <= Norm v + Norm w;

theorem :: VECTMETR:8
  for V be translatible add-associative right_zeroed
  right_complementable non empty RLSMetrStruct for v,w be Element of V holds
  dist(v,w) = Norm (w - v);

definition
  let n be Element of NAT;
  func RLMSpace n -> strict RealLinearMetrSpace means
:: VECTMETR:def 8

  the carrier of it = REAL n &
  the distance of it = Pitag_dist n &
  0.it = 0*n &
  (for x,y be Element of REAL n holds (the addF of it).(x,y) = x + y) &
  for x be Element of REAL n,r be Element of REAL holds
    (the Mult of it).(r,x) = r * x;
end;

theorem :: VECTMETR:9
  for n be Element of NAT for f be onto isometric Function of RLMSpace n,
  RLMSpace n holds rng f = REAL n;

begin  :: Groups of Onto Isometric Functions

definition
  let n be Element of NAT;
  func IsomGroup n -> strict multMagma means
:: VECTMETR:def 9

  the carrier of it = ISOM RLMSpace n &
  for f,g be Function st f in ISOM RLMSpace n & g in ISOM RLMSpace n
   holds (the multF of it).(f,g) = f*g;
end;

registration
  let n be Element of NAT;
  cluster IsomGroup n -> non empty;
end;

registration
  let n be Element of NAT;
  cluster IsomGroup n -> associative Group-like;
end;

theorem :: VECTMETR:10
  for n be Element of NAT holds 1_IsomGroup n = id (RLMSpace n);

theorem :: VECTMETR:11
  for n be Element of NAT for f be Element of IsomGroup n for g be
  Function of RLMSpace n,RLMSpace n st f = g holds f" = g";

definition
  let n be Element of NAT;
  let G be Subgroup of IsomGroup n;
  func SubIsomGroupRel G -> Relation of the carrier of RLMSpace n means
:: VECTMETR:def 10

  for A,B be Element of RLMSpace n holds [A,B] in it iff ex f be Function st f
  in the carrier of G & f.A = B;
end;

registration
  let n be Element of NAT;
  let G be Subgroup of IsomGroup n;
  cluster SubIsomGroupRel G -> total symmetric transitive;
end;