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;