:: Topology of Real Unitary Space
::  by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama
::
:: Received October 25, 2002
:: Copyright (c) 2002-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, RLVECT_1, RUSUB_4, SUBSET_1, ARYTM_3,
      SUPINF_2, TARSKI, ALGSTR_0, ARYTM_1, REAL_1, RELAT_1, BHSP_1, RLSUB_1,
      STRUCT_0, RVSUM_1, PROB_2, CARD_1, NORMSP_1, SQUARE_1, XXREAL_0,
      RLVECT_3, PCOMPS_1, SETFAM_1, PRE_TOPC, METRIC_1, RCOMP_1, COMPLEX1,
      RUSUB_5;
 notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS, XXREAL_0,
      XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, PRE_TOPC, DOMAIN_1, STRUCT_0,
      ALGSTR_0, RLVECT_1, RLSUB_1, SQUARE_1, BHSP_1, BHSP_2, RUSUB_1, RUSUB_3,
      RUSUB_4;
 constructors SETFAM_1, REAL_1, SQUARE_1, MEMBERED, COMPLEX1, REALSET1,
      PRE_TOPC, RLVECT_3, BHSP_2, RUSUB_3, RUSUB_4, XXREAL_0;
 registrations XBOOLE_0, SUBSET_1, XXREAL_0, XREAL_0, STRUCT_0, PRE_TOPC,
      TOPS_1, RLVECT_1, RUSUB_4, SQUARE_1, ORDINAL1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin  :: Parallelism of Subspaces

definition
  let V be non empty RLSStruct, M,N be Affine Subset of V;
  pred M is_parallel_to N means
:: RUSUB_5:def 1

  ex v being VECTOR of V st M = N + {v};
end;

theorem :: RUSUB_5:1
  for V being right_zeroed non empty RLSStruct, M be Affine Subset of
  V holds M is_parallel_to M;

theorem :: RUSUB_5:2
  for V being add-associative right_zeroed right_complementablenon
  empty RLSStruct, M,N be Affine Subset of V st M is_parallel_to N holds N
  is_parallel_to M;

theorem :: RUSUB_5:3
  for V being Abelian add-associative right_zeroed
  right_complementable non empty RLSStruct, M,L,N be Affine Subset of V st M
  is_parallel_to L & L is_parallel_to N holds M is_parallel_to N;

definition
  let V be non empty addLoopStr, M,N be Subset of V;
  func M - N -> Subset of V equals
:: RUSUB_5:def 2
  {u - v where u,v is Element of V: u in M &
  v in N};
end;

theorem :: RUSUB_5:4
  for V being RealLinearSpace, M,N being Affine Subset of V holds M
  - N is Affine;

theorem :: RUSUB_5:5
  for V being non empty addLoopStr, M,N being Subset of V st M is empty
  or N is empty holds M + N is empty;

theorem :: RUSUB_5:6
  for V being non empty addLoopStr, M,N being non empty Subset of V
  holds M + N is non empty;

theorem :: RUSUB_5:7
  for V being non empty addLoopStr, M,N being Subset of V st M is empty
  or N is empty holds M - N is empty;

theorem :: RUSUB_5:8
  for V being non empty addLoopStr, M,N being non empty Subset of V
  holds M - N is non empty;

theorem :: RUSUB_5:9
  for V being Abelian add-associative right_zeroed
  right_complementable non empty addLoopStr, M,N being Subset of V, v being
  Element of V holds M = N + {v} iff M - {v} = N;

theorem :: RUSUB_5:10
  for V being Abelian add-associative right_zeroed right_complementable
  non empty addLoopStr, M,N being Subset of V, v being Element of V st v in N
  holds M + {v} c= M + N;

theorem :: RUSUB_5:11
  for V being Abelian add-associative right_zeroed right_complementable
  non empty addLoopStr, M,N being Subset of V, v being Element of V st v in N
  holds M - {v} c= M - N;

theorem :: RUSUB_5:12
  for V being RealLinearSpace, M being non empty Subset of V holds 0.V in M - M
;

theorem :: RUSUB_5:13
  for V being RealLinearSpace, M being non empty Affine Subset of
  V, v being VECTOR of V st M is Subspace-like & v in M holds M + {v} c= M;

theorem :: RUSUB_5:14
  for V being RealLinearSpace, M being non empty Affine Subset of
  V, N1,N2 being non empty Affine Subset of V st N1 is Subspace-like & N2 is
  Subspace-like & M is_parallel_to N1 & M is_parallel_to N2 holds N1 = N2;

theorem :: RUSUB_5:15
  for V being RealLinearSpace, M being non empty Affine Subset of
  V, v being VECTOR of V st v in M holds 0.V in M - {v};

theorem :: RUSUB_5:16
  for V being RealLinearSpace, M being non empty Affine Subset of
V, v being VECTOR of V st v in M holds ex N being non empty Affine Subset of V
  st N = M - {v} & M is_parallel_to N & N is Subspace-like;

theorem :: RUSUB_5:17
  for V being RealLinearSpace, M being non empty Affine Subset of
  V, u,v being VECTOR of V st u in M & v in M holds M - {v} = M - {u};

theorem :: RUSUB_5:18
  for V being RealLinearSpace, M being non empty Affine Subset of
  V holds M - M = union {M - {v} where v is VECTOR of V : v in M};

theorem :: RUSUB_5:19
  for V being RealLinearSpace, M being non empty Affine Subset of
  V, v being VECTOR of V st v in M holds M - {v} = union {M - {u} where u is
  VECTOR of V : u in M};

theorem :: RUSUB_5:20
  for V being RealLinearSpace, M be non empty Affine Subset of V holds
  ex L being non empty Affine Subset of V st L = M - M & L is Subspace-like & M
  is_parallel_to L;

begin :: Orthogonality

definition
  let V be RealUnitarySpace, W be Subspace of V;
  func Ort_Comp W -> strict Subspace of V means
:: RUSUB_5:def 3

  the carrier of it = {v
  where v is VECTOR of V : for w being VECTOR of V st w in W holds w, v
  are_orthogonal};
end;

definition
  let V be RealUnitarySpace, M be non empty Subset of V;
  func Ort_Comp M -> strict Subspace of V means
:: RUSUB_5:def 4

  the carrier of it = {v
  where v is VECTOR of V : for w being VECTOR of V st w in M holds w, v
  are_orthogonal};
end;

theorem :: RUSUB_5:21
  for V being RealUnitarySpace, W being Subspace of V holds 0.V in Ort_Comp W;

theorem :: RUSUB_5:22
  for V being RealUnitarySpace holds Ort_Comp (0).V = (Omega).V;

theorem :: RUSUB_5:23
  for V being RealUnitarySpace holds Ort_Comp (Omega).V = (0).V;

theorem :: RUSUB_5:24
  for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of
  V st v <> 0.V holds v in W implies not v in Ort_Comp W;

theorem :: RUSUB_5:25
  for V being RealUnitarySpace, M being non empty Subset of V
  holds M c= the carrier of Ort_Comp (Ort_Comp M);

theorem :: RUSUB_5:26
  for V being RealUnitarySpace, M,N being non empty Subset of V st
  M c= N holds the carrier of Ort_Comp N c= the carrier of Ort_Comp M;

theorem :: RUSUB_5:27
  for V being RealUnitarySpace, W being Subspace of V, M being non
  empty Subset of V st M = the carrier of W holds Ort_Comp M = Ort_Comp W;

theorem :: RUSUB_5:28
  for V being RealUnitarySpace, M being non empty Subset of V holds
  Ort_Comp M = Ort_Comp (Ort_Comp (Ort_Comp M));

theorem :: RUSUB_5:29
  for V being RealUnitarySpace, x,y being VECTOR of V holds ||.x +
y.||^2 = ||.x.||^2 + 2 * x .|. y + ||.y.||^2 & ||.x - y.||^2 = ||.x.||^2 - 2 *
  x .|. y + ||.y.||^2;

theorem :: RUSUB_5:30
  for V being RealUnitarySpace, x,y being VECTOR of V st x,y
  are_orthogonal holds ||.x+y.||^2 = ||.x.||^2 + ||.y.||^2;

:: Parallelogram Law

theorem :: RUSUB_5:31
  for V being RealUnitarySpace, x,y being VECTOR of V holds ||.x+y.||^2
  + ||.x-y.||^2 = 2*||.x.||^2 + 2*||.y.||^2;

theorem :: RUSUB_5:32
  for V being RealUnitarySpace, v being VECTOR of V ex W being Subspace
  of V st the carrier of W = {u where u is VECTOR of V : u .|. v = 0};

begin  :: Topology of Real Unitary Space

definition
  let V be RealUnitarySpace;
  func Family_open_set(V) -> Subset-Family of V means
:: RUSUB_5:def 5

  for M being Subset of V holds M in it
   iff for x being Point of V st x in M
   ex r being Real st r>0 & Ball(x,r) c= M;
end;

theorem :: RUSUB_5:33
  for V being RealUnitarySpace, v being Point of V, r,p being Real
  st r <= p holds Ball(v,r) c= Ball(v,p);

theorem :: RUSUB_5:34
  for V being RealUnitarySpace, v being Point of V
   ex r being Real st r>0 & Ball(v,r) c= the carrier of V;

theorem :: RUSUB_5:35
  for V being RealUnitarySpace, v,u being Point of V, r being Real
  st u in Ball(v,r)
   ex p being Real st p>0 & Ball(u,p) c= Ball(v,r);

theorem :: RUSUB_5:36
  for V being RealUnitarySpace, u,v,w being Point of V,
      r,p being Real
st v in Ball(u,r) /\ Ball(w,p)
  ex q being Real st Ball(v,q) c= Ball(u,r)
  & Ball(v,q) c= Ball(w,p);

theorem :: RUSUB_5:37
  for V being RealUnitarySpace, v being Point of V, r being Real
  holds Ball(v,r) in Family_open_set(V);

theorem :: RUSUB_5:38
  for V being RealUnitarySpace holds the carrier of V in Family_open_set(V);

theorem :: RUSUB_5:39
  for V being RealUnitarySpace, M,N being Subset of V st M in
Family_open_set(V) & N in Family_open_set(V) holds M /\ N in Family_open_set(V)
;

theorem :: RUSUB_5:40
  for V being RealUnitarySpace, A being Subset-Family of V st A c=
  Family_open_set(V) holds union A in Family_open_set(V);

theorem :: RUSUB_5:41
  for V being RealUnitarySpace holds TopStruct (#the carrier of V,
    Family_open_set(V)#) is TopSpace;

definition
  let V be RealUnitarySpace;
  func TopUnitSpace V -> TopStruct equals
:: RUSUB_5:def 6
  TopStruct (#the carrier of V,
    Family_open_set(V)#);
end;

registration
  let V be RealUnitarySpace;
  cluster TopUnitSpace V -> TopSpace-like;
end;

registration
  let V be RealUnitarySpace;
  cluster TopUnitSpace V -> non empty;
end;

theorem :: RUSUB_5:42
  for V being RealUnitarySpace, M being Subset of TopUnitSpace V st M =
  [#]V holds M is open & M is closed;

theorem :: RUSUB_5:43
  for V being RealUnitarySpace, M being Subset of TopUnitSpace V st M =
  {}V holds M is open & M is closed;

theorem :: RUSUB_5:44
  for V being RealUnitarySpace, v being VECTOR of V, r being Real st the
  carrier of V = {0.V} & r <> 0 holds Sphere(v,r) is empty;

theorem :: RUSUB_5:45
  for V being RealUnitarySpace, v being VECTOR of V, r being Real st the
  carrier of V <> {0.V} & r > 0 holds Sphere(v,r) is non empty;

theorem :: RUSUB_5:46
  for V being RealUnitarySpace, v being VECTOR of V, r being Real st r =
  0 holds Ball(v,r) is empty;

theorem :: RUSUB_5:47
  for V being RealUnitarySpace, v being VECTOR of V, r being Real st the
  carrier of V = {0.V} & r > 0 holds Ball(v,r) = {0.V};

theorem :: RUSUB_5:48
  for V being RealUnitarySpace, v being VECTOR of V, r being Real st the
carrier of V <> {0.V} & r > 0 ex w being VECTOR of V st w <> v & w in Ball(v,r)
;

theorem :: RUSUB_5:49
  for V being RealUnitarySpace holds the carrier of V = the carrier of
  TopUnitSpace V & the topology of TopUnitSpace V = Family_open_set V;

theorem :: RUSUB_5:50
  for V being RealUnitarySpace, M being Subset of TopUnitSpace(V),
  r being Real, v being Point of V st M = Ball(v,r) holds M is open;

theorem :: RUSUB_5:51
  for V being RealUnitarySpace, M being Subset of TopUnitSpace(V) holds
M is open iff
  for v being Point of V st v in M ex r being Real st r>0 & Ball(v,
  r) c= M;

theorem :: RUSUB_5:52
  for V being RealUnitarySpace, v1,v2 being Point of V, r1,r2 being Real
ex u being Point of V, r being Real st Ball(v1,r1) \/ Ball(v2,r2) c= Ball(u,r);

theorem :: RUSUB_5:53  :: TOPREAL6:65
  for V being RealUnitarySpace, M being Subset of TopUnitSpace V,
  v being VECTOR of V, r being Real st M = cl_Ball(v,r) holds M is closed;

theorem :: RUSUB_5:54
  for V being RealUnitarySpace, M being Subset of TopUnitSpace V, v
  being VECTOR of V, r being Real st M = Sphere(v,r) holds M is closed;