:: Baire's Category Theorem and Some Spaces Generated from Real Normed Space
::  by Noboru Endou , Yasunari Shidama and Katsumasa Okamura
::
:: Received November 21, 2006
:: Copyright (c) 2006-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, XBOOLE_0, METRIC_1, PROB_1, REWRITE1, TARSKI, RELAT_1,
      STRUCT_0, SUBSET_1, FUNCT_1, PCOMPS_1, REAL_1, PRE_TOPC, CARD_1, ARYTM_3,
      NEWTON, XXREAL_0, NAT_1, SEQ_1, ZFMISC_1, MCART_1, ARYTM_1, BHSP_3,
      SEQ_2, ORDINAL2, NORMSP_1, RELAT_2, ORDINAL1, METRIC_6, RCOMP_1,
      COMPTS_1, WAYBEL_3, YELLOW_8, FRECHET, CONNSP_2, PARTFUN1, FCONT_1,
      TMAP_1, CFCONT_1, RLTOPSP1, SUPINF_2, ALGSTR_0, RLVECT_1, SETFAM_1,
      COMPLEX1, RLVECT_3, CARD_3, NORMSP_2, FUNCT_7;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, ORDINAL1, NUMBERS,
      XCMPLX_0, XREAL_0, XXREAL_0, SETFAM_1, RELSET_1, PARTFUN1, FUNCT_2,
      BINOP_1, COMPLEX1, REAL_1, NAT_1, STRUCT_0, ALGSTR_0, PRE_TOPC, FRECHET,
      NEWTON, FRECHET2, YELLOW_8, DOMAIN_1, WAYBEL_3, RLVECT_1, CONVEX1,
      COMPTS_1, TBSP_1, TMAP_1, CONNSP_2, CARD_3, METRIC_1, METRIC_6, PCOMPS_1,
      RUSUB_4, RLTOPSP1, NFCONT_1, SEQ_1, KURATO_2, NORMSP_0, NORMSP_1;
 constructors SETFAM_1, DOMAIN_1, REAL_1, SQUARE_1, NEWTON, CONNSP_2, TBSP_1,
      RUSUB_4, CONVEX1, TMAP_1, METRIC_6, WAYBEL_3, YELLOW_8, FRECHET,
      FRECHET2, NFCONT_1, RLTOPSP1, RELSET_1, TOPS_2, BINOP_1, VFUNCT_1;
 registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0,
      STRUCT_0, TOPS_1, METRIC_1, PCOMPS_1, HAUSDORF, KURATO_2, RLTOPSP1,
      FRECHET, NEWTON, NAT_1, XTUPLE_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: Baire's Category Theorem

theorem :: NORMSP_2:1
  for X be non empty MetrSpace, Y be SetSequence of X st X is complete &
  union rng Y = the carrier of X & for n be Nat holds (Y.n)` in
Family_open_set X holds ex n0 be Nat,
    r be Real, x0 be Point of X st
  0 < r & Ball(x0,r) c= Y.n0;

begin :: Metric Space generated from Real Normed Space

reserve X for RealNormSpace;

definition
  let X be RealNormSpace;
  func distance_by_norm_of X -> Function of [:the carrier of X,the carrier of
  X:],REAL means
:: NORMSP_2:def 1

  for x, y be Point of X holds it.(x,y) = ||.x-y.||;
end;

definition
  let X be RealNormSpace;
  func MetricSpaceNorm X -> non empty MetrSpace equals
:: NORMSP_2:def 2
  MetrStruct(# the
    carrier of X,distance_by_norm_of X #);
end;

theorem :: NORMSP_2:2
  for X be RealNormSpace, z be Element of MetricSpaceNorm X, r be
Real holds ex x be Point of X st x = z & Ball(z,r) = {y where y is Point
  of X:||.x-y.|| < r};

theorem :: NORMSP_2:3
  for X be RealNormSpace, z be Element of MetricSpaceNorm X, r be
  Real holds ex x be Point of X st x = z & cl_Ball(z,r) = {y where y is
  Point of X: ||.x-y.|| <= r};

theorem :: NORMSP_2:4
  for X be RealNormSpace, S be sequence of X, St be sequence of
MetricSpaceNorm X, x be Point of X, xt be Point of MetricSpaceNorm X st S = St
  & x = xt holds St is_convergent_in_metrspace_to xt iff
  for r be Real st 0 < r
  ex m be Nat st for n be Nat st m <= n holds ||. S.n - x
  .|| < r;

theorem :: NORMSP_2:5
  for X be RealNormSpace, S be sequence of X, St be sequence of
  MetricSpaceNorm X st S = St holds St is convergent iff S is convergent;

theorem :: NORMSP_2:6
  for X be RealNormSpace, S be sequence of X, St be sequence of
  MetricSpaceNorm X st S = St & St is convergent holds lim St = lim S;

begin :: Topological Space generated from Real Normed Space

definition
  let X be RealNormSpace;
  func TopSpaceNorm X -> non empty TopSpace equals
:: NORMSP_2:def 3
  TopSpaceMetr
  MetricSpaceNorm X;
end;

theorem :: NORMSP_2:7
  for X be RealNormSpace, V be Subset of TopSpaceNorm X holds V is
  open iff for x be Point of X st x in V
 ex r be Real st r>0 & {y where y
  is Point of X: ||.x-y.|| < r} c= V;

theorem :: NORMSP_2:8
  for X be RealNormSpace, x be Point of X,
      r be Real holds {y where
  y is Point of X:||.x-y.|| < r} is open Subset of TopSpaceNorm X;

theorem :: NORMSP_2:9
  for X be RealNormSpace, x be Point of X, r be Real
  holds {y where y is
  Point of X: ||.x-y.|| <= r} is closed Subset of TopSpaceNorm X;

::$N Baire Category Theorem (Hausdorff spaces)
theorem :: NORMSP_2:10
  for X be Hausdorff non empty TopSpace st X is locally-compact holds X
  is Baire;

theorem :: NORMSP_2:11
  for X be RealNormSpace holds TopSpaceNorm(X) is sequential;

registration
  let X be RealNormSpace;
  cluster TopSpaceNorm(X) -> sequential;
end;

theorem :: NORMSP_2:12
  for X be RealNormSpace, S be sequence of X, St be sequence of
TopSpaceNorm X, x be Point of X, xt be Point of TopSpaceNorm X st S = St & x =
  xt holds St is_convergent_to xt iff
 for r be Real st 0 < r ex m be Nat
   st for n be Nat st m <= n holds ||. S.n - x.|| < r;

theorem :: NORMSP_2:13
  for X be RealNormSpace, S be sequence of X, St be sequence of
  TopSpaceNorm X st S = St holds St is convergent iff S is convergent;

theorem :: NORMSP_2:14
  for X be RealNormSpace, S be sequence of X, St be sequence of
TopSpaceNorm X st S = St & St is convergent holds Lim St = {lim S} & lim St=lim
  S;

theorem :: NORMSP_2:15
  for X be RealNormSpace, V be Subset of X, Vt be Subset of
  TopSpaceNorm X st V = Vt holds V is closed iff Vt is closed;

theorem :: NORMSP_2:16
  for X be RealNormSpace, V be Subset of X, Vt be Subset of
  TopSpaceNorm X st V = Vt holds V is open iff Vt is open;

theorem :: NORMSP_2:17
  for X be RealNormSpace, U be Subset of X, Ut be Subset of
TopSpaceNorm X, x be Point of X, xt be Point of TopSpaceNorm X st U = Ut & x =
  xt holds U is Neighbourhood of x iff Ut is a_neighborhood of xt;

theorem :: NORMSP_2:18
  for X,Y be RealNormSpace, f be PartFunc of X,Y, ft be Function
of TopSpaceNorm X,TopSpaceNorm Y, x be Point of X, xt be Point of TopSpaceNorm
  X st f = ft & x = xt holds f is_continuous_in x iff ft is_continuous_at xt;

theorem :: NORMSP_2:19
  for X,Y be RealNormSpace, f be PartFunc of X,Y, ft be Function of
TopSpaceNorm X,TopSpaceNorm Y st f = ft holds f is_continuous_on the carrier of
  X iff ft is continuous;

begin :: Linear Topological Space generated from Real Normed Space

definition
  let X be RealNormSpace;
  func LinearTopSpaceNorm X -> strict non empty RLTopStruct means
:: NORMSP_2:def 4

  the
carrier of it = the carrier of X & 0.it = 0.X & the addF of it = the addF of X
  & the Mult of it = the Mult of X & the topology of it = the topology of
  TopSpaceNorm X;
end;

registration
  let X be RealNormSpace;
  cluster LinearTopSpaceNorm X -> add-continuous Mult-continuous TopSpace-like
Abelian add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital;
end;

theorem :: NORMSP_2:20
  for X be RealNormSpace, V be Subset of TopSpaceNorm X, Vt be
  Subset of LinearTopSpaceNorm X st V=Vt holds V is open iff Vt is open;

theorem :: NORMSP_2:21
  for X be RealNormSpace, V be Subset of TopSpaceNorm X, Vt be
  Subset of LinearTopSpaceNorm X st V=Vt holds V is closed iff Vt is closed;

theorem :: NORMSP_2:22
  for X be RealNormSpace, V be Subset of LinearTopSpaceNorm X holds V is
  open iff for x be Point of X st x in V
 ex r be Real st r>0 & {y where y
  is Point of X:||.x-y.|| < r} c= V;

theorem :: NORMSP_2:23
  for X be RealNormSpace, x be Point of X, r be Real, V be Subset of
LinearTopSpaceNorm X st V = {y where y is Point of X:||.x-y.|| < r} holds V is
  open;

theorem :: NORMSP_2:24
  for X be RealNormSpace, x be Point of X, r be Real, V be Subset of
  TopSpaceNorm X st V = {y where y is Point of X:||.x-y.|| <= r} holds V is
  closed;

registration
  let X be RealNormSpace;
  cluster LinearTopSpaceNorm X -> T_2;
  cluster LinearTopSpaceNorm X -> sober;
end;

theorem :: NORMSP_2:25
  for X be RealNormSpace, S be Subset-Family of TopSpaceNorm X, St
  be Subset-Family of LinearTopSpaceNorm X, x be Point of TopSpaceNorm X, xt be
  Point of LinearTopSpaceNorm X st S=St & x=xt holds St is Basis of xt iff S is
  Basis of x;

registration
  let X be RealNormSpace;
  cluster LinearTopSpaceNorm X -> first-countable;
  cluster LinearTopSpaceNorm X -> Frechet;
  cluster LinearTopSpaceNorm X -> sequential;
end;

theorem :: NORMSP_2:26
  for X be RealNormSpace, S be sequence of TopSpaceNorm X, St be
sequence of LinearTopSpaceNorm X, x be Point of TopSpaceNorm X, xt be Point of
  LinearTopSpaceNorm X st S=St & x=xt holds St is_convergent_to xt iff S
  is_convergent_to x;

theorem :: NORMSP_2:27
  for X be RealNormSpace, S be sequence of TopSpaceNorm X, St be
  sequence of LinearTopSpaceNorm X st S=St holds St is convergent iff S is
  convergent;

theorem :: NORMSP_2:28
  for X be RealNormSpace, S be sequence of TopSpaceNorm X, St be
  sequence of LinearTopSpaceNorm X st S=St & St is convergent holds Lim S = Lim
  St & lim S = lim St;

theorem :: NORMSP_2:29
  for X be RealNormSpace, S be sequence of X, St be sequence of
LinearTopSpaceNorm X, x be Point of X, xt be Point of LinearTopSpaceNorm X st S
  =St & x=xt holds St is_convergent_to xt iff
 for r be Real st 0 < r ex m be
  Nat st for n be Nat st m <= n holds ||.(S.n) - x.|| < r;

theorem :: NORMSP_2:30
  for X be RealNormSpace, S be sequence of X, St be sequence of
  LinearTopSpaceNorm X st S=St holds St is convergent iff S is convergent;

theorem :: NORMSP_2:31
  for X be RealNormSpace, S be sequence of X, St be sequence of
LinearTopSpaceNorm X st S=St & St is convergent holds Lim St = {lim S} & lim St
  =lim S;

theorem :: NORMSP_2:32
  for X be RealNormSpace, V be Subset of X, Vt be Subset of
  LinearTopSpaceNorm X st V=Vt holds V is closed iff Vt is closed;

theorem :: NORMSP_2:33
  for X be RealNormSpace, V be Subset of X, Vt be Subset of
  LinearTopSpaceNorm X st V=Vt holds V is open iff Vt is open;

theorem :: NORMSP_2:34
  for X be RealNormSpace, U be Subset of TopSpaceNorm X, Ut be
  Subset of LinearTopSpaceNorm X, x be Point of TopSpaceNorm X, xt be Point of
  LinearTopSpaceNorm X st U=Ut & x=xt holds U is a_neighborhood of x iff Ut is
  a_neighborhood of xt;

theorem :: NORMSP_2:35
  for X,Y be RealNormSpace, f be Function of TopSpaceNorm X,
TopSpaceNorm Y, ft be Function of LinearTopSpaceNorm X,LinearTopSpaceNorm Y, x
be Point of TopSpaceNorm X, xt be Point of LinearTopSpaceNorm X st f=ft & x=xt
  holds f is_continuous_at x iff ft is_continuous_at xt;

theorem :: NORMSP_2:36
  for X,Y be RealNormSpace, f be Function of TopSpaceNorm X,TopSpaceNorm
Y, ft be Function of LinearTopSpaceNorm X,LinearTopSpaceNorm Y st f=ft holds f
  is continuous iff ft is continuous;