:: Introduction to Real Linear Topological Spaces
:: by Czes{\l}aw Byli\'nski
::
:: Received October 6, 2004
:: Copyright (c) 2004-2018 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, REAL_1, XBOOLE_0, RLVECT_1, SUBSET_1, PRE_TOPC, RELAT_1,
XCMPLX_0, SETFAM_1, TARSKI, ALGSTR_0, ARYTM_3, ZFMISC_1, STRUCT_0,
SUPINF_2, ARYTM_1, CONNSP_2, TOPS_1, CONVEX1, CARD_1, XXREAL_0, RELAT_2,
COMPLEX1, BINOP_1, FUNCT_1, RCOMP_1, ORDINAL2, TOPS_2, YELLOW13,
XXREAL_2, FINSET_1, RVSUM_1, EQREL_1, COMPTS_1, RLTOPSP1, FUNCT_2,
INCSP_1, AFF_1, PENCIL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, SETFAM_1, ORDINAL1,
NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, RELAT_1, FUNCT_1,
RELSET_1, FUNCT_2, BINOP_1, REAL_1, EQREL_1, DOMAIN_1, STRUCT_0,
ALGSTR_0, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_2, COMPTS_1, YELLOW13,
RLVECT_1, RUSUB_4, CONVEX1;
constructors SETFAM_1, BINOP_1, DOMAIN_1, XXREAL_0, REAL_1, COMPLEX1, EQREL_1,
TOPS_1, TOPS_2, CONNSP_2, RUSUB_4, CONVEX1, URYSOHN1, YELLOW13, COMPTS_1,
RELSET_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELSET_1, PARTFUN1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, STRUCT_0, TOPS_1, RLVECT_1, CONVEX1, TOPGRP_1,
ORDINAL1, BORSUK_1, COMPTS_1, PRE_TOPC, FUNCT_2, ANPROJ_1;
requirements BOOLE, REAL, NUMERALS, SUBSET, ARITHM;
begin :: Preliminaries
reserve r,s,t,u for Real;
theorem :: RLTOPSP1:1
for X being non empty RLSStruct, M being Subset of X, x being Point of
X, r being Real st x in M holds r*x in r*M;
registration
cluster non zero for Real;
end;
theorem :: RLTOPSP1:2
for T being non empty TopSpace, X being non empty Subset of T, FX
being Subset-Family of T st FX is Cover of X for x being Point of T st x in X
ex W being Subset of T st x in W & W in FX;
theorem :: RLTOPSP1:3
for X being non empty addLoopStr, M,N being Subset of X, x,y
being Point of X st x in M & y in N holds x+y in M+N;
theorem :: RLTOPSP1:4
for X being non empty addLoopStr, M,N being Subset of X, F being
Subset-Family of X st F = {x+N where x is Point of X: x in M} holds M+N = union
F;
theorem :: RLTOPSP1:5
for X being add-associative right_zeroed right_complementable
non empty addLoopStr, M being Subset of X holds 0.X+M = M;
theorem :: RLTOPSP1:6
for X being add-associative non empty addLoopStr,x,y being
Point of X, M being Subset of X holds x+y+M = x+(y+M);
theorem :: RLTOPSP1:7
for X being add-associative non empty addLoopStr, x being Point
of X, M,N being Subset of X holds x+M+N = x+(M+N);
theorem :: RLTOPSP1:8
for X being non empty addLoopStr, M,N being Subset of X, x being
Point of X st M c= N holds x+M c= x+N;
theorem :: RLTOPSP1:9
for X being add-associative right_zeroed right_complementable
non empty addLoopStr, M being Subset of X, x being Point of X st x in M holds
0.X in -x+M;
theorem :: RLTOPSP1:10
for X being non empty addLoopStr, M,N,V being Subset of X st M
c= N holds M+V c= N+V;
theorem :: RLTOPSP1:11
for X being non empty addLoopStr, V1,V2,W1,W2 being Subset of X
st V1 c= W1 & V2 c= W2 holds V1+V2 c= W1+W2;
theorem :: RLTOPSP1:12
for X being right_zeroed non empty addLoopStr, V1,V2 being
Subset of X st 0.X in V2 holds V1 c= V1+V2;
theorem :: RLTOPSP1:13
for X being RealLinearSpace, r being Real holds r*{0.X} = {0.X};
theorem :: RLTOPSP1:14
for X being RealLinearSpace, M being Subset of X, r being non zero
Real st 0.X in r*M holds 0.X in M;
theorem :: RLTOPSP1:15
for X being RealLinearSpace, M,N being Subset of X, r being non
zero Real holds (r * M) /\ (r * N) = r * (M /\ N);
theorem :: RLTOPSP1:16
for X being non empty TopSpace, x being Point of X, A being
a_neighborhood of x, B being Subset of X st A c= B holds B is a_neighborhood of
x;
definition
let V be RealLinearSpace, M be Subset of V;
redefine attr M is convex means
:: RLTOPSP1:def 1
for u,v being Point of V, r being Real
st 0 <= r & r <= 1 & u in M & v in M holds r*u + (1-r)*v in M;
end;
registration
let X be RealLinearSpace, M be empty Subset of X;
cluster conv(M) -> empty;
end;
theorem :: RLTOPSP1:17
for X being RealLinearSpace, M being convex Subset of X holds conv(M) = M;
theorem :: RLTOPSP1:18
for X being RealLinearSpace, M being Subset of X, r being Real
holds r*conv(M) = conv(r*M);
theorem :: RLTOPSP1:19
for X being RealLinearSpace, M1,M2 being Subset of X st M1 c= M2
holds Convex-Family M2 c= Convex-Family M1;
theorem :: RLTOPSP1:20
for X being RealLinearSpace, M1,M2 being Subset of X st M1 c= M2
holds conv(M1) c= conv(M2);
theorem :: RLTOPSP1:21
for X being RealLinearSpace, M being convex Subset of X, r being Real
st 0 <= r & r <= 1 & 0.X in M holds r*M c= M;
definition
let X be RealLinearSpace, v,w be Point of X;
func LSeg(v,w) -> Subset of X equals
:: RLTOPSP1:def 2
{(1-r)*v + r*w : 0 <= r & r <= 1 };
commutativity;
end;
registration
let X be RealLinearSpace, v,w be Point of X;
cluster LSeg(v,w) -> non empty convex;
end;
theorem :: RLTOPSP1:22
for X being RealLinearSpace, M being Subset of X holds M is convex iff
for u,w being Point of X st u in M & w in M holds LSeg(u,w) c= M;
definition
let V be non empty RLSStruct, P be Subset-Family of V;
attr P is convex-membered means
:: RLTOPSP1:def 3
for M being Subset of V st M in P holds M is convex;
end;
registration
let V be non empty RLSStruct;
cluster non empty convex-membered for Subset-Family of V;
end;
theorem :: RLTOPSP1:23
for V being non empty RLSStruct, F being convex-membered Subset-Family
of V holds meet F is convex;
definition
let X be non empty RLSStruct, A be Subset of X;
func -A -> Subset of X equals
:: RLTOPSP1:def 4
(-1)*A;
end;
theorem :: RLTOPSP1:24
for X being RealLinearSpace, M,N being Subset of X, v being
Point of X holds v+M meets N iff v in N+(-M);
definition
let X be non empty RLSStruct, A be Subset of X;
attr A is symmetric means
:: RLTOPSP1:def 5
A = -A;
end;
registration
let X be RealLinearSpace;
cluster non empty symmetric for Subset of X;
end;
theorem :: RLTOPSP1:25
for X being RealLinearSpace, A being symmetric Subset of X, x
being Point of X st x in A holds -x in A;
definition
let X be non empty RLSStruct, A be Subset of X;
attr A is circled means
:: RLTOPSP1:def 6
for r being Real st |.r.| <= 1 holds r*A c= A;
end;
registration
let X be non empty RLSStruct;
cluster empty -> circled for Subset of X;
end;
theorem :: RLTOPSP1:26
for X being RealLinearSpace holds {0.X} is circled;
registration
let X be RealLinearSpace;
cluster non empty circled for Subset of X;
end;
theorem :: RLTOPSP1:27
for X being RealLinearSpace, B being non empty circled Subset of
X holds 0.X in B;
registration
let X be RealLinearSpace, A,B be circled Subset of X;
cluster A+B -> circled;
end;
theorem :: RLTOPSP1:28
for X being RealLinearSpace, A being circled Subset of X for r
being Real st |.r.| = 1 holds r*A = A;
registration
let X be RealLinearSpace;
cluster circled -> symmetric for Subset of X;
end;
registration
let X be RealLinearSpace, M be circled Subset of X;
cluster conv(M) -> circled;
end;
definition
let X be non empty RLSStruct, F be Subset-Family of X;
attr F is circled-membered means
:: RLTOPSP1:def 7
for V being Subset of X st V in F holds V is circled;
end;
registration
let V be non empty RLSStruct;
cluster non empty circled-membered for Subset-Family of V;
end;
theorem :: RLTOPSP1:29
for X being non empty RLSStruct, F being circled-membered
Subset-Family of X holds union F is circled;
theorem :: RLTOPSP1:30
for X being non empty RLSStruct, F being circled-membered
Subset-Family of X holds meet F is circled;
begin
definition
struct(RLSStruct,TopStruct) RLTopStruct (# carrier -> set, ZeroF -> Element
of the carrier, addF -> BinOp of the carrier, Mult -> Function of [:REAL, the
carrier:],the carrier, topology -> Subset-Family of the carrier #);
end;
registration
let X be non empty set, O be Element of X, F be BinOp of X, G be Function of
[:REAL,X:],X, T be Subset-Family of X;
cluster RLTopStruct (# X,O,F,G,T #) -> non empty;
end;
registration
cluster strict non empty for RLTopStruct;
end;
definition
let X be non empty RLTopStruct;
attr X is add-continuous means
:: RLTOPSP1:def 8
for x1,x2 being Point of X, V being
Subset of X st V is open & x1+x2 in V ex V1,V2 being Subset of X st V1 is open
& V2 is open & x1 in V1 & x2 in V2 & V1+V2 c= V;
attr X is Mult-continuous means
:: RLTOPSP1:def 9
for a being Real, x being Point of X,
V being Subset of X st V is open & a*x in V
ex r being positive Real, W being Subset of X st W is open & x in W &
for s being Real st |.s-a.| < r holds s*W c= V;
end;
registration
cluster strict add-continuous Mult-continuous TopSpace-like Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital for non
empty RLTopStruct;
end;
definition
mode LinearTopSpace is add-continuous Mult-continuous TopSpace-like Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital
non empty RLTopStruct;
end;
theorem :: RLTOPSP1:31
for X being LinearTopSpace, x1,x2 being Point of X, V being
a_neighborhood of x1+x2 ex V1 being a_neighborhood of x1, V2 being
a_neighborhood of x2 st V1+V2 c= V;
theorem :: RLTOPSP1:32
for X being LinearTopSpace, a being Real, x being Point of X, V
being a_neighborhood of a*x
ex r being positive Real, W being a_neighborhood of
x st for s being Real st |.s-a.| < r holds s*W c= V;
definition
let X be non empty RLTopStruct, a be Point of X;
func transl(a,X) -> Function of X,X means
:: RLTOPSP1:def 10
for x being Point of X holds it.x = a+x;
end;
theorem :: RLTOPSP1:33
for X being non empty RLTopStruct, a being Point of X, V being
Subset of X holds transl(a,X).:V = a+V;
theorem :: RLTOPSP1:34
for X being LinearTopSpace, a being Point of X holds rng transl( a,X) = [#]X;
theorem :: RLTOPSP1:35
for X being LinearTopSpace, a being Point of X holds transl(a,X)
" = transl(-a,X);
registration
let X be LinearTopSpace, a be Point of X;
cluster transl(a,X) -> being_homeomorphism;
end;
registration
let X be LinearTopSpace, E be open Subset of X, x be Point of X;
cluster x+E -> open;
end;
registration
let X be LinearTopSpace, E be open Subset of X, K be Subset of X;
cluster K+E -> open;
end;
registration
let X be LinearTopSpace, D be closed Subset of X, x be Point of X;
cluster x+D -> closed;
end;
theorem :: RLTOPSP1:36
for X being LinearTopSpace, V1,V2,V being Subset of X st V1+V2
c= V holds Int V1 + Int V2 c= Int V;
theorem :: RLTOPSP1:37
for X being LinearTopSpace, x being Point of X, V being Subset
of X holds x+Int(V) = Int(x+V);
theorem :: RLTOPSP1:38
for X being LinearTopSpace, x being Point of X, V being Subset of X
holds x+Cl(V) = Cl(x+V);
theorem :: RLTOPSP1:39
for X being LinearTopSpace, x,v being Point of X, V being
a_neighborhood of x holds v+V is a_neighborhood of v+x;
theorem :: RLTOPSP1:40
for X being LinearTopSpace, x being Point of X, V being a_neighborhood
of x holds -x+V is a_neighborhood of 0.X;
definition
let X be non empty RLTopStruct;
mode local_base of X is basis of 0.X;
end;
definition
let X be non empty RLTopStruct;
attr X is locally-convex means
:: RLTOPSP1:def 11
ex P being local_base of X st P is convex-membered;
end;
definition
let X be LinearTopSpace, E be Subset of X;
attr E is bounded means
:: RLTOPSP1:def 12
for V being a_neighborhood of 0.X ex s st s
> 0 & for t st t > s holds E c= t*V;
end;
registration
let X be LinearTopSpace;
cluster empty -> bounded for Subset of X;
end;
registration
let X be LinearTopSpace;
cluster bounded for Subset of X;
end;
theorem :: RLTOPSP1:41
for X being LinearTopSpace, V1,V2 being bounded Subset of X
holds V1 \/ V2 is bounded;
theorem :: RLTOPSP1:42
for X being LinearTopSpace, P being bounded Subset of X, Q being
Subset of X st Q c= P holds Q is bounded;
theorem :: RLTOPSP1:43
for X being LinearTopSpace, F being Subset-Family of X st F is finite
& F = the set of all P where P is bounded Subset of X holds union F is
bounded;
theorem :: RLTOPSP1:44
for X being LinearTopSpace, P being Subset-Family of X st P = the set of all
U
where U is a_neighborhood of 0.X holds P is local_base of X;
theorem :: RLTOPSP1:45
for X being LinearTopSpace, O being local_base of X, P being
Subset-Family of X st P = {a+U where a is Point of X, U is Subset of X: U in O}
holds P is basis of X;
definition
let X be non empty RLTopStruct, r be Real;
func mlt(r,X) -> Function of X,X means
:: RLTOPSP1:def 13
for x being Point of X holds it.x = r*x;
end;
theorem :: RLTOPSP1:46
for X being non empty RLTopStruct, V being Subset of X, r being
non zero Real holds mlt(r,X).:V = r*V;
theorem :: RLTOPSP1:47
for X being LinearTopSpace, r being non zero Real holds rng mlt( r,X) = [#]X;
theorem :: RLTOPSP1:48
for X being LinearTopSpace, r being non zero Real holds mlt(r,X)
" = mlt(r",X);
registration
let X be LinearTopSpace, r be non zero Real;
cluster mlt(r,X) -> being_homeomorphism;
end;
theorem :: RLTOPSP1:49
for X being LinearTopSpace, V being open Subset of X, r being
non zero Real holds r*V is open;
theorem :: RLTOPSP1:50
for X being LinearTopSpace, V being closed Subset of X, r being
non zero Real holds r*V is closed;
theorem :: RLTOPSP1:51
for X being LinearTopSpace, V being Subset of X, r be non zero
Real holds r*Int(V) = Int(r*V);
theorem :: RLTOPSP1:52
for X being LinearTopSpace, A being Subset of X, r being non
zero Real holds r*Cl(A) = Cl(r*A);
theorem :: RLTOPSP1:53
for X being LinearTopSpace,A being Subset of X st X is T_1 holds 0*Cl(
A) = Cl(0*A);
theorem :: RLTOPSP1:54
for X being LinearTopSpace, x being Point of X, V being
a_neighborhood of x, r be non zero Real
holds r*V is a_neighborhood of r*x;
theorem :: RLTOPSP1:55
for X being LinearTopSpace, V being a_neighborhood of 0.X, r be
non zero Real holds r*V is a_neighborhood of 0.X;
registration
let X be LinearTopSpace, V be bounded Subset of X, r be Real;
cluster r*V -> bounded;
end;
theorem :: RLTOPSP1:56
for X being LinearTopSpace, W being a_neighborhood of 0.X ex U
being open a_neighborhood of 0.X st U is symmetric & U+U c= W;
theorem :: RLTOPSP1:57
for X being LinearTopSpace, K being compact Subset of X, C being
closed Subset of X st K misses C ex V being a_neighborhood of 0.X st K+V misses
C+V;
theorem :: RLTOPSP1:58
for X being LinearTopSpace, B being local_base of X, V being
a_neighborhood of 0.X ex W being a_neighborhood of 0.X st W in B & Cl W c= V;
theorem :: RLTOPSP1:59
for X being LinearTopSpace, V being a_neighborhood of 0.X ex W
being a_neighborhood of 0.X st Cl W c= V;
registration
cluster T_1 -> Hausdorff for LinearTopSpace;
end;
theorem :: RLTOPSP1:60
for X being LinearTopSpace, A being Subset of X holds Cl A = meet the set of
all A+V
where V is a_neighborhood of 0.X;
theorem :: RLTOPSP1:61
for X being LinearTopSpace, A,B being Subset of X holds Int A +
Int B c= Int(A+B);
theorem :: RLTOPSP1:62
for X being LinearTopSpace, A,B being Subset of X holds Cl A +
Cl B c= Cl(A+B);
registration
let X be LinearTopSpace, C be convex Subset of X;
cluster Cl C -> convex;
end;
registration
let X be LinearTopSpace, C be convex Subset of X;
cluster Int C -> convex;
end;
registration
let X be LinearTopSpace, B be circled Subset of X;
cluster Cl B -> circled;
end;
theorem :: RLTOPSP1:63
for X being LinearTopSpace, B being circled Subset of X st 0.X in Int
B holds Int B is circled;
registration
let X be LinearTopSpace, E be bounded Subset of X;
cluster Cl E -> bounded;
end;
theorem :: RLTOPSP1:64
for X being LinearTopSpace, U being a_neighborhood of 0.X ex W
being a_neighborhood of 0.X st W is circled & W c= U;
theorem :: RLTOPSP1:65
for X being LinearTopSpace, U being a_neighborhood of 0.X st U
is convex ex W being a_neighborhood of 0.X st W is circled convex & W c= U;
theorem :: RLTOPSP1:66
for X being LinearTopSpace ex P being local_base of X st P is
circled-membered;
theorem :: RLTOPSP1:67
for X being LinearTopSpace st X is locally-convex ex P being
local_base of X st P is convex-membered;
begin :: Addenda
:: segments in a real vector space, 2009.04.01- A.T.
reserve V for RealLinearSpace,
v,w for Point of V;
theorem :: RLTOPSP1:68 :: TOPREAL1:6
v in LSeg(v,w);
theorem :: RLTOPSP1:69 :: GOBOARD7:7
1/2*(v+w) in LSeg(v,w);
theorem :: RLTOPSP1:70 :: TOPREAL1:7
LSeg(v,v) = {v};
theorem :: RLTOPSP1:71 :: JORDAN2C:47
0.V in LSeg(v,w) implies ex r st v = r*w or w = r*v;
:: from EUCLID_4 (generalized), A.T.
definition
let V,v,w;
func Line(v,w) -> Subset of V equals
:: RLTOPSP1:def 14
the set of all (1-r)*v + r*w ;
commutativity;
end;
theorem :: RLTOPSP1:72
v in Line(v,w);
registration
let V,v,w;
cluster Line(v,w) -> non empty;
end;
theorem :: RLTOPSP1:73
LSeg(v,w) c= Line(v,w);
reserve x1,x2,x3,x4,y1,y2 for Element of V;
theorem :: RLTOPSP1:74
y1 in Line(x1,x2) & y2 in Line(x1,x2) implies Line(y1,y2) c= Line(x1,x2);
theorem :: RLTOPSP1:75
y1 in Line(x1,x2) & y2 in Line(x1,x2) & y1 <> y2 implies
Line(y1,y2) = Line(x1,x2);
:: 12.11.28, A.T.
definition
let V;
let A be Subset of V;
attr A is being_line means
:: RLTOPSP1:def 15
ex x1,x2 st A=Line(x1,x2);
end;
registration let V;
cluster being_line for Subset of V;
end;
registration let V be non trivial RealLinearSpace;
cluster non trivial being_line for Subset of V;
end;
definition let V;
mode line of V is being_line Subset of V;
end;
definition let V;
let x1,x2,x3 be Point of V;
pred x1,x2,x3 are_collinear means
:: RLTOPSP1:def 16
ex L being line of V st x1 in L & x2 in L & x3 in L;
end;
definition let V;
let x1,x2,x3,x4 be Point of V;
pred x1,x2,x3,x4 are_collinear means
:: RLTOPSP1:def 17
ex L being line of V st x1 in L & x2 in L & x3 in L & x4 in L;
end;
theorem :: RLTOPSP1:76
for x being object st x in LSeg(v,w)
ex r st 0<=r & r<=1 & x=(1-r)*v+r*w;
theorem :: RLTOPSP1:77
Line(v,v) = {v};
registration let V,v;
cluster {v} -> being_line for Subset of V;
let w;
cluster Line(v,w) -> being_line;
end;
theorem :: RLTOPSP1:78
for V being non trivial RealLinearSpace, L being non trivial line of V
ex p,q being Point of V st p <> q & L = Line(p,q);
theorem :: RLTOPSP1:79
for x1,x2,x3,x4 be Point of V st x1,x2,x3,x4 are_collinear
holds x1,x2,x3 are_collinear & x1,x2,x4 are_collinear;
theorem :: RLTOPSP1:80
for L being line of V, x1,x2 st x1 <> x2 & x1 in L & x2 in L
holds L = Line(x1,x2);
theorem :: RLTOPSP1:81
for x1,x2,x3,x4 be Point of V
st x1 <> x2 & x1,x2,x3 are_collinear & x1,x2,x4 are_collinear
holds x1,x2,x3,x4 are_collinear;