:: Bounding boxes for compact sets in ${\calE}^2$
::  by Czes{\l}aw Byli\'nski and Piotr Rudnicki
::
:: Received July 29, 1997
:: Copyright (c) 1997-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, FREEALG, SETFAM_1, CARD_1, XBOOLE_0, SUBSET_1, REAL_1,
      ORDINAL1, TARSKI, FUNCT_1, RELAT_1, ZFMISC_1, ARYTM_3, XXREAL_0, ARYTM_1,
      SEQ_1, SEQ_2, VALUED_0, ORDINAL2, XXREAL_2, SEQ_4, RCOMP_1, XXREAL_1,
      MEMBER_1, FUNCOP_1, PRALG_1, PRE_TOPC, STRUCT_0, LIMFUNC1, EUCLID,
      MCART_1, RLTOPSP1, PSCOMP_1, FUNCT_7, XCMPLX_0, NAT_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      COMPLEX1, SETFAM_1, REAL_1, NAT_1, INT_1, MEMBERED, RELAT_1, FUNCT_1,
      RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, STRUCT_0, PRE_TOPC, TOPS_2,
      VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4, RCOMP_1, LIMFUNC1,
      COMPTS_1, RLTOPSP1, EUCLID, XXREAL_0, XXREAL_2, MEASURE6;
 constructors DOMAIN_1, REAL_1, NAT_1, COMPLEX1, SEQ_2, SEQ_4, RCOMP_1,
      FUNCOP_1, LIMFUNC1, MEASURE6, TOPS_2, COMPTS_1, PCOMPS_1, TSP_1,
      TOPREAL1, SUPINF_1, XXREAL_2, PARTFUN1, RELSET_1, BINOP_2, COMSEQ_2;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS,
      XXREAL_0, XREAL_0, MEMBERED, SEQ_2, STRUCT_0, PRE_TOPC, COMPTS_1, EUCLID,
      SPPOL_2, VALUED_0, VALUED_1, XXREAL_2, FINSET_1, FCONT_3, MEASURE6,
      TOPREAL1, RELSET_1, XCMPLX_0;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Preliminaries

reserve r, s, t, g for Real,

          r3, r1, r2, q3, p3 for Real;

begin :: Real maps

definition
  let T be 1-sorted;
  mode RealMap of T is Function of the carrier of T, REAL;
end;

registration
  let T be non empty 1-sorted;
  cluster bounded for RealMap of T;
end;

definition
  let T be 1-sorted, f be RealMap of T;

  func lower_bound f -> Real equals
:: PSCOMP_1:def 1
  lower_bound (f.:the carrier of T);
  func upper_bound f -> Real equals
:: PSCOMP_1:def 2
  upper_bound (f.:the carrier of T);
end;

theorem :: PSCOMP_1:1
  for T being non empty TopSpace, f being bounded_below RealMap of
  T for p being Point of T holds f.p >= lower_bound f;

theorem :: PSCOMP_1:2
  for T being non empty TopSpace, f being bounded_below RealMap of T for
  s being Real st for t being Point of T holds f.t >= s
  holds lower_bound f >= s;

theorem :: PSCOMP_1:3
  for T being non empty TopSpace, f being RealMap of T st (for p being
  Point of T holds f.p >= r) & for t st for p being Point of T holds f.p >= t
  holds r >= t holds r = lower_bound f;

theorem :: PSCOMP_1:4
  for T being non empty TopSpace, f being bounded_above RealMap of
  T for p being Point of T holds f.p <= upper_bound f;

theorem :: PSCOMP_1:5
  for T being non empty TopSpace, f being bounded_above RealMap of T for
  t st for p being Point of T holds f.p <= t holds upper_bound f <= t;

theorem :: PSCOMP_1:6
  for T being non empty TopSpace, f being RealMap of T st (for p being
  Point of T holds f.p <= r) & (for t st for p being Point of T holds f.p <= t
  holds r <= t) holds r = upper_bound f;

theorem :: PSCOMP_1:7
  for T being non empty 1-sorted, f being bounded RealMap of T
  holds lower_bound f <= upper_bound f;

definition
  let T be TopStruct, f be RealMap of T;

  attr f is continuous means
:: PSCOMP_1:def 3

  for Y being Subset of REAL st Y is closed holds f"Y is closed;
end;

registration
  let T be non empty TopSpace;
  cluster continuous for RealMap of T;
end;

registration
  let T be non empty TopSpace, S be non empty SubSpace of T;
  cluster continuous for RealMap of S;
end;

reserve T for TopStruct,
  f for RealMap of T;

theorem :: PSCOMP_1:8
  f is continuous iff for Y being Subset of REAL st Y is open holds f"Y is open
;

theorem :: PSCOMP_1:9
  f is continuous implies -f is continuous;

theorem :: PSCOMP_1:10
  f is continuous implies r3+f is continuous;

theorem :: PSCOMP_1:11
  f is continuous & not 0 in rng f implies Inv f is continuous;

theorem :: PSCOMP_1:12
  for R being Subset-Family of REAL st f is continuous & R is open holds
  ("f).:R is open;

theorem :: PSCOMP_1:13
  for R being Subset-Family of REAL st f is continuous & R is
  closed holds ("f).:R is closed;

definition
  let T be non empty TopStruct, f be RealMap of T, X be Subset of T;
  redefine func f|X -> RealMap of T|X;
end;

registration
  let T be non empty TopSpace, f be continuous RealMap of T, X be Subset of T;
  cluster f|X -> continuous for RealMap of T|X;
end;

registration
  let T be non empty TopSpace, P be compact non empty Subset of T;
  cluster T|P -> compact;
end;

begin :: Pseudocompact spaces

theorem :: PSCOMP_1:14
  for T being non empty TopSpace holds (for f being RealMap of T
  st f is continuous holds f is with_max) iff for f being RealMap of T st f is
  continuous holds f is with_min;

theorem :: PSCOMP_1:15
  for T being non empty TopSpace holds (for f being RealMap of T
  st f is continuous holds f is bounded) iff for f being RealMap of T st f is
  continuous holds f is with_max;

definition

  let T be TopStruct;
  attr T is pseudocompact means
:: PSCOMP_1:def 4

  for f being RealMap of T st f is continuous holds f is bounded;
end;

registration
  cluster compact -> pseudocompact for non empty TopSpace;
end;

registration
  cluster non empty compact for TopSpace;
end;

registration
  let T be pseudocompact non empty TopSpace;
  cluster continuous -> bounded with_max with_min for RealMap of T;
end;

theorem :: PSCOMP_1:16
  for T being non empty TopSpace, X being non empty Subset of T, Y
being compact Subset of T, f being continuous RealMap of T st X c= Y
holds lower_bound
  (f|Y) <= lower_bound (f|X);

theorem :: PSCOMP_1:17
  for T being non empty TopSpace, X being non empty Subset of T, Y
being compact Subset of T, f being continuous RealMap of T st X c= Y
holds upper_bound
  (f|X) <= upper_bound (f|Y);

begin :: Bounding boxes of compact sets in TOP-REAL 2

registration
  let n be Element of NAT, X, Y be compact Subset of TOP-REAL n;
  cluster X /\ Y -> compact for Subset of TOP-REAL n;
end;

reserve p for Point of TOP-REAL 2,
  P for Subset of TOP-REAL 2,
  Z for non empty Subset of TOP-REAL 2,
  X for non empty compact Subset of TOP-REAL 2;

definition
  func proj1 -> RealMap of TOP-REAL 2 means
:: PSCOMP_1:def 5

  for p being Point of TOP-REAL 2 holds it.p = p`1;
  func proj2 -> RealMap of TOP-REAL 2 means
:: PSCOMP_1:def 6

  for p being Point of TOP-REAL 2 holds it.p = p`2;
end;

theorem :: PSCOMP_1:18
  proj1"].r,s.[ = {|[ r1, r2 ]| : r < r1 & r1 < s};

theorem :: PSCOMP_1:19
  for r3, q3 st P = {|[ r1, r2 ]| : r3 < r1 & r1 < q3} holds P is open;

theorem :: PSCOMP_1:20
  proj2"].r,s.[ = {|[ r1, r2 ]| : r < r2 & r2 < s};

theorem :: PSCOMP_1:21
  for r3, q3 st P = {|[ r1, r2 ]| : r3 < r2 & r2 < q3} holds P is open;

registration
  cluster proj1 -> continuous;
  cluster proj2 -> continuous;
end;

theorem :: PSCOMP_1:22
  for X being Subset of TOP-REAL 2, p being Point of TOP-REAL 2 st
  p in X holds (proj1|X).p = p`1;

theorem :: PSCOMP_1:23
  for X being Subset of TOP-REAL 2, p being Point of TOP-REAL 2 st
  p in X holds (proj2|X).p = p`2;

definition
  let X be Subset of TOP-REAL 2;
  func W-bound X -> Real equals
:: PSCOMP_1:def 7
  lower_bound (proj1|X);
  func N-bound X -> Real equals
:: PSCOMP_1:def 8
  upper_bound (proj2|X);
  func E-bound X -> Real equals
:: PSCOMP_1:def 9
  upper_bound (proj1|X);
  func S-bound X -> Real equals
:: PSCOMP_1:def 10
  lower_bound (proj2|X);
end;

theorem :: PSCOMP_1:24
  p in X implies W-bound X <= p`1 & p`1 <= E-bound X & S-bound X <= p`2
  & p`2 <= N-bound X;

definition
  let X be Subset of TOP-REAL 2;
  func SW-corner X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 11
  |[W-bound X, S-bound X]|;
  func NW-corner X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 12
  |[W-bound X, N-bound X]|;
  func NE-corner X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 13
  |[E-bound X, N-bound X]|;
  func SE-corner X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 14
  |[E-bound X, S-bound X]|;
end;

theorem :: PSCOMP_1:25
  (SW-corner P)`1 = (NW-corner P)`1;

theorem :: PSCOMP_1:26
  (SE-corner P)`1 = (NE-corner P)`1;

theorem :: PSCOMP_1:27
  (NW-corner P)`2 = (NE-corner P)`2;

theorem :: PSCOMP_1:28
  (SW-corner P)`2 = (SE-corner P)`2;

definition
  let X be Subset of TOP-REAL 2;
  func W-most X -> Subset of TOP-REAL 2 equals
:: PSCOMP_1:def 15
  LSeg(SW-corner X, NW-corner X)
  /\X;
  func N-most X -> Subset of TOP-REAL 2 equals
:: PSCOMP_1:def 16
  LSeg(NW-corner X, NE-corner X)
  /\X;
  func E-most X -> Subset of TOP-REAL 2 equals
:: PSCOMP_1:def 17
  LSeg(SE-corner X, NE-corner X)
  /\X;
  func S-most X -> Subset of TOP-REAL 2 equals
:: PSCOMP_1:def 18
  LSeg(SW-corner X, SE-corner X)
  /\X;
end;

registration
  let X be non empty compact Subset of TOP-REAL 2;
  cluster W-most X -> non empty compact;
  cluster N-most X -> non empty compact;
  cluster E-most X -> non empty compact;
  cluster S-most X -> non empty compact;
end;

definition
  let X be Subset of TOP-REAL 2;
  func W-min X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 19
  |[W-bound X, lower_bound (proj2|W-most X)]|;
  func W-max X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 20
  |[W-bound X, upper_bound (proj2|W-most X)]|;
  func N-min X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 21
  |[lower_bound (proj1|N-most X), N-bound X]|;
  func N-max X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 22
  |[upper_bound (proj1|N-most X), N-bound X]|;
  func E-max X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 23
  |[E-bound X, upper_bound (proj2|E-most X)]|;
  func E-min X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 24
  |[E-bound X, lower_bound (proj2|E-most X)]|;
  func S-max X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 25
  |[upper_bound (proj1|S-most X), S-bound X]|;
  func S-min X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 26
  |[lower_bound (proj1|S-most X), S-bound X]|;
end;

theorem :: PSCOMP_1:29
  (SW-corner P)`1 = (W-min P)`1 & (SW-corner P)`1 = (W-max P)`1 &
  (W-min P)`1 = (W-max P)`1 & (W-min P)`1 = (NW-corner P)`1 & (W-max P)`1 = (
  NW-corner P)`1;

theorem :: PSCOMP_1:30
  (SW-corner X)`2 <= (W-min X)`2 & (SW-corner X)`2 <= (W-max X)`2
& (SW-corner X)`2 <= (NW-corner X)`2 & (W-min X)`2 <= (W-max X)`2 & (W-min X)`2
  <= (NW-corner X)`2 & (W-max X)`2 <= (NW-corner X)`2;

theorem :: PSCOMP_1:31
  p in W-most Z implies p`1 = (W-min Z)`1 & (Z is compact implies
  (W-min Z)`2 <= p`2 & p`2 <= (W-max Z)`2);

theorem :: PSCOMP_1:32
  W-most X c= LSeg(W-min X, W-max X);

theorem :: PSCOMP_1:33
  LSeg(W-min X, W-max X) c= LSeg(SW-corner X, NW-corner X);

theorem :: PSCOMP_1:34
  W-min X in W-most X & W-max X in W-most X;

theorem :: PSCOMP_1:35
  LSeg(SW-corner X, W-min X)/\X = {W-min X} & LSeg(W-max X, NW-corner X)
  /\X = {W-max X};

theorem :: PSCOMP_1:36
  W-min X = W-max X implies W-most X = {W-min X};

theorem :: PSCOMP_1:37
  (NW-corner P)`2 = (N-min P)`2 & (NW-corner P)`2 = (N-max P)`2 &
  (N-min P)`2 = (N-max P)`2 & (N-min P)`2 = (NE-corner P)`2 & (N-max P)`2 = (
  NE-corner P)`2;

theorem :: PSCOMP_1:38
  (NW-corner X)`1 <= (N-min X)`1 & (NW-corner X)`1 <= (N-max X)`1
& (NW-corner X)`1 <= (NE-corner X)`1 & (N-min X)`1 <= (N-max X)`1 & (N-min X)`1
  <= (NE-corner X)`1 & (N-max X)`1 <= (NE-corner X)`1;

theorem :: PSCOMP_1:39
  p in N-most Z implies p`2 = (N-min Z)`2 & (Z is compact implies
  (N-min Z)`1 <= p`1 & p`1 <= (N-max Z)`1);

theorem :: PSCOMP_1:40
  N-most X c= LSeg(N-min X, N-max X);

theorem :: PSCOMP_1:41
  LSeg(N-min X, N-max X) c= LSeg(NW-corner X, NE-corner X);

theorem :: PSCOMP_1:42
  N-min X in N-most X & N-max X in N-most X;

theorem :: PSCOMP_1:43
  LSeg(NW-corner X, N-min X)/\X = {N-min X} & LSeg(N-max X, NE-corner X)
  /\X = {N-max X};

theorem :: PSCOMP_1:44
  N-min X = N-max X implies N-most X = {N-min X};

theorem :: PSCOMP_1:45
  (SE-corner P)`1 = (E-min P)`1 & (SE-corner P)`1 = (E-max P)`1 &
  (E-min P)`1 = (E-max P)`1 & (E-min P)`1 = (NE-corner P)`1 & (E-max P)`1 = (
  NE-corner P)`1;

theorem :: PSCOMP_1:46
  (SE-corner X)`2 <= (E-min X)`2 & (SE-corner X)`2 <= (E-max X)`2
& (SE-corner X)`2 <= (NE-corner X)`2 & (E-min X)`2 <= (E-max X)`2 & (E-min X)`2
  <= (NE-corner X)`2 & (E-max X)`2 <= (NE-corner X)`2;

theorem :: PSCOMP_1:47
  p in E-most Z implies p`1 = (E-min Z)`1 & (Z is compact implies
  (E-min Z)`2 <= p`2 & p`2 <= (E-max Z)`2);

theorem :: PSCOMP_1:48
  E-most X c= LSeg(E-min X, E-max X);

theorem :: PSCOMP_1:49
  LSeg(E-min X, E-max X) c= LSeg(SE-corner X, NE-corner X);

theorem :: PSCOMP_1:50
  E-min X in E-most X & E-max X in E-most X;

theorem :: PSCOMP_1:51
  LSeg(SE-corner X, E-min X)/\X = {E-min X} & LSeg(E-max X, NE-corner X)
  /\X = {E-max X};

theorem :: PSCOMP_1:52
  E-min X = E-max X implies E-most X = {E-min X};

theorem :: PSCOMP_1:53
  (SW-corner P)`2 = (S-min P)`2 & (SW-corner P)`2 = (S-max P)`2 &
  (S-min P)`2 = (S-max P)`2 & (S-min P)`2 = (SE-corner P)`2 & (S-max P)`2 = (
  SE-corner P)`2;

theorem :: PSCOMP_1:54
  (SW-corner X)`1 <= (S-min X)`1 & (SW-corner X)`1 <= (S-max X)`1
& (SW-corner X)`1 <= (SE-corner X)`1 & (S-min X)`1 <= (S-max X)`1 & (S-min X)`1
  <= (SE-corner X)`1 & (S-max X)`1 <= (SE-corner X)`1;

theorem :: PSCOMP_1:55
  p in S-most Z implies p`2 = (S-min Z)`2 & (Z is compact implies
  (S-min Z)`1 <= p`1 & p`1 <= (S-max Z)`1);

theorem :: PSCOMP_1:56
  S-most X c= LSeg(S-min X, S-max X);

theorem :: PSCOMP_1:57
  LSeg(S-min X, S-max X) c= LSeg(SW-corner X, SE-corner X);

theorem :: PSCOMP_1:58
  S-min X in S-most X & S-max X in S-most X;

theorem :: PSCOMP_1:59
  LSeg(SW-corner X, S-min X)/\X = {S-min X} & LSeg(S-max X, SE-corner X)
  /\X = {S-max X};

theorem :: PSCOMP_1:60
  S-min X = S-max X implies S-most X = {S-min X};

:: Degenerate cases

theorem :: PSCOMP_1:61
  W-max P = N-min P implies W-max P = NW-corner P;

theorem :: PSCOMP_1:62
  N-max P = E-max P implies N-max P = NE-corner P;

theorem :: PSCOMP_1:63
  E-min P = S-max P implies E-min P = SE-corner P;

theorem :: PSCOMP_1:64
  S-min P = W-min P implies S-min P = SW-corner P;

theorem :: PSCOMP_1:65
  proj2. |[r,s]| = s & proj1. |[r,s]| = r;

:: Moved from JORDAN1E, AK, 23.02.2006

theorem :: PSCOMP_1:66
  for X be non empty Subset of TOP-REAL 2 for Y be compact Subset of
  TOP-REAL 2 st X c= Y holds N-bound X <= N-bound Y;

theorem :: PSCOMP_1:67
  for X be non empty Subset of TOP-REAL 2 for Y be compact Subset of
  TOP-REAL 2 st X c= Y holds E-bound X <= E-bound Y;

theorem :: PSCOMP_1:68
  for X be non empty Subset of TOP-REAL 2 for Y be compact Subset of
  TOP-REAL 2 st X c= Y holds S-bound X >= S-bound Y;

theorem :: PSCOMP_1:69
  for X be non empty Subset of TOP-REAL 2 for Y be compact Subset of
  TOP-REAL 2 st X c= Y holds W-bound X >= W-bound Y;