:: Introduction to Real Linear Topological Spaces
::  by Czes{\l}aw Byli\'nski
::
:: Received October 6, 2004
:: Copyright (c) 2004-2021 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;