:: Sequences of Metric Spaces and an Abstract Intermediate Value Theorem
::  by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received September 11, 2002
:: Copyright (c) 2002-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, SUBSET_1, XXREAL_0, SEQ_4, XXREAL_2, ARYTM_1,
      CARD_1, ARYTM_3, METRIC_1, NAT_1, PCOMPS_1, SEQ_2, FUNCT_1, RCOMP_1,
      ORDINAL2, TARSKI, REAL_1, STRUCT_0, PRE_TOPC, RELAT_1, SEQ_1, COMPLEX1,
      XXREAL_1, TOPMETR, VALUED_0, BORSUK_1, EUCLID, TOPREAL1, TOPREAL2,
      PSCOMP_1, JORDAN6, TOPS_2;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
      XXREAL_2, XREAL_0, COMPLEX1, REAL_1, RELAT_1, FUNCT_1, RELSET_1,
      PARTFUN1, FUNCT_2, BINOP_1, NAT_1, STRUCT_0, METRIC_1, PRE_TOPC, TOPS_2,
      COMPTS_1, PCOMPS_1, RCOMP_1, EUCLID, PSCOMP_1, TOPMETR, SEQ_1, SEQ_2,
      SEQM_3, SEQ_4, TBSP_1, JORDAN6, TOPREAL1, TOPREAL2;
 constructors REAL_1, COMPLEX1, RCOMP_1, TOPS_2, COMPTS_1, TBSP_1, TOPMETR,
      TOPREAL1, PSCOMP_1, JORDAN5C, JORDAN6, SEQ_4, BINOP_2, SEQ_2, PCOMPS_1,
      COMSEQ_2, BINOP_1;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED,
      STRUCT_0, PRE_TOPC, METRIC_1, PCOMPS_1, EUCLID, TOPMETR, COMPTS_1,
      VALUED_0, SEQ_4;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

theorem :: TOPMETR3:1
  for X being non empty MetrSpace, S being sequence of X, F being
  Subset of TopSpaceMetr(X) st S is convergent & (for n being Nat
  holds S.n in F) & F is closed holds lim S in F;

theorem :: TOPMETR3:2
  for X,Y being non empty MetrSpace, f being Function of
TopSpaceMetr(X),TopSpaceMetr(Y),S being sequence of X holds f*S is sequence of
  Y;

theorem :: TOPMETR3:3
  for X,Y being non empty MetrSpace, f being Function of
TopSpaceMetr(X),TopSpaceMetr(Y),S being sequence of X, T being sequence of Y st
  S is convergent & T= f*S & f is continuous holds T is convergent;

theorem :: TOPMETR3:4
  for s being Real_Sequence,S being sequence of RealSpace st s=S
  holds (s is convergent iff S is convergent) & (s is convergent implies lim s=
  lim S);

theorem :: TOPMETR3:5
  for a,b being Real,s being Real_Sequence st rng s c= [.a,b
  .] holds s is sequence of Closed-Interval-MSpace(a,b);

theorem :: TOPMETR3:6
  for a,b being Real, S being sequence of
  Closed-Interval-MSpace(a,b) st a<=b holds S is sequence of RealSpace;

theorem :: TOPMETR3:7
  for a,b being Real, S1 being sequence of
Closed-Interval-MSpace(a,b), S being sequence of RealSpace st S=S1 & a<=b holds
(S is convergent iff S1 is convergent)& (S is convergent implies lim S=lim S1);

theorem :: TOPMETR3:8
  for a,b being Real,s being Real_Sequence, S being
sequence of Closed-Interval-MSpace(a,b) st S=s & a<=b & s is convergent holds S
  is convergent & lim s=lim S;

theorem :: TOPMETR3:9
  for a,b being Real,s being Real_Sequence, S being sequence of
  Closed-Interval-MSpace(a,b) st S=s & a<=b & s is non-decreasing holds S is
  convergent;

theorem :: TOPMETR3:10
  for a,b being Real,s being Real_Sequence, S being sequence of
  Closed-Interval-MSpace(a,b) st S=s & a<=b & s is non-increasing holds S is
  convergent;

theorem :: TOPMETR3:11
  for R being non empty Subset of REAL st R is bounded_above holds
ex s being Real_Sequence st s is non-decreasing convergent & rng s c= R & lim s
  =upper_bound R;

theorem :: TOPMETR3:12
  for R being non empty Subset of REAL st R is bounded_below holds
ex s being Real_Sequence st s is non-increasing convergent & rng s c= R & lim s
  =lower_bound R;

theorem :: TOPMETR3:13
  :: An Abstract Intermediate Value Theorem for Closed Sets
  for X being non empty MetrSpace, f being Function of I[01],
TopSpaceMetr(X), F1,F2 being Subset of TopSpaceMetr(X),
   r1,r2 being Real st 0<=
r1 & r2<=1 & r1<=r2 & f.r1 in F1 & f.r2 in F2 & F1 is closed & F2 is closed & f
is continuous & F1 \/ F2 =the carrier of X
   ex r being Real st r1<=r & r<=r2 & f.r in F1 /\ F2;

theorem :: TOPMETR3:14
  for n being Nat,p1,p2 being Point of TOP-REAL n, P,P1
being non empty Subset of TOP-REAL n st P is_an_arc_of p1,p2 & P1 is_an_arc_of
  p2,p1 & P1 c= P holds P1=P;

theorem :: TOPMETR3:15
  for P,P1 being compact non empty Subset of TOP-REAL 2 st P is
  being_simple_closed_curve & P1 is_an_arc_of W-min(P),E-max(P) & P1 c= P holds
  P1=Upper_Arc(P) or P1=Lower_Arc(P);