Volume 14, 2002

University of Bialystok

Copyright (c) 2002 Association of Mizar Users

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

Back to top