Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users

### Topology of Real Unitary Space

by
Noboru Endou,
Takashi Mitsuishi, and
Yasunari Shidama

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