The abstract of the Mizar article:

Topology of Real Unitary Space

by

Noboru Endou,

Takashi Mitsuishi, and

Yasunari Shidama

Received October 25, 2002

MML identifier: RUSUB_5

[ Mizar article, MML identifier index ]

environ

 vocabulary RLVECT_1, RLSUB_1, BOOLE, ARYTM_1, TARSKI, RLVECT_3, BHSP_1,
      SUBSET_1, RUSUB_4, ARYTM_3, RUSUB_5, PROB_2, PRE_TOPC, NORMSP_1,
      SQUARE_1, METRIC_1, ABSVALUE, PCOMPS_1, SETFAM_1, ARYTM;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XREAL_0, REAL_1, ABSVALUE,
      PRE_TOPC, STRUCT_0, RLVECT_1, RLSUB_1, SQUARE_1, BHSP_1, BHSP_2, RUSUB_1,
      RUSUB_3, RUSUB_4;
 constructors REAL_1, RLVECT_2, DOMAIN_1, RLVECT_3, RUSUB_3, PRE_TOPC, RUSUB_4,
      SQUARE_1, BHSP_2, ABSVALUE, MEMBERED;
 clusters SUBSET_1, STRUCT_0, XREAL_0, PRE_TOPC, RLVECT_1, RUSUB_4, COMPLSP1,
      TOPS_1, MEMBERED, ZFMISC_1;
 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_complementable(non 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 LoopStr,
 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 LoopStr, 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 LoopStr, M,N being non empty Subset of V holds
 M + N is non empty;

theorem :: RUSUB_5:7
  for V being non empty LoopStr, 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 LoopStr, 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 LoopStr), 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 LoopStr), 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 LoopStr), 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

scheme SubFamExU {A() -> UNITSTR, P[Subset of A()]}:
   ex F being Subset-Family of A() st
   for B being Subset of A() holds B in F iff P[B];

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

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

definition
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;