:: 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;