:: The Theorem of Weierstrass
::  by J\'ozef Bia\las and Yatsuka Nakamura
::
:: Received July 10, 1995
:: Copyright (c) 1995-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, METRIC_1, PRE_TOPC, REAL_1, XBOOLE_0, TARSKI, COMPLEX1,
      ARYTM_3, XXREAL_0, CARD_1, ARYTM_1, NAT_1, SETFAM_1, FINSEQ_1, TOPMETR,
      RELAT_1, FINSET_1, FUNCT_1, ORDINAL2, RCOMP_1, SUBSET_1, ZFMISC_1,
      EUCLID, XXREAL_2, STRUCT_0, PCOMPS_1, SEQ_1, SEQ_2, VALUED_0, SEQ_4,
      WEIERSTR;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2,
      BINOP_1, SETFAM_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1,
      REAL_1, NAT_1, TOPMETR, METRIC_1, COMPTS_1, SEQ_1, SEQ_2, VALUED_0,
      SEQ_4, FINSEQ_1, FINSET_1, STRUCT_0, PRE_TOPC, TOPS_2, RCOMP_1, EUCLID,
      PCOMPS_1, XXREAL_0, XXREAL_2;
 constructors REAL_1, COMPLEX1, SEQ_2, SEQ_4, RCOMP_1, TOPS_2, COMPTS_1,
      EUCLID, TOPMETR, BINOP_2, PCOMPS_1, COMSEQ_2, BINOP_1;
 registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, NUMBERS,
      XREAL_0, MEMBERED, STRUCT_0, METRIC_1, PCOMPS_1, EUCLID, TOPMETR,
      FINSEQ_1;
 requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM;


begin

theorem :: WEIERSTR:1
  for M being MetrSpace, x1,x2 being Point of M, r1,r2 being Real
ex x being Point of M, r being Real
   st Ball(x1,r1) \/ Ball(x2,r2) c= Ball(x,r);

theorem :: WEIERSTR:2
  for M being MetrSpace, n being Nat, F being Subset-Family of M, p
  being FinSequence st F is being_ball-family & rng p = F & dom p = Seg(n+1)
holds ex G being Subset-Family of M st (G is finite & G is being_ball-family &
ex q being FinSequence st rng q = G & dom q = Seg(n) & ex x being Point of M st
  ex r being Real st union F c= union G \/ Ball(x,r) );

theorem :: WEIERSTR:3
  for M being MetrSpace, F being Subset-Family of M st F is finite
  & F is being_ball-family holds ex x being Point of M, r being Real st union F
  c= Ball(x,r);

theorem :: WEIERSTR:4
  for T,S being non empty TopSpace, f being Function of T,S, B
  being Subset-Family of S st f is continuous & B is open holds f"B is open;

theorem :: WEIERSTR:5
  for T,S being non empty TopSpace holds for f being Function of T,S
  holds for Q being Subset-Family of S holds Q is finite implies f"Q is finite;

theorem :: WEIERSTR:6
  for T,S being non empty TopSpace holds for f being Function of T,S
  holds for P being Subset-Family of T holds P is finite implies f.:P is finite
;

theorem :: WEIERSTR:7
  for T,S being non empty TopSpace holds for f being Function of T
,S holds for P being Subset of T holds for F being Subset-Family of S holds (ex
  B being Subset-Family of T st (B c= f"F & B is Cover of P & B is finite))
  implies ex G being Subset-Family of S st G c= F & G is Cover of f.:P & G is
  finite;

begin

::
::                       The Weierstrass` theorem
::

theorem :: WEIERSTR:8
  for T,S being non empty TopSpace holds for f being Function of T
,S holds for P being Subset of T holds P is compact & f is continuous implies f
  .:P is compact;

theorem :: WEIERSTR:9
  for T being non empty TopSpace holds for f being Function of T,R^1
holds for P being Subset of T holds P is compact & f is continuous implies f.:P
  is compact;

theorem :: WEIERSTR:10
  for f being Function of TOP-REAL 2,R^1 holds for P being Subset of
TOP-REAL 2 holds P is compact & f is continuous implies f.:P is compact;

definition

  let P be Subset of R^1;
  func [#](P) -> Subset of REAL equals
:: WEIERSTR:def 1
  P;
end;

theorem :: WEIERSTR:11
  for P being Subset of R^1 holds P is compact implies [#](P) is real-bounded;

theorem :: WEIERSTR:12
  for P being Subset of R^1 holds P is compact implies [#](P) is closed;

theorem :: WEIERSTR:13
  for P being Subset of R^1 holds P is compact implies [#](P) is compact;

definition
  let P be Subset of R^1;
  func upper_bound(P) -> Real equals
:: WEIERSTR:def 2
  upper_bound([#](P));
  func lower_bound(P) -> Real equals
:: WEIERSTR:def 3
  lower_bound([#](P));
end;

::$N Extreme value theorem#Generalization to arbitrary topological spaces
theorem :: WEIERSTR:14
  for T being non empty TopSpace holds for f being Function of T,
  R^1 holds for P being Subset of T holds P <> {} & P is compact & f is
continuous implies ex x1 being Point of T st x1 in P & f.x1 = upper_bound(f.:P)
;

::$N Extreme value theorem#Generalization to arbitrary topological spaces
theorem :: WEIERSTR:15
  for T being non empty TopSpace holds for f being Function of T,
  R^1 holds for P being Subset of T holds P <> {} & P is compact & f is
continuous implies ex x2 being Point of T st x2 in P & f.x2 = lower_bound(f.:P)
;

begin

::
::           The measure of the distance between compact sets
::

definition
  let M be non empty MetrSpace;
  let x be Point of M;
  func dist(x) -> Function of TopSpaceMetr(M),R^1 means
:: WEIERSTR:def 4

  for y being Point of M holds it.y = dist(y,x);
end;

theorem :: WEIERSTR:16
  for M being non empty MetrSpace holds for x being Point of M
  holds dist(x) is continuous;

theorem :: WEIERSTR:17
  for M being non empty MetrSpace holds for x being Point of M holds for
  P being Subset of TopSpaceMetr(M) holds P <> {} & P is compact implies ex x1
being Point of TopSpaceMetr(M) st x1 in P & (dist(x)).x1 = upper_bound((dist(x)
  ).:P);

theorem :: WEIERSTR:18
  for M being non empty MetrSpace holds for x being Point of M holds for
  P being Subset of TopSpaceMetr(M) holds P <> {} & P is compact implies ex x2
being Point of TopSpaceMetr(M) st x2 in P & (dist(x)).x2 = lower_bound((dist(x)
  ).:P);

definition
  let M be non empty MetrSpace;
  let P be Subset of TopSpaceMetr(M);
  func dist_max(P) -> Function of TopSpaceMetr(M),R^1 means
:: WEIERSTR:def 5

  for x being Point of M holds it.x = upper_bound((dist(x)).:P);
  func dist_min(P) -> Function of TopSpaceMetr(M),R^1 means
:: WEIERSTR:def 6

  for x being Point of M holds it.x = lower_bound((dist(x)).:P);
end;

theorem :: WEIERSTR:19
  for M being non empty MetrSpace holds for P being Subset of
  TopSpaceMetr(M) st P is compact for p1,p2 being Point of M holds p1 in P
implies dist(p1,p2) <= upper_bound((dist(p2)).:P) & lower_bound((dist(p2)).:P)
  <= dist(p1,p2);

theorem :: WEIERSTR:20
  for M being non empty MetrSpace holds for P being Subset of
  TopSpaceMetr(M) st P <> {} & P is compact holds for p1,p2 being Point of M
holds |.upper_bound((dist(p1)).:P) - upper_bound((dist(p2)).:P).| <= dist(p1,
  p2);

theorem :: WEIERSTR:21
  for M being non empty MetrSpace holds for P being Subset of
  TopSpaceMetr(M) st P <> {} & P is compact holds for p1,p2 being Point of M
holds for x1,x2 being Real holds x1 = (dist_max(P)).p1 & x2 = (dist_max(P)).p2
  implies |.x1 - x2.| <= dist(p1,p2);

theorem :: WEIERSTR:22
  for M being non empty MetrSpace holds for P being Subset of
  TopSpaceMetr(M) st P <> {} & P is compact holds for p1,p2 being Point of M
holds |.lower_bound((dist(p1)).:P) - lower_bound((dist(p2)).:P).| <= dist(p1,
  p2);

theorem :: WEIERSTR:23
  for M being non empty MetrSpace holds for P being Subset of
  TopSpaceMetr(M) st P <> {} & P is compact holds for p1,p2 being Point of M
holds for x1,x2 being Real holds x1 = (dist_min(P)).p1 & x2 = (dist_min(P)).p2
  implies |.x1 - x2.| <= dist(p1,p2);

theorem :: WEIERSTR:24
  for M being non empty MetrSpace holds for X being Subset of
  TopSpaceMetr(M) st X <> {} & X is compact holds dist_max(X) is continuous;

theorem :: WEIERSTR:25
  for M being non empty MetrSpace holds for P,Q being Subset of
  TopSpaceMetr(M) holds P <> {} & P is compact & Q <> {} & Q is compact implies
  ex x1 being Point of TopSpaceMetr(M) st x1 in Q & (dist_max(P)).x1 =
  upper_bound((dist_max(P)).:Q);

theorem :: WEIERSTR:26
  for M being non empty MetrSpace holds for P,Q being Subset of
  TopSpaceMetr(M) holds P <> {} & P is compact & Q <> {} & Q is compact implies
  ex x2 being Point of TopSpaceMetr(M) st x2 in Q & (dist_max(P)).x2 =
  lower_bound((dist_max(P)).:Q);

theorem :: WEIERSTR:27
  for M being non empty MetrSpace holds for X being Subset of
  TopSpaceMetr(M) st X <> {} & X is compact holds dist_min(X) is continuous;

theorem :: WEIERSTR:28
  for M being non empty MetrSpace holds for P,Q being Subset of
  TopSpaceMetr(M) holds P <> {} & P is compact & Q <> {} & Q is compact implies
  ex x1 being Point of TopSpaceMetr(M) st x1 in Q & (dist_min(P)).x1 =
  upper_bound((dist_min(P)).:Q);

theorem :: WEIERSTR:29
  for M being non empty MetrSpace holds for P,Q being Subset of
  TopSpaceMetr(M) holds P <> {} & P is compact & Q <> {} & Q is compact implies
  ex x2 being Point of TopSpaceMetr(M) st x2 in Q & (dist_min(P)).x2 =
  lower_bound((dist_min(P)).:Q);

definition
  let M be non empty MetrSpace;
  let P,Q be Subset of TopSpaceMetr(M);
  func min_dist_min(P,Q) -> Real equals
:: WEIERSTR:def 7
  lower_bound((dist_min(P)).:Q);
  func max_dist_min(P,Q) -> Real equals
:: WEIERSTR:def 8
  upper_bound((dist_min(P)).:Q);
  func min_dist_max(P,Q) -> Real equals
:: WEIERSTR:def 9
  lower_bound((dist_max(P)).:Q);
  func max_dist_max(P,Q) -> Real equals
:: WEIERSTR:def 10
  upper_bound((dist_max(P)).:Q);
end;

theorem :: WEIERSTR:30
  for M being non empty MetrSpace holds for P,Q being Subset of
TopSpaceMetr(M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1,
  x2 being Point of M st x1 in P & x2 in Q & dist(x1,x2) = min_dist_min(P,Q);

theorem :: WEIERSTR:31
  for M being non empty MetrSpace holds for P,Q being Subset of
TopSpaceMetr(M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1,
  x2 being Point of M st x1 in P & x2 in Q & dist(x1,x2) = min_dist_max(P,Q);

theorem :: WEIERSTR:32
  for M being non empty MetrSpace holds for P,Q being Subset of
TopSpaceMetr(M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1,
  x2 being Point of M st x1 in P & x2 in Q & dist(x1,x2) = max_dist_min(P,Q);

theorem :: WEIERSTR:33
  for M being non empty MetrSpace holds for P,Q being Subset of
TopSpaceMetr(M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1,
  x2 being Point of M st x1 in P & x2 in Q & dist(x1,x2) = max_dist_max(P,Q);

theorem :: WEIERSTR:34
  for M being non empty MetrSpace holds for P,Q being Subset of
TopSpaceMetr(M) st P is compact & Q is compact holds for x1,x2 being Point of M
  st x1 in P & x2 in Q holds min_dist_min(P,Q) <= dist(x1,x2) & dist(x1,x2) <=
  max_dist_max(P,Q);

::  B i b l i o g r a p h y
::  J.Dieudonne, "Foundations of Modern Analysis",Academic Press, 1960.
::  J.L.Kelley, "General Topology", von Nostnend, 1955.
::  K.Yosida, "Functional Analysis", Springer Verlag, 1968.