:: Topology of Real Unitary Space
:: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama
::
:: Received October 25, 2002
:: Copyright (c) 2002-2016 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;