:: Bounding boxes for compact sets in ${\calE}^2$
:: by Czes{\l}aw Byli\'nski and Piotr Rudnicki
::
:: Received July 29, 1997
:: Copyright (c) 1997-2026 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;
definitions TARSKI, TOPS_2, ORDINAL1, XXREAL_2, SEQ_2, MEASURE6;
equalities RCOMP_1, STRUCT_0, SUBSET_1, LIMFUNC1, XCMPLX_0, MEASURE6;
expansions TARSKI, RCOMP_1, XXREAL_2, MEASURE6;
theorems TARSKI, RELAT_1, FUNCT_1, FUNCT_2, PRE_TOPC, SEQ_4, RCOMP_1,
FUNCOP_1, EUCLID, SEQ_1, SEQ_2, TOPS_1, TSP_1, COMPTS_1, SETFAM_1,
ZFMISC_1, TOPREAL1, JORDAN1, GOBOARD7, XREAL_0, XBOOLE_0, XBOOLE_1,
XCMPLX_1, MEASURE6, XREAL_1, XXREAL_0, VALUED_1, XXREAL_2, RLTOPSP1,
XXREAL_1, MEMBER_1, ORDINAL1;
schemes FUNCT_2, DOMAIN_1;
begin :: Preliminaries
reserve r, s, t, g for Real,
r3, r1, r2, q3, p3 for Real;
Lm1: for X being Subset of REAL st X is bounded_below holds --X is
bounded_above
proof
let X be Subset of REAL;
given s such that
A1: s is LowerBound of X;
take -s;
let t be ExtReal;
assume t in --X; then
t in {-r2 where r2 is Complex : r2 in X} by MEMBER_1:def 2;
then consider r2 being Complex such that
A2: t = -r2 and
A3: r2 in X;
reconsider r3 = r2 as Real by A3;
r3 >= s by A1,A3,XXREAL_2:def 2;
hence thesis by A2,XREAL_1:24;
end;
Lm2: for X being non empty set, f being Function of X, REAL st f is with_min
holds -f is with_max
proof
let X be non empty set, f be Function of X, REAL;
assume that
A1: f.:X is bounded_below and
A2: lower_bound (f.:X) in f.:X;
A3: --(f.:X) = (-f).:X by MEASURE6:65;
hence (-f).:X is bounded_above by A1,Lm1;
then
A4: upper_bound ((-f).:X) = - lower_bound -- --(f.:X) by A3,MEASURE6:44
.= - lower_bound (f.:X);
- lower_bound (f.:X) in --(f.:X) by A2,MEMBER_1:11;
hence thesis by A4,MEASURE6:65;
end;
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;
existence
proof
set c = (the carrier of T);
reconsider f = c --> In(0,REAL) as RealMap of T;
take f;
dom f = c & rng f = {0 qua Real} by FUNCOP_1:8,FUNCT_2:def 1;
hence f.:c is bounded_above by RELAT_1:113;
thus f.:c is bounded_below;
end;
end;
definition
let T be 1-sorted, f be RealMap of T;
func lower_bound f -> Real equals
lower_bound (f.:the carrier of T);
coherence;
func upper_bound f -> Real equals
upper_bound (f.:the carrier of T);
coherence;
end;
theorem Th1:
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
proof
let T be non empty TopSpace, f be bounded_below RealMap of T;
set fc = (f.:the carrier of T);
let p be Point of T;
fc is bounded_below & f.p in fc by FUNCT_2:35,MEASURE6:def 10;
hence thesis by SEQ_4:def 2;
end;
theorem
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
proof
let T be non empty TopSpace, f be bounded_below RealMap of T;
set c = the carrier of T;
set fc = (f.:the carrier of T);
let s be Real;
assume
A1: for t being Point of T holds f.t >= s;
now
let p1 be Real;
assume p1 in fc;
then ex x being object st x in c & x in c & p1 = f.x by FUNCT_2:64;
hence p1 >= s by A1;
end;
hence thesis by SEQ_4:43;
end;
theorem
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
proof
let T be non empty TopSpace, f be RealMap of T;
set c = the carrier of T;
set fc = (f.:the carrier of T);
assume that
A1: for p being Point of T holds f.p >= r and
A2: for t st for p being Point of T holds f.p >= t holds r >= t;
A3: now
let t;
assume for s st s in fc holds s >= t;
then for s being Point of T holds f.s >= t by FUNCT_2:35;
hence r >= t by A2;
end;
now
let s;
assume s in fc;
then ex x being object st x in c & x in c & s = f.x by FUNCT_2:64;
hence s >= r by A1;
end;
hence thesis by A3,SEQ_4:44;
end;
theorem Th4:
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
proof
let T be non empty TopSpace, f be bounded_above RealMap of T;
set fc = (f.:the carrier of T);
let p be Point of T;
fc is bounded_above & f.p in fc by FUNCT_2:35,MEASURE6:def 11;
hence thesis by SEQ_4:def 1;
end;
theorem
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
proof
let T be non empty TopSpace, f be bounded_above RealMap of T;
set c = the carrier of T;
set fc = (f.:the carrier of T);
let t;
assume
A1: for p being Point of T holds f.p <= t;
now
let s;
assume s in fc;
then ex x being object st x in c & x in c & s = f.x by FUNCT_2:64;
hence s <= t by A1;
end;
hence thesis by SEQ_4:45;
end;
theorem
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
proof
let T be non empty TopSpace, f be RealMap of T;
set c = the carrier of T;
set fc = (f.:the carrier of T);
assume that
A1: for p being Point of T holds f.p <= r and
A2: for t st for p being Point of T holds f.p <= t holds r <= t;
A3: now
let t;
assume for s st s in fc holds s <= t;
then for s being Point of T holds f.s <= t by FUNCT_2:35;
hence r <= t by A2;
end;
now
let s;
assume s in fc;
then ex x being object st x in c & x in c & s = f.x by FUNCT_2:64;
hence s <= r by A1;
end;
hence thesis by A3,SEQ_4:46;
end;
theorem Th7:
for T being non empty 1-sorted, f being bounded RealMap of T
holds lower_bound f <= upper_bound f
proof
let T be non empty 1-sorted, f be bounded RealMap of T;
f.:the carrier of T is bounded_below & f.:the carrier of T is
bounded_above by MEASURE6:def 10,def 11;
hence thesis by SEQ_4:11;
end;
definition
let T be TopStruct, f be RealMap of T;
attr f is continuous means
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;
existence
proof
set c = (the carrier of T);
reconsider f = c --> In(0,REAL) as RealMap of T;
take f;
A1: dom f = c by FUNCT_2:def 1;
let Y be Subset of REAL;
A2: rng f = {0 qua Real} by FUNCOP_1:8;
assume Y is closed;
per cases;
suppose
0 in Y;
then
A3: rng f c= Y by A2,ZFMISC_1:31;
f"Y = f"(rng f /\ Y) by RELAT_1:133
.= f"rng f by A3,XBOOLE_1:28
.= [#]T by A1,RELAT_1:134;
hence thesis;
end;
suppose
not 0 in Y;
then
A4: rng f misses Y by A2,ZFMISC_1:50;
f"Y = f"(rng f /\ Y) by RELAT_1:133
.= f"{} by A4,XBOOLE_0:def 7
.= {}T;
hence thesis;
end;
end;
end;
registration
let T be non empty TopSpace, S be non empty SubSpace of T;
cluster continuous for RealMap of S;
existence
proof
set c = (the carrier of S);
reconsider f = c --> In(0,REAL) as RealMap of S;
take f;
A1: dom f = c by FUNCT_2:def 1;
let Y be Subset of REAL;
A2: rng f = {0 qua Real} by FUNCOP_1:8;
assume Y is closed;
per cases;
suppose
0 in Y;
then
A3: rng f c= Y by A2,ZFMISC_1:31;
f"Y = f"(rng f /\ Y) by RELAT_1:133
.= f"rng f by A3,XBOOLE_1:28
.= [#]S by A1,RELAT_1:134;
hence thesis;
end;
suppose
not 0 in Y;
then
A4: rng f misses Y by A2,ZFMISC_1:50;
f"Y = f"(rng f /\ Y) by RELAT_1:133
.= f"{} by A4,XBOOLE_0:def 7
.= {}S;
hence thesis;
end;
end;
end;
reserve T for TopStruct,
f for RealMap of T;
theorem Th8:
f is continuous iff for Y being Subset of REAL st Y is open holds f"Y is open
proof
hereby
assume
A1: f is continuous;
let Y be Subset of REAL;
assume Y is open;
then Y` is closed;
then
A2: f"(Y`) is closed by A1;
f"(Y`) = (f"REAL) \ f"(Y) by FUNCT_1:69
.= ([#]T) \ f"Y by FUNCT_2:40;
then ([#]T) \ (([#]T) \ f"(Y)) is open by A2,PRE_TOPC:def 3;
hence f"Y is open by PRE_TOPC:3;
end;
assume
A3: for Y being Subset of REAL st Y is open holds f"Y is open;
let Y be Subset of REAL;
assume Y is closed;
then Y` is open;
then
A4: f"(Y`) is open by A3;
f"(Y`) = (f"REAL) \ f"(Y) by FUNCT_1:69
.= ([#]T) \ f"Y by FUNCT_2:40;
hence thesis by A4,PRE_TOPC:def 3;
end;
theorem Th9:
f is continuous implies -f is continuous
proof
assume
A1: f is continuous;
let X be Subset of REAL;
assume X is closed;
then
A2: --X is closed by MEASURE6:45;
(-f)"X = f"(--X) by MEASURE6:68;
hence thesis by A1,A2;
end;
theorem Th10:
f is continuous implies r3+f is continuous
proof
assume
A1: f is continuous;
let X be Subset of REAL;
assume X is closed;
then
A2: -r3++X is closed by MEASURE6:53;
(r3+f)"X = f"(-r3++X) by MEASURE6:70;
hence thesis by A1,A2;
end;
theorem Th11:
f is continuous & not 0 in rng f implies Inv f is continuous
proof
assume that
A1: f is continuous and
A2: not 0 in rng f;
let X0 be Subset of REAL;
0 in {0} by TARSKI:def 1;
then not 0 in X0\{0} by XBOOLE_0:def 5;
then reconsider X = X0\{0} as without_zero Subset of REAL by MEASURE6:def 2;
set X9 = Inv X;
A3: X0\{0} c= X0 by XBOOLE_1:36;
set X9r = X9/\rng f;
assume
A4: X0 is closed;
now
let x be object;
hereby
A5: X9r c= Cl X9r by MEASURE6:58;
assume
A6: x in X9r;
then x in rng f by XBOOLE_0:def 4;
hence x in (Cl X9r) /\ rng f by A6,A5,XBOOLE_0:def 4;
end;
assume
A7: x in (Cl X9r) /\ rng f;
then reconsider s = x as Real;
x in Cl (X9r) by A7,XBOOLE_0:def 4;
then consider seq being Real_Sequence such that
A8: rng seq c= X9r and
A9: seq is convergent and
A10: lim seq = s by MEASURE6:64;
assume
A11: not x in X9r;
A12: x in rng f by A7,XBOOLE_0:def 4;
now
rng (seq") c= X
proof
let y be object;
assume y in rng (seq");
then consider n being object such that
A13: n in dom (seq") and
A14: y = (seq").n by FUNCT_1:def 3;
reconsider n as Element of NAT by A13;
seq.n in rng seq by FUNCT_2:4;
then
A15: 1/(1/seq.n) in X9 by A8,XBOOLE_0:def 4;
(seq").n = (seq.n)" by VALUED_1:10
.= 1/(seq.n);
hence thesis by A14,A15,MEASURE6:54;
end;
then
A16: rng (seq") c= X0 by A3;
assume
A17: lim seq <> 0;
now
let n be Nat;
A18: n in NAT by ORDINAL1:def 12;
assume seq.n = 0;
then 0 in rng seq by FUNCT_2:4,A18;
hence contradiction by A2,A8,XBOOLE_0:def 4;
end;
then
A19: seq is non-zero by SEQ_1:5;
then seq" is convergent by A9,A17,SEQ_2:21;
then
A20: lim (seq") in X0 by A4,A16;
A21: lim (seq") = (lim seq)" by A9,A17,A19,SEQ_2:22;
then lim (seq") <> 0 by A17;
then not lim (seq") in {0} by TARSKI:def 1;
then lim (seq") in X by A20,XBOOLE_0:def 5;
then 1/(lim (seq")) in X9;
hence contradiction by A12,A10,A11,A21,XBOOLE_0:def 4;
end;
hence contradiction by A2,A7,A10,XBOOLE_0:def 4;
end;
then
A22: X9r = (Cl X9r) /\ rng f by TARSKI:2;
f"(Cl X9r) is closed by A1;
then
A23: f"X9r is closed by A22,RELAT_1:133;
A24: now
let x be object;
hereby
assume
A25: x in (Inv f)"X0;
then
A26: (Inv f).x in X0 by FUNCT_2:38;
reconsider xx=x as set by TARSKI:1;
now
assume not (Inv f).x in X;
then (Inv f).x in {0} by A26,XBOOLE_0:def 5;
then (Inv f).x = 0 by TARSKI:def 1;
then 0 = (f.xx)" by VALUED_1:10;
hence contradiction by A2,A25,FUNCT_2:4,XCMPLX_1:202;
end;
hence x in (Inv f)"X by A25,FUNCT_2:38;
end;
(Inv f)"X c= (Inv f)"X0 by RELAT_1:143,XBOOLE_1:36;
hence x in (Inv f)"X implies x in (Inv f)"X0;
end;
f"X9 = f"X9r & (Inv f)"X = f"(Inv X) by MEASURE6:71,RELAT_1:133;
hence thesis by A23,A24,TARSKI:2;
end;
theorem
for R being Subset-Family of REAL st f is continuous & R is open holds
("f).:R is open
proof
let R be Subset-Family of REAL;
assume
A1: f is continuous;
assume
A2: R is open;
let P be Subset of T;
assume P in ("f).:R;
then consider eR being object such that
A3: eR in bool REAL and
A4: eR in R and
A5: P = ("f).eR by FUNCT_2:64;
reconsider eR as set by TARSKI:1;
A6: P = f"eR by A3,A5,MEASURE6:def 3;
reconsider eR as Subset of REAL by A3;
eR is open by A2,A4;
hence thesis by A1,A6,Th8;
end;
theorem Th13:
for R being Subset-Family of REAL st f is continuous & R is
closed holds ("f).:R is closed
proof
let R be Subset-Family of REAL;
assume
A1: f is continuous;
assume
A2: R is closed;
let P be Subset of T;
assume P in ("f).:R;
then consider eR being object such that
A3: eR in bool REAL and
A4: eR in R and
A5: P = ("f).eR by FUNCT_2:64;
reconsider eR as set by TARSKI:1;
A6: P = f"eR by A3,A5,MEASURE6:def 3;
reconsider eR as Subset of REAL by A3;
eR is closed by A2,A4;
hence thesis by A1,A6;
end;
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; :: redefines | (RELAT_1, definition)
coherence
proof
the carrier of T|X = X by PRE_TOPC:8;
hence thesis by FUNCT_2:32;
end;
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;
coherence
proof
now
let Y be Subset of REAL;
assume Y is open;
then
A1: f"Y is open by Th8;
the carrier of (T|X) = X & (f|X)"Y = X/\(f"Y) by FUNCT_1:70,PRE_TOPC:8;
hence (f|X)"Y is open by A1,TSP_1:def 1;
end;
hence thesis by Th8;
end;
end;
registration
let T be non empty TopSpace, P be compact non empty Subset of T;
cluster T|P -> compact;
coherence by COMPTS_1:3;
end;
begin :: Pseudocompact spaces
theorem Th14:
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
proof
let T be non empty TopSpace;
hereby
assume
A1: for f being RealMap of T st f is continuous holds f is with_max;
let f be RealMap of T;
assume f is continuous;
then -f is continuous by Th9;
then -f is with_max by A1;
hence f is with_min by MEASURE6:66;
end;
assume
A2: for f being RealMap of T st f is continuous holds f is with_min;
let f be RealMap of T;
assume f is continuous;
then -f is continuous by Th9;
then - -f is with_max by A2,Lm2;
hence thesis;
end;
theorem Th15:
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
proof
let T be non empty TopSpace;
set cT = the carrier of T;
hereby
assume
A1: for f being RealMap of T st f is continuous holds f is bounded;
let f be RealMap of T such that
A2: f is continuous;
set fcT = f.:cT;
f is bounded by A1,A2;
then
A3: fcT is bounded_above by MEASURE6:def 11;
set b = upper_bound fcT;
set bf = b+-f;
-f is continuous by A2,Th9;
then
A4: bf is continuous by Th10;
reconsider bf9 = bf as Function of cT, REAL;
reconsider f9 = f as Function of cT, REAL;
set g = Inv bf;
set gcT = g.:cT;
assume not f is with_max;
then
A5: not fcT is with_max;
then
A6: not upper_bound (fcT) in fcT by A3;
now
assume 0 in rng bf;
then consider x being object such that
A7: x in dom bf and
A8: bf.x = 0 by FUNCT_1:def 3;
reconsider x as Element of cT by A7;
bf9.x = b+(-f9).x by VALUED_1:2
.= b+-(f.x) by VALUED_1:8
.= b-f.x;
hence contradiction by A6,A8,FUNCT_2:35;
end;
then
A9: g is continuous by A4,Th11;
now
g is bounded by A1,A9;
then gcT is bounded_above by MEASURE6:def 11;
then consider p be Real such that
A10: p is UpperBound of gcT;
A11: for r be Real st r in gcT holds r <= p by A10,XXREAL_2:def 1;
per cases;
suppose
A12: p <= 0;
reconsider a19 = 1 as Real;
take a19;
thus a19 > 0;
let r be Real;
assume r in gcT;
hence r <= a19 by A11,A12;
end;
suppose
A13: p > 0;
take p;
thus p>0 by A13;
thus for r be Real st r in gcT holds r <= p by A11;
end;
end;
then consider p be Real such that
A14: p > 0 and
A15: for r be Real st r in gcT holds r <= p;
consider r be Real such that
A16: r in fcT and
A17: b-1/p < r by A3,A14,SEQ_4:def 1;
consider x being object such that
A18: x in the carrier of T and
x in the carrier of T and
A19: r = f.x by A16,FUNCT_2:64;
reconsider x as Element of T by A18;
A20: f.x <= b by A3,A16,A19,SEQ_4:def 1;
f.x <> b by A3,A5,A16,A19;
then f.x+0 < b by A20,XXREAL_0:1;
then
A21: b-f.x > 0 by XREAL_1:20;
g.x = (bf9.x)" by VALUED_1:10
.= (b+(-f9).x)" by VALUED_1:2
.= 1/(b+(-f9).x)
.= 1/(b+-(f.x)) by VALUED_1:8
.= 1/(b-f.x);
then 1/(b-f.x) <= p by A15,FUNCT_2:35;
then 1 <= p*(b-f.x) by A21,XREAL_1:81;
then 1/p <= b-f.x by A14,XREAL_1:79;
then f.x+1/p <= b by XREAL_1:19;
hence contradiction by A17,A19,XREAL_1:19;
end;
assume
A22: for f being RealMap of T st f is continuous holds f is with_max;
let f be RealMap of T;
assume
A23: f is continuous;
then f is with_max by A22;
then f.:(the carrier of T) is with_max;
then f.:(the carrier of T) is bounded_above;
hence f is bounded_above;
f is with_min by A22,A23,Th14;
then f.:(the carrier of T) is with_min;
then f.:(the carrier of T) is bounded_below;
hence thesis;
end;
definition
let T be TopStruct;
attr T is pseudocompact means
:Def4:
for f being RealMap of T st f is continuous holds f is bounded;
end;
registration
cluster compact -> pseudocompact for non empty TopSpace;
coherence
proof
let T be non empty TopSpace;
assume
A1: T is compact;
let f be RealMap of T such that
A2: f is continuous;
thus f is bounded_above
proof
set p = the Element of T;
defpred P[Real] means $1 >= f.p;
set R = {right_closed_halfline(r3) where r3 is Element of REAL : P[r3]};
A3: R is Subset-Family of REAL from DOMAIN_1:sch 8;
A4: right_closed_halfline(f.p) in R;
then reconsider R as non empty Subset-Family of REAL by A3;
reconsider F = ("f).:R as Subset-Family of T;
A5: F is c=-linear
proof
let X,Y be set;
assume X in F;
then consider A being object such that
A6: A in bool REAL and
A7: A in R and
A8: X = ("f).A by FUNCT_2:64;
reconsider A as set by TARSKI:1;
A9: X = f"A by A6,A8,MEASURE6:def 3;
consider r1 being Element of REAL such that
A10: A = right_closed_halfline(r1) and
r1 >= f.p by A7;
assume Y in F;
then consider B being object such that
A11: B in bool REAL and
A12: B in R and
A13: Y = ("f).B by FUNCT_2:64;
reconsider B as set by TARSKI:1;
A14: Y = f"B by A11,A13,MEASURE6:def 3;
consider r2 being Element of REAL such that
A15: B = right_closed_halfline(r2) and
r2 >= f.p by A12;
r1 >= r2 or r2 >= r1;
then X c= Y or Y c= X by A10,A15,A9,A14,RELAT_1:143,XXREAL_1:38;
hence thesis by XBOOLE_0:def 9;
end;
assume
A16: for s be Real holds s is not UpperBound of f.:(the carrier of T);
now
assume {} in F;
then consider rchx being object such that
A17: rchx in bool REAL and
A18: rchx in R and
A19: {} = ("f).rchx by FUNCT_2:64;
consider r3 being Element of REAL such that
A20: rchx = right_closed_halfline(r3) and
r3 >= f.p by A18;
r3 is not UpperBound of f.:(the carrier of T) by A16;
then consider r1 being ExtReal such that
A21: r1 in f.:(the carrier of T) and
A22: r1 > r3 by XXREAL_2:def 1;
reconsider rchx as set by TARSKI:1;
rchx = {g where g is Real: g >= r3} by A20,XXREAL_1:232;
then
A23: r1 in rchx by A21,A22;
A24: ex c being object st c in the carrier of T & c in the carrier of T &
r1 = f.c by A21,FUNCT_2:64;
{} = f"rchx by A17,A19,MEASURE6:def 3;
hence contradiction by A24,A23,FUNCT_2:38;
end;
then
A25: F is with_non-empty_elements by SETFAM_1:def 8;
R is closed
proof
let X be Subset of REAL;
assume X in R;
then ex r3 being Element of REAL
st X = right_closed_halfline(r3) & r3 >= f.p;
hence thesis;
end;
then
A26: F is closed by A2,Th13;
("f).right_closed_halfline(f.p) in F by A4,FUNCT_2:35;
then meet F <> {} by A1,A25,A5,A26,COMPTS_1:4;
then consider x being object such that
A27: x in meet F by XBOOLE_0:def 1;
set eR = the Element of R;
eR in R;
then consider er being Element of REAL such that
A28: eR = right_closed_halfline(er) and
A29: er >= f.p;
reconsider x as Element of T by A27;
A30: f.x in meet R by A27,MEASURE6:35;
then
A31: f.x in eR by SETFAM_1:def 1;
consider fx9 being Real such that
A32: fx9 > f.x by XREAL_1:1;
reconsider fx9 as Element of REAL by XREAL_0:def 1;
right_closed_halfline(er) = {r3:r3>=er} by XXREAL_1:232;
then ex r1 being Real st f.x = r1 & r1 >= er by A31,A28;
then f.x >= f.p by A29,XXREAL_0:2;
then fx9 >= f.p by A32,XXREAL_0:2;
then right_closed_halfline(fx9) in R;
then
A33: f.x in right_closed_halfline(fx9) by A30,SETFAM_1:def 1;
right_closed_halfline(fx9) = {r3:r3>=fx9} by XXREAL_1:232;
then ex r3 st f.x = r3 & r3 >= fx9 by A33;
hence contradiction by A32;
end;
set p = the Element of T;
defpred P[Real] means $1 <= f.p;
set R = {left_closed_halfline(r3) where r3 is Element of REAL: P[r3]};
A34: R is Subset-Family of REAL from DOMAIN_1:sch 8;
A35: left_closed_halfline(f.p) in R;
then reconsider R as non empty Subset-Family of REAL by A34;
reconsider F = ("f).:R as Subset-Family of T;
R is closed
proof
let X be Subset of REAL;
assume X in R;
then ex r3 being Element of REAL
st X = left_closed_halfline(r3) & r3 <= f.p;
hence thesis;
end;
then
A36: F is closed by A2,Th13;
A37: F is c=-linear
proof
let X,Y be set;
assume X in F;
then consider A being object such that
A38: A in bool REAL and
A39: A in R and
A40: X = ("f).A by FUNCT_2:64;
reconsider A as set by TARSKI:1;
A41: X = f"A by A38,A40,MEASURE6:def 3;
consider r1 being Element of REAL such that
A42: A = left_closed_halfline(r1) and
r1 <= f.p by A39;
assume Y in F;
then consider B being object such that
A43: B in bool REAL and
A44: B in R and
A45: Y = ("f).B by FUNCT_2:64;
reconsider B as set by TARSKI:1;
A46: Y = f"B by A43,A45,MEASURE6:def 3;
consider r2 being Element of REAL such that
A47: B = left_closed_halfline(r2) and
r2 <= f.p by A44;
r1 <= r2 or r2 <= r1;
then X c= Y or Y c= X by A42,A47,A41,A46,RELAT_1:143,XXREAL_1:42;
hence thesis by XBOOLE_0:def 9;
end;
assume
A48: for s holds s is not LowerBound of f.:(the carrier of T);
now
assume {} in F;
then consider rchx being object such that
A49: rchx in bool REAL and
A50: rchx in R and
A51: {} = ("f).rchx by FUNCT_2:64;
consider r3 being Element of REAL such that
A52: rchx = left_closed_halfline(r3) and
r3 <= f.p by A50;
r3 is not LowerBound of f.:(the carrier of T) by A48;
then consider r1 being ExtReal such that
A53: r1 in f.:(the carrier of T) and
A54: r1 < r3 by XXREAL_2:def 2;
reconsider rchx as set by TARSKI:1;
rchx = {g where g is Real: g <= r3} by A52,XXREAL_1:231;
then
A55: r1 in rchx by A53,A54;
A56: ex c being object st c in the carrier of T & c in the carrier of T & r1
= f.c by A53,FUNCT_2:64;
{} = f"rchx by A49,A51,MEASURE6:def 3;
hence contradiction by A56,A55,FUNCT_2:38;
end;
then
A57: F is with_non-empty_elements by SETFAM_1:def 8;
("f).left_closed_halfline(f.p) in F by A35,FUNCT_2:35;
then meet F <> {} by A1,A57,A37,A36,COMPTS_1:4;
then consider x being object such that
A58: x in meet F by XBOOLE_0:def 1;
set eR = the Element of R;
eR in R;
then consider er being Element of REAL such that
A59: eR = left_closed_halfline(er) and
A60: er <= f.p;
reconsider x as Element of T by A58;
A61: f.x in meet R by A58,MEASURE6:35;
then
A62: f.x in eR by SETFAM_1:def 1;
consider fx9 being Real such that
A63: fx9 < f.x by XREAL_1:2;
reconsider fx9 as Element of REAL by XREAL_0:def 1;
left_closed_halfline(er) = {r3 : r3 <= er} by XXREAL_1:231;
then ex r1 being Real st f.x = r1 & r1 <= er by A62,A59;
then f.x <= f.p by A60,XXREAL_0:2;
then fx9 <= f.p by A63,XXREAL_0:2;
then left_closed_halfline(fx9) in R;
then
A64: f.x in left_closed_halfline(fx9) by A61,SETFAM_1:def 1;
left_closed_halfline(fx9) = {r3 : r3 <= fx9} by XXREAL_1:231;
then ex r3 st f.x = r3 & r3 <= fx9 by A64;
hence contradiction by A63;
end;
end;
registration
cluster non empty compact for TopSpace;
existence
proof
set T = the non empty compact TopSpace;
take T;
thus thesis;
end;
end;
registration
let T be pseudocompact non empty TopSpace;
cluster continuous -> bounded with_max with_min for RealMap of T;
coherence
proof
let f be RealMap of T;
assume
A1: f is continuous;
hence f is bounded by Def4;
A2: for f being RealMap of T st f is continuous holds f is bounded by Def4;
hence f is with_max by A1,Th15;
for f being RealMap of T st f is continuous holds f is with_max by A2,Th15;
hence thesis by A1,Th14;
end;
end;
theorem Th16:
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)
proof
let T be non empty TopSpace, X be non empty Subset of T, Y be compact Subset
of T, f be continuous RealMap of T;
A1: (f|Y).:the carrier of (T|Y) = (f|Y).:Y by PRE_TOPC:8
.= f.:Y by RELAT_1:129;
assume
A2: X c= Y;
then reconsider Y1 = Y as non empty compact Subset of T;
A3: (f|X).:the carrier of (T|X) = (f|X).:X by PRE_TOPC:8
.= f.:X by RELAT_1:129;
(f|Y1).:the carrier of (T|Y1) is bounded_below by MEASURE6:def 10;
hence thesis by A2,A1,A3,RELAT_1:123,SEQ_4:47;
end;
theorem Th17:
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)
proof
let T be non empty TopSpace, X be non empty Subset of T, Y be compact Subset
of T, f be continuous RealMap of T;
A1: (f|Y).:the carrier of (T|Y) = (f|Y).:Y by PRE_TOPC:8
.= f.:Y by RELAT_1:129;
assume
A2: X c= Y;
then reconsider Y1 = Y as non empty compact Subset of T;
A3: (f|X).:the carrier of (T|X) = (f|X).:X by PRE_TOPC:8
.= f.:X by RELAT_1:129;
(f|Y1).:the carrier of (T|Y1) is bounded_above by MEASURE6:def 11;
hence thesis by A2,A1,A3,RELAT_1:123,SEQ_4:48;
end;
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;
coherence by COMPTS_1:11;
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
:Def5:
for p being Point of TOP-REAL 2 holds it.p = p`1;
existence
proof
deffunc F(Point of TOP-REAL 2) = In($1`1,REAL);
consider f be RealMap of TOP-REAL 2 such that
A1: for p being Point of TOP-REAL 2
holds f.p = F(p) from FUNCT_2:sch 4;
take f;
let p be Point of TOP-REAL 2;
f.p = F(p) by A1;
hence thesis;
end;
uniqueness
proof
let it1, it2 be RealMap of TOP-REAL 2 such that
A2: for p being Point of TOP-REAL 2 holds it1.p = p`1 and
A3: for p being Point of TOP-REAL 2 holds it2.p = p`1;
now
let p be Point of TOP-REAL 2;
thus it1.p = p`1 by A2
.= it2.p by A3;
end;
hence it1 = it2 by FUNCT_2:63;
end;
func proj2 -> RealMap of TOP-REAL 2 means
:Def6:
for p being Point of TOP-REAL 2 holds it.p = p`2;
existence
proof
deffunc F(Point of TOP-REAL 2) = In($1`2,REAL);
consider f be RealMap of TOP-REAL 2 such that
A4: for p being Point of TOP-REAL 2
holds f.p = F(p) from FUNCT_2:sch 4;
take f;
let p be Point of TOP-REAL 2;
f.p = F(p) by A4;
hence thesis;
end;
uniqueness
proof
let it1, it2 be RealMap of TOP-REAL 2 such that
A5: for p being Point of TOP-REAL 2 holds it1.p = p`2 and
A6: for p being Point of TOP-REAL 2 holds it2.p = p`2;
now
let p be Point of TOP-REAL 2;
thus it1.p = p`2 by A5
.= it2.p by A6;
end;
hence it1 = it2 by FUNCT_2:63;
end;
end;
theorem Th18:
proj1"].r,s.[ = {|[ r1, r2 ]| : r < r1 & r1 < s}
proof
set Q = proj1"].r,s.[;
set QQ = {|[ r1,r2 ]|: r < r1 & r1 < s};
now
let z be object;
hereby
assume
A1: z in Q;
then reconsider p = z as Point of TOP-REAL 2;
proj1.p in ].r,s.[ by A1,FUNCT_2:38;
then
A2: ex t being Real st t = proj1.p & r<t & t<s;
p`1 = proj1.p & p = |[ p`1,p`2 ]| by Def5,EUCLID:53;
hence z in QQ by A2;
end;
assume z in QQ;
then consider r1, r2 being Real such that
A3: z = |[ r1,r2 ]| and
A4: r<r1 & r1 <s;
set p = |[ r1,r2 ]|;
A5: r1 in ].r,s.[ by A4;
proj1.p = p`1 by Def5
.= r1 by EUCLID:52;
hence z in Q by A3,A5,FUNCT_2:38;
end;
hence thesis by TARSKI:2;
end;
theorem Th19:
for r3, q3 st P = {|[ r1, r2 ]| : r3 < r1 & r1 < q3} holds P is open
proof
deffunc F(Real,Real) = |[ $1,$2 ]|;
let r3, q3;
defpred P1[Real,Real] means r3 < $1;
defpred P2[Real,Real] means $1 < q3;
reconsider Q1 = {|[ r1,r2 ]|: r3 < r1}, Q2 = {|[ r1,r2 ]|: r1 < q3} as
open Subset of TOP-REAL 2 by JORDAN1:20,21;
assume
A1: P = {|[ r1, r2 ]| : r3 < r1 & r1 < q3};
now
let x be object;
hereby
assume x in P;
then consider r1, r2 being Real such that
A2: x = |[ r1, r2 ]| & r3 < r1 & r1 < q3 by A1;
x in Q1 & x in Q2 by A2;
hence x in Q1/\Q2 by XBOOLE_0:def 4;
end;
assume
A3: x in Q1/\Q2;
then x in Q1 by XBOOLE_0:def 4;
then consider r1, r2 being Real such that
A4: x = |[ r1, r2 ]| & r3 < r1;
x in Q2 by A3,XBOOLE_0:def 4;
then consider r19, r29 being Real such that
A5: x = |[ r19, r29 ]| & r19 < q3;
|[ r1, r2 ]|`1 = r1 & |[ r19, r29 ]|`1 = r19 by EUCLID:52;
hence x in P by A1,A4,A5;
end;
then
A6: P = Q1/\Q2 by TARSKI:2;
thus thesis by A6,TOPS_1:11;
end;
theorem Th20:
proj2"].r,s.[ = {|[ r1, r2 ]| : r < r2 & r2 < s}
proof
set Q = proj2"].r,s.[;
set QQ = {|[ r1,r2 ]|: r < r2 & r2 < s};
now
let z be object;
hereby
assume
A1: z in Q;
then reconsider p = z as Point of TOP-REAL 2;
proj2.p in ].r,s.[ by A1,FUNCT_2:38;
then
A2: ex t being Real st t = proj2.p & r<t & t<s;
p`2 = proj2.p & p = |[ p`1,p`2 ]| by Def6,EUCLID:53;
hence z in QQ by A2;
end;
assume z in QQ;
then consider r1, r2 being Real such that
A3: z = |[ r1,r2 ]| and
A4: r<r2 & r2 <s;
set p = |[ r1,r2 ]|;
A5: r2 in ].r,s.[ by A4;
proj2.p = p`2 by Def6
.= r2 by EUCLID:52;
hence z in Q by A3,A5,FUNCT_2:38;
end;
hence thesis by TARSKI:2;
end;
theorem Th21:
for r3, q3 st P = {|[ r1, r2 ]| : r3 < r2 & r2 < q3} holds P is open
proof
deffunc F(Real,Real) = |[ $1,$2 ]|;
let r3, q3;
defpred P1[Real,Real] means r3 < $2;
defpred P2[Real,Real] means $2 < q3;
reconsider Q1 = {|[ r1,r2 ]|: r3 < r2}, Q2 = {|[ r1,r2 ]|: r2 < q3} as
open Subset of TOP-REAL 2 by JORDAN1:22,23;
assume
A1: P = {|[ r1, r2 ]| : r3 < r2 & r2 < q3};
now
let x be object;
hereby
assume x in P;
then ex r1, r2 being Real
st x = |[ r1, r2 ]| & r3 < r2 & r2 < q3 by A1;
then x in Q1 & x in Q2;
hence x in Q1/\Q2 by XBOOLE_0:def 4;
end;
assume
A2: x in Q1/\Q2;
then x in Q1 by XBOOLE_0:def 4;
then consider r1, r2 being Real such that
A3: x = |[ r1, r2 ]| & r3 < r2;
x in Q2 by A2,XBOOLE_0:def 4;
then consider r19, r29 being Real such that
A4: x = |[ r19, r29 ]| & r29 < q3;
|[ r1, r2 ]|`2 = r2 & |[ r19, r29 ]|`2 = r29 by EUCLID:52;
hence x in P by A1,A3,A4;
end;
then
A5: P = Q1/\Q2 by TARSKI:2;
thus thesis by A5,TOPS_1:11;
end;
registration
cluster proj1 -> continuous;
coherence
proof
now
let Y be Subset of REAL;
set p1Y = (proj1"Y);
assume
A1: Y is open;
now
let x be set;
hereby
assume
A2: x in p1Y;
then reconsider p = x as Point of TOP-REAL 2;
set p1 = proj1.p;
p1 in Y by A2,FUNCT_2:38;
then consider g such that
A3: 0<g and
A4: ].p1-g,p1+g.[ c= Y by A1,RCOMP_1:19;
reconsider g as Real;
reconsider Q = proj1"].p1-g,p1+g.[ as Subset of TOP-REAL 2;
take Q;
Q = {|[ q3,p3 ]|: p1-g < q3 & q3 < p1+g} by Th18;
hence Q is open by Th19;
thus Q c= p1Y by A4,RELAT_1:143;
A5: p1 < p1+g by A3,XREAL_1:29;
then p1-g < p1 by XREAL_1:19;
then p1 in ].p1-g,p1+g.[ by A5;
hence x in Q by FUNCT_2:38;
end;
assume ex Q being Subset of TOP-REAL 2 st Q is open & Q c= p1Y & x
in Q;
hence x in p1Y;
end;
hence p1Y is open by TOPS_1:25;
end;
hence thesis by Th8;
end;
cluster proj2 -> continuous;
coherence
proof
now
let Y be Subset of REAL;
set p1Y = (proj2"Y);
assume
A6: Y is open;
now
let x be set;
hereby
assume
A7: x in p1Y;
then reconsider p = x as Point of TOP-REAL 2;
set p1 = proj2.p;
p1 in Y by A7,FUNCT_2:38;
then consider g such that
A8: 0<g and
A9: ].p1-g,p1+g.[ c= Y by A6,RCOMP_1:19;
reconsider g as Real;
reconsider Q = proj2"].p1-g,p1+g.[ as Subset of TOP-REAL 2;
take Q;
Q = {|[ q3,p3 ]|: p1-g < p3 & p3 < p1+g} by Th20;
hence Q is open by Th21;
thus Q c= p1Y by A9,RELAT_1:143;
A10: p1 < p1+g by A8,XREAL_1:29;
then p1-g < p1 by XREAL_1:19;
then p1 in ].p1-g,p1+g.[ by A10;
hence x in Q by FUNCT_2:38;
end;
assume ex Q being Subset of TOP-REAL 2 st Q is open & Q c= p1Y & x
in Q;
hence x in p1Y;
end;
hence p1Y is open by TOPS_1:25;
end;
hence thesis by Th8;
end;
end;
theorem Th22:
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
proof
let X be Subset of TOP-REAL 2, p be Point of TOP-REAL 2;
assume p in X;
hence (proj1|X).p = proj1.p by FUNCT_1:49
.= p`1 by Def5;
end;
theorem Th23:
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
proof
let X be Subset of TOP-REAL 2,p be Point of TOP-REAL 2;
assume p in X;
hence (proj2|X).p = proj2.p by FUNCT_1:49
.= p`2 by Def6;
end;
definition
let X be Subset of TOP-REAL 2;
func W-bound X -> Real equals
lower_bound (proj1|X);
coherence;
func N-bound X -> Real equals
upper_bound (proj2|X);
coherence;
func E-bound X -> Real equals
upper_bound (proj1|X);
coherence;
func S-bound X -> Real equals
lower_bound (proj2|X);
coherence;
end;
Lm3: p in X implies lower_bound (proj1|X) <= p`1 &
p`1 <= upper_bound (proj1|X) & lower_bound (proj2|X
) <= p`2 & p`2 <= upper_bound (proj2|X)
proof
assume
A1: p in X;
then reconsider p9 = p as Point of (TOP-REAL 2)|X by PRE_TOPC:8;
A2: (proj1|X) .p9 = p`1 by A1,Th22;
hence lower_bound (proj1|X) <= p`1 by Th1;
thus p`1 <= upper_bound (proj1|X) by A2,Th4;
A3: (proj2|X) .p9 = p`2 by A1,Th23;
hence lower_bound (proj2|X) <= p`2 by Th1;
thus thesis by A3,Th4;
end;
theorem
p in X implies W-bound X <= p`1 & p`1 <= E-bound X & S-bound X <= p`2
& p`2 <= N-bound X by Lm3;
definition
let X be Subset of TOP-REAL 2;
func SW-corner X -> Point of TOP-REAL 2 equals
|[W-bound X, S-bound X]|;
coherence;
func NW-corner X -> Point of TOP-REAL 2 equals
|[W-bound X, N-bound X]|;
coherence;
func NE-corner X -> Point of TOP-REAL 2 equals
|[E-bound X, N-bound X]|;
coherence;
func SE-corner X -> Point of TOP-REAL 2 equals
|[E-bound X, S-bound X]|;
coherence;
end;
theorem
(SW-corner P)`1 = (NW-corner P)`1
proof
thus (SW-corner P)`1 = W-bound P by EUCLID:52
.= (NW-corner P)`1 by EUCLID:52;
end;
theorem
(SE-corner P)`1 = (NE-corner P)`1
proof
thus (SE-corner P)`1 = E-bound P by EUCLID:52
.= (NE-corner P)`1 by EUCLID:52;
end;
theorem
(NW-corner P)`2 = (NE-corner P)`2
proof
thus (NW-corner P)`2 = N-bound P by EUCLID:52
.= (NE-corner P)`2 by EUCLID:52;
end;
theorem
(SW-corner P)`2 = (SE-corner P)`2
proof
thus (SW-corner P)`2 = S-bound P by EUCLID:52
.= (SE-corner P)`2 by EUCLID:52;
end;
definition
let X be Subset of TOP-REAL 2;
func W-most X -> Subset of TOP-REAL 2 equals
LSeg(SW-corner X, NW-corner X)
/\X;
coherence;
func N-most X -> Subset of TOP-REAL 2 equals
LSeg(NW-corner X, NE-corner X)
/\X;
coherence;
func E-most X -> Subset of TOP-REAL 2 equals
LSeg(SE-corner X, NE-corner X)
/\X;
coherence;
func S-most X -> Subset of TOP-REAL 2 equals
LSeg(SW-corner X, SE-corner X)
/\X;
coherence;
end;
registration
let X be non empty compact Subset of TOP-REAL 2;
cluster W-most X -> non empty compact;
coherence
proof
set p1X = (proj1|X), c = the carrier of (TOP-REAL 2)|X;
A1: (SW-corner X)`1 = W-bound X & (NW-corner X)`1 = W-bound X by EUCLID:52;
p1X.:c is with_min by MEASURE6:def 13;
then lower_bound (p1X.:c) in p1X.:c;
then consider p being object such that
A2: p in c and
p in c and
A3: lower_bound (p1X.:c) = p1X.p by FUNCT_2:64;
A4: c = X by PRE_TOPC:8;
then reconsider p as Point of TOP-REAL 2 by A2;
A5: p`2 <= N-bound X by A4,A2,Lm3;
A6: (SW-corner X)`2 = S-bound X & (NW-corner X)`2 = N-bound X by EUCLID:52;
p1X.p = p`1 & S-bound X <= p`2 by A4,A2,Lm3,Th22;
then p in LSeg(SW-corner X, NW-corner X) by A1,A6,A3,A5,GOBOARD7:7;
hence thesis by A4,A2,XBOOLE_0:def 4;
end;
cluster N-most X -> non empty compact;
coherence
proof
set p2X = (proj2|X), c = the carrier of (TOP-REAL 2)|X;
A7: (NW-corner X)`1 = W-bound X & (NE-corner X)`1 = E-bound X by EUCLID:52;
p2X.:c is with_max by MEASURE6:def 12;
then upper_bound (p2X.:c) in p2X.:c;
then consider p being object such that
A8: p in c and
p in c and
A9: upper_bound (p2X.:c) = p2X.p by FUNCT_2:64;
A10: c = X by PRE_TOPC:8;
then reconsider p as Point of TOP-REAL 2 by A8;
A11: p`1 <= E-bound X by A10,A8,Lm3;
A12: (NW-corner X)`2 = N-bound X & (NE-corner X)`2 = N-bound X by EUCLID:52;
p2X.p = p`2 & W-bound X <= p`1 by A10,A8,Lm3,Th23;
then p in LSeg(NW-corner X, NE-corner X) by A7,A12,A9,A11,GOBOARD7:8;
hence thesis by A10,A8,XBOOLE_0:def 4;
end;
cluster E-most X -> non empty compact;
coherence
proof
set p1X = (proj1|X), c = the carrier of (TOP-REAL 2)|X;
A13: (SE-corner X)`1 = E-bound X & (NE-corner X)`1 = E-bound X by EUCLID:52;
p1X.:c is with_max by MEASURE6:def 12;
then upper_bound (p1X.:c) in p1X.:c;
then consider p being object such that
A14: p in c and
p in c and
A15: upper_bound (p1X.:c) = p1X.p by FUNCT_2:64;
A16: c = X by PRE_TOPC:8;
then reconsider p as Point of TOP-REAL 2 by A14;
A17: p`2 <= N-bound X by A16,A14,Lm3;
A18: (SE-corner X)`2 = S-bound X & (NE-corner X)`2 = N-bound X by EUCLID:52;
p1X.p = p`1 & S-bound X <= p`2 by A16,A14,Lm3,Th22;
then p in LSeg(SE-corner X, NE-corner X) by A13,A18,A15,A17,GOBOARD7:7;
hence thesis by A16,A14,XBOOLE_0:def 4;
end;
cluster S-most X -> non empty compact;
coherence
proof
set p2X = (proj2|X), c = the carrier of (TOP-REAL 2)|X;
A19: (SW-corner X)`1 = W-bound X & (SE-corner X)`1 = E-bound X by EUCLID:52;
p2X.:c is with_min by MEASURE6:def 13;
then lower_bound (p2X.:c) in p2X.:c;
then consider p being object such that
A20: p in c and
p in c and
A21: lower_bound (p2X.:c) = p2X.p by FUNCT_2:64;
A22: c = X by PRE_TOPC:8;
then reconsider p as Point of TOP-REAL 2 by A20;
A23: p`1 <= E-bound X by A22,A20,Lm3;
A24: (SW-corner X)`2 = S-bound X & (SE-corner X)`2 = S-bound X by EUCLID:52;
p2X.p = p`2 & W-bound X <= p`1 by A22,A20,Lm3,Th23;
then p in LSeg(SW-corner X, SE-corner X) by A19,A24,A21,A23,GOBOARD7:8;
hence thesis by A22,A20,XBOOLE_0:def 4;
end;
end;
definition
let X be Subset of TOP-REAL 2;
func W-min X -> Point of TOP-REAL 2 equals
|[W-bound X, lower_bound (proj2|W-most X)]|;
coherence;
func W-max X -> Point of TOP-REAL 2 equals
|[W-bound X, upper_bound (proj2|W-most X)]|;
coherence;
func N-min X -> Point of TOP-REAL 2 equals
|[lower_bound (proj1|N-most X), N-bound X]|;
coherence;
func N-max X -> Point of TOP-REAL 2 equals
|[upper_bound (proj1|N-most X), N-bound X]|;
coherence;
func E-max X -> Point of TOP-REAL 2 equals
|[E-bound X, upper_bound (proj2|E-most X)]|;
coherence;
func E-min X -> Point of TOP-REAL 2 equals
|[E-bound X, lower_bound (proj2|E-most X)]|;
coherence;
func S-max X -> Point of TOP-REAL 2 equals
|[upper_bound (proj1|S-most X), S-bound X]|;
coherence;
func S-min X -> Point of TOP-REAL 2 equals
|[lower_bound (proj1|S-most X), S-bound X]|;
coherence;
end;
theorem Th29:
(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
proof
(W-min P)`1 = W-bound P & (W-max P)`1 = W-bound P by EUCLID:52;
hence thesis by EUCLID:52;
end;
theorem Th30:
(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
proof
set LX = W-most X;
A1: (W-min X)`2 = lower_bound (proj2|LX) by EUCLID:52;
A2: (SW-corner X)`2 = lower_bound (proj2|X) by EUCLID:52;
hence (SW-corner X)`2 <= (W-min X)`2 by A1,Th16,XBOOLE_1:17;
A3: (W-max X)`2 = upper_bound (proj2|LX) by EUCLID:52;
then
A4: (W-min X)`2 <= (W-max X)`2 by A1,Th7;
(SW-corner X)`2 <= (W-min X)`2 by A2,A1,Th16,XBOOLE_1:17;
hence
A5: (SW-corner X)`2 <= (W-max X)`2 by A4,XXREAL_0:2;
A6: (NW-corner X)`2 = upper_bound (proj2|X) by EUCLID:52;
then
A7: (W-max X)`2 <= (NW-corner X)`2 by A3,Th17,XBOOLE_1:17;
hence (SW-corner X)`2 <= (NW-corner X)`2 by A5,XXREAL_0:2;
thus (W-min X)`2 <= (W-max X)`2 by A1,A3,Th7;
thus (W-min X)`2 <= (NW-corner X)`2 by A4,A7,XXREAL_0:2;
thus thesis by A3,A6,Th17,XBOOLE_1:17;
end;
theorem Th31:
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)
proof
A1: (SW-corner Z)`1 = W-bound Z & (W-min Z)`1 = W-bound Z by EUCLID:52;
A2: (NW-corner Z)`1 = W-bound Z by EUCLID:52;
assume
A3: p in W-most Z;
then p in LSeg(SW-corner Z, NW-corner Z) by XBOOLE_0:def 4;
hence p`1 = (W-min Z)`1 by A1,A2,GOBOARD7:5;
assume Z is compact;
then reconsider Z as non empty compact Subset of TOP-REAL 2;
(W-min Z)`2 = lower_bound (proj2|W-most Z) &
(W-max Z)`2 = upper_bound (proj2|W-most Z )
by EUCLID:52;
hence thesis by A3,Lm3;
end;
theorem Th32:
W-most X c= LSeg(W-min X, W-max X)
proof
let x be object;
assume
A1: x in W-most X;
then reconsider p = x as Point of TOP-REAL 2;
A2: p`2 <=(W-max X)`2 by A1,Th31;
A3: (W-min X)`1 = (W-max X)`1 by Th29;
p`1 = (W-min X)`1 & (W-min X)`2 <= p`2 by A1,Th31;
hence thesis by A3,A2,GOBOARD7:7;
end;
theorem
LSeg(W-min X, W-max X) c= LSeg(SW-corner X, NW-corner X)
proof
A1: (SW-corner X)`1 = W-bound X & (NW-corner X)`1 = W-bound X by EUCLID:52;
A2: (W-max X)`2 <= (NW-corner X)`2 by Th30;
(W-max X)`1 = W-bound X & (SW-corner X)`2 <= (W-max X)`2 by Th30,EUCLID:52;
then
A3: W-max X in LSeg(SW-corner X, NW-corner X) by A1,A2,GOBOARD7:7;
A4: (W-min X)`2 <= (NW-corner X)`2 by Th30;
(W-min X)`1 = W-bound X & (SW-corner X)`2 <= (W-min X)`2 by Th30,EUCLID:52;
then W-min X in LSeg(SW-corner X, NW-corner X) by A1,A4,GOBOARD7:7;
hence thesis by A3,TOPREAL1:6;
end;
theorem Th34:
W-min X in W-most X & W-max X in W-most X
proof
set p2W = (proj2|W-most X), c = the carrier of (TOP-REAL 2)|W-most X;
A1: (SW-corner X)`1 = W-bound X & (NW-corner X)`1 = W-bound X by EUCLID:52;
p2W.:c is with_min by MEASURE6:def 13;
then lower_bound (p2W.:c) in p2W.:c;
then consider p being object such that
A2: p in c and
p in c and
A3: lower_bound (p2W.:c) = p2W.p by FUNCT_2:64;
A4: c = W-most X by PRE_TOPC:8;
then reconsider p as Point of TOP-REAL 2 by A2;
p in LSeg(SW-corner X, NW-corner X) by A4,A2,XBOOLE_0:def 4;
then
A5: p`1 = W-bound X by A1,GOBOARD7:5;
A6: (SW-corner X)`1 = W-bound X & (NW-corner X)`1 = W-bound X by EUCLID:52;
p2W.p = p`2 by A4,A2,Th23;
hence W-min X in W-most X by A4,A2,A3,A5,EUCLID:53;
p2W.:c is with_max by MEASURE6:def 12;
then upper_bound (p2W.:c) in p2W.:c;
then consider p being object such that
A7: p in c and
p in c and
A8: upper_bound (p2W.:c) = p2W.p by FUNCT_2:64;
reconsider p as Point of TOP-REAL 2 by A4,A7;
p in LSeg(SW-corner X, NW-corner X) by A4,A7,XBOOLE_0:def 4;
then
A9: p`1 = W-bound X by A6,GOBOARD7:5;
p2W.p = p`2 by A4,A7,Th23;
hence thesis by A4,A7,A8,A9,EUCLID:53;
end;
theorem
LSeg(SW-corner X, W-min X)/\X = {W-min X} & LSeg(W-max X, NW-corner X)
/\X = {W-max X}
proof
now
let x be object;
A1: W-min X in LSeg(SW-corner X, W-min X) by RLTOPSP1:68;
hereby
W-min X in W-most X by Th34;
then SW-corner X in LSeg(SW-corner X, NW-corner X) & W-min X in LSeg(
SW-corner X, NW-corner X) by RLTOPSP1:68,XBOOLE_0:def 4;
then
A2: LSeg
(SW-corner X, W-min X) c= LSeg(SW-corner X, NW-corner X) by TOPREAL1:6;
assume
A3: x in LSeg(SW-corner X, W-min X)/\X;
then
A4: x in LSeg(SW-corner X, W-min X) by XBOOLE_0:def 4;
reconsider p = x as Point of TOP-REAL 2 by A3;
x in X by A3,XBOOLE_0:def 4;
then p in W-most X by A4,A2,XBOOLE_0:def 4;
then
A5: (W-min X)`2 <= p`2 by Th31;
(SW-corner X)`2 <= (W-min X)`2 by Th30;
then p`2 <= (W-min X)`2 by A4,TOPREAL1:4;
then
A6: p`2 = (W-min X)`2 by A5,XXREAL_0:1;
(SW-corner X)`1 = (W-min X)`1 by Th29;
then
A7: p`1 = (W-min X)`1 by A4,GOBOARD7:5;
p = |[p`1, p`2]| by EUCLID:53;
hence x = W-min X by A7,A6,EUCLID:53;
end;
W-min X in W-most X by Th34;
then
A8: W-min X in X by XBOOLE_0:def 4;
assume x = W-min X;
hence x in LSeg(SW-corner X, W-min X)/\X by A8,A1,XBOOLE_0:def 4;
end;
hence LSeg(SW-corner X, W-min X)/\X = {W-min X} by TARSKI:def 1;
now
let x be object;
A9: W-max X in LSeg(W-max X, NW-corner X) by RLTOPSP1:68;
hereby
W-max X in W-most X by Th34;
then NW-corner X in LSeg(SW-corner X, NW-corner X) & W-max X in LSeg(
SW-corner X, NW-corner X) by RLTOPSP1:68,XBOOLE_0:def 4;
then
A10: LSeg
(W-max X, NW-corner X) c= LSeg(SW-corner X, NW-corner X) by TOPREAL1:6;
assume
A11: x in LSeg(W-max X, NW-corner X)/\X;
then
A12: x in LSeg(W-max X, NW-corner X) by XBOOLE_0:def 4;
reconsider p = x as Point of TOP-REAL 2 by A11;
x in X by A11,XBOOLE_0:def 4;
then p in W-most X by A12,A10,XBOOLE_0:def 4;
then
A13: p`2 <= (W-max X)`2 by Th31;
(W-max X)`2 <= (NW-corner X)`2 by Th30;
then (W-max X)`2 <= p`2 by A12,TOPREAL1:4;
then
A14: p`2 = (W-max X)`2 by A13,XXREAL_0:1;
(NW-corner X)`1 = (W-max X)`1 by Th29;
then
A15: p`1 = (W-max X)`1 by A12,GOBOARD7:5;
p = |[p`1, p`2]| by EUCLID:53;
hence x = W-max X by A15,A14,EUCLID:53;
end;
W-max X in W-most X by Th34;
then
A16: W-max X in X by XBOOLE_0:def 4;
assume x = W-max X;
hence x in LSeg(W-max X, NW-corner X)/\X by A16,A9,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem
W-min X = W-max X implies W-most X = {W-min X}
proof
assume W-min X = W-max X;
then W-most X c= LSeg(W-min X, W-min X) by Th32;
then W-most X c= {W-min X} by RLTOPSP1:70;
hence thesis by ZFMISC_1:33;
end;
theorem Th37:
(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
proof
(N-min P)`2 = N-bound P & (N-max P)`2 = N-bound P by EUCLID:52;
hence thesis by EUCLID:52;
end;
theorem Th38:
(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
proof
set LX = N-most X;
A1: (N-min X)`1 = lower_bound (proj1|LX) by EUCLID:52;
A2: (NW-corner X)`1 = lower_bound (proj1|X) by EUCLID:52;
hence (NW-corner X)`1 <= (N-min X)`1 by A1,Th16,XBOOLE_1:17;
A3: (N-max X)`1 = upper_bound (proj1|LX) by EUCLID:52;
then
A4: (N-min X)`1 <= (N-max X)`1 by A1,Th7;
(NW-corner X)`1 <= (N-min X)`1 by A2,A1,Th16,XBOOLE_1:17;
hence
A5: (NW-corner X)`1 <= (N-max X)`1 by A4,XXREAL_0:2;
A6: (NE-corner X)`1 = upper_bound (proj1|X) by EUCLID:52;
then
A7: (N-max X)`1 <= (NE-corner X)`1 by A3,Th17,XBOOLE_1:17;
hence (NW-corner X)`1 <= (NE-corner X)`1 by A5,XXREAL_0:2;
thus (N-min X)`1 <= (N-max X)`1 by A1,A3,Th7;
thus (N-min X)`1 <= (NE-corner X)`1 by A4,A7,XXREAL_0:2;
thus thesis by A3,A6,Th17,XBOOLE_1:17;
end;
theorem Th39:
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)
proof
A1: (NW-corner Z)`2 = N-bound Z & (N-min Z)`2 = N-bound Z by EUCLID:52;
A2: (NE-corner Z)`2 = N-bound Z by EUCLID:52;
assume
A3: p in N-most Z;
then p in LSeg(NW-corner Z, NE-corner Z) by XBOOLE_0:def 4;
hence p`2 = (N-min Z)`2 by A1,A2,GOBOARD7:6;
assume Z is compact;
then reconsider Z as non empty compact Subset of TOP-REAL 2;
(N-min Z)`1 = lower_bound (proj1|N-most Z) &
(N-max Z)`1 = upper_bound (proj1|N-most Z )
by EUCLID:52;
hence thesis by A3,Lm3;
end;
theorem Th40:
N-most X c= LSeg(N-min X, N-max X)
proof
let x be object;
assume
A1: x in N-most X;
then reconsider p = x as Point of TOP-REAL 2;
A2: p`1 <=(N-max X)`1 by A1,Th39;
A3: (N-min X)`2 = (N-max X)`2 by Th37;
p`2 = (N-min X)`2 & (N-min X)`1 <= p`1 by A1,Th39;
hence thesis by A3,A2,GOBOARD7:8;
end;
theorem
LSeg(N-min X, N-max X) c= LSeg(NW-corner X, NE-corner X)
proof
A1: (NW-corner X)`2 = N-bound X & (NE-corner X)`2 = N-bound X by EUCLID:52;
A2: (N-max X)`1 <= (NE-corner X)`1 by Th38;
(N-max X)`2 = N-bound X & (NW-corner X)`1 <= (N-max X)`1 by Th38,EUCLID:52;
then
A3: N-max X in LSeg(NW-corner X, NE-corner X) by A1,A2,GOBOARD7:8;
A4: (N-min X)`1 <= (NE-corner X)`1 by Th38;
(N-min X)`2 = N-bound X & (NW-corner X)`1 <= (N-min X)`1 by Th38,EUCLID:52;
then N-min X in LSeg(NW-corner X, NE-corner X) by A1,A4,GOBOARD7:8;
hence thesis by A3,TOPREAL1:6;
end;
theorem Th42:
N-min X in N-most X & N-max X in N-most X
proof
set p2W = (proj1|N-most X), c = the carrier of (TOP-REAL 2)|N-most X;
A1: (NW-corner X)`2 = N-bound X & (NE-corner X)`2 = N-bound X by EUCLID:52;
p2W.:c is with_min by MEASURE6:def 13;
then lower_bound (p2W.:c) in p2W.:c;
then consider p being object such that
A2: p in c and
p in c and
A3: lower_bound (p2W.:c) = p2W.p by FUNCT_2:64;
A4: c = N-most X by PRE_TOPC:8;
then reconsider p as Point of TOP-REAL 2 by A2;
p in LSeg(NW-corner X, NE-corner X) by A4,A2,XBOOLE_0:def 4;
then
A5: p`2 = N-bound X by A1,GOBOARD7:6;
A6: (NW-corner X)`2 = N-bound X & (NE-corner X)`2 = N-bound X by EUCLID:52;
p2W.p = p`1 by A4,A2,Th22;
hence N-min X in N-most X by A4,A2,A3,A5,EUCLID:53;
p2W.:c is with_max by MEASURE6:def 12;
then upper_bound (p2W.:c) in p2W.:c;
then consider p being object such that
A7: p in c and
p in c and
A8: upper_bound (p2W.:c) = p2W.p by FUNCT_2:64;
reconsider p as Point of TOP-REAL 2 by A4,A7;
p in LSeg(NW-corner X, NE-corner X) by A4,A7,XBOOLE_0:def 4;
then
A9: p`2 = N-bound X by A6,GOBOARD7:6;
p2W.p = p`1 by A4,A7,Th22;
hence thesis by A4,A7,A8,A9,EUCLID:53;
end;
theorem
LSeg(NW-corner X, N-min X)/\X = {N-min X} & LSeg(N-max X, NE-corner X)
/\X = {N-max X}
proof
now
let x be object;
A1: N-min X in LSeg(NW-corner X, N-min X) by RLTOPSP1:68;
hereby
N-min X in N-most X by Th42;
then NW-corner X in LSeg(NW-corner X, NE-corner X) & N-min X in LSeg(
NW-corner X, NE-corner X) by RLTOPSP1:68,XBOOLE_0:def 4;
then
A2: LSeg
(NW-corner X, N-min X) c= LSeg(NW-corner X, NE-corner X) by TOPREAL1:6;
assume
A3: x in LSeg(NW-corner X, N-min X)/\X;
then
A4: x in LSeg(NW-corner X, N-min X) by XBOOLE_0:def 4;
reconsider p = x as Point of TOP-REAL 2 by A3;
x in X by A3,XBOOLE_0:def 4;
then p in N-most X by A4,A2,XBOOLE_0:def 4;
then
A5: (N-min X)`1 <= p`1 by Th39;
(NW-corner X)`1 <= (N-min X)`1 by Th38;
then p`1 <= (N-min X)`1 by A4,TOPREAL1:3;
then
A6: p`1 = (N-min X)`1 by A5,XXREAL_0:1;
(NW-corner X)`2 = (N-min X)`2 by Th37;
then
A7: p`2 = (N-min X)`2 by A4,GOBOARD7:6;
p = |[p`1, p`2]| by EUCLID:53;
hence x = N-min X by A7,A6,EUCLID:53;
end;
N-min X in N-most X by Th42;
then
A8: N-min X in X by XBOOLE_0:def 4;
assume x = N-min X;
hence x in LSeg(NW-corner X, N-min X)/\X by A8,A1,XBOOLE_0:def 4;
end;
hence LSeg(NW-corner X, N-min X)/\X = {N-min X} by TARSKI:def 1;
now
let x be object;
A9: N-max X in LSeg(N-max X, NE-corner X) by RLTOPSP1:68;
hereby
N-max X in N-most X by Th42;
then NE-corner X in LSeg(NW-corner X, NE-corner X) & N-max X in LSeg(
NW-corner X, NE-corner X) by RLTOPSP1:68,XBOOLE_0:def 4;
then
A10: LSeg
(N-max X, NE-corner X) c= LSeg(NW-corner X, NE-corner X) by TOPREAL1:6;
assume
A11: x in LSeg(N-max X, NE-corner X)/\X;
then
A12: x in LSeg(N-max X, NE-corner X) by XBOOLE_0:def 4;
reconsider p = x as Point of TOP-REAL 2 by A11;
x in X by A11,XBOOLE_0:def 4;
then p in N-most X by A12,A10,XBOOLE_0:def 4;
then
A13: p`1 <= (N-max X)`1 by Th39;
(N-max X)`1 <= (NE-corner X)`1 by Th38;
then (N-max X)`1 <= p`1 by A12,TOPREAL1:3;
then
A14: p`1 = (N-max X)`1 by A13,XXREAL_0:1;
(NE-corner X)`2 = (N-max X)`2 by Th37;
then
A15: p`2 = (N-max X)`2 by A12,GOBOARD7:6;
p = |[p`1, p`2]| by EUCLID:53;
hence x = N-max X by A15,A14,EUCLID:53;
end;
N-max X in N-most X by Th42;
then
A16: N-max X in X by XBOOLE_0:def 4;
assume x = N-max X;
hence x in LSeg(N-max X, NE-corner X)/\X by A16,A9,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem
N-min X = N-max X implies N-most X = {N-min X}
proof
assume N-min X = N-max X;
then N-most X c= LSeg(N-min X, N-min X) by Th40;
then N-most X c= {N-min X} by RLTOPSP1:70;
hence thesis by ZFMISC_1:33;
end;
theorem Th45:
(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
proof
(E-min P)`1 = E-bound P & (E-max P)`1 = E-bound P by EUCLID:52;
hence thesis by EUCLID:52;
end;
theorem Th46:
(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
proof
set LX = E-most X;
A1: (E-min X)`2 = lower_bound (proj2|LX) by EUCLID:52;
A2: (SE-corner X)`2 = lower_bound (proj2|X) by EUCLID:52;
hence (SE-corner X)`2 <= (E-min X)`2 by A1,Th16,XBOOLE_1:17;
A3: (E-max X)`2 = upper_bound (proj2|LX) by EUCLID:52;
then
A4: (E-min X)`2 <= (E-max X)`2 by A1,Th7;
(SE-corner X)`2 <= (E-min X)`2 by A2,A1,Th16,XBOOLE_1:17;
hence
A5: (SE-corner X)`2 <= (E-max X)`2 by A4,XXREAL_0:2;
A6: (NE-corner X)`2 = upper_bound (proj2|X) by EUCLID:52;
then
A7: (E-max X)`2 <= (NE-corner X)`2 by A3,Th17,XBOOLE_1:17;
hence (SE-corner X)`2 <= (NE-corner X)`2 by A5,XXREAL_0:2;
thus (E-min X)`2 <= (E-max X)`2 by A1,A3,Th7;
thus (E-min X)`2 <= (NE-corner X)`2 by A4,A7,XXREAL_0:2;
thus thesis by A3,A6,Th17,XBOOLE_1:17;
end;
theorem Th47:
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)
proof
A1: (SE-corner Z)`1 = E-bound Z & (E-min Z)`1 = E-bound Z by EUCLID:52;
A2: (NE-corner Z)`1 = E-bound Z by EUCLID:52;
assume
A3: p in E-most Z;
then p in LSeg(SE-corner Z, NE-corner Z) by XBOOLE_0:def 4;
hence p`1 = (E-min Z)`1 by A1,A2,GOBOARD7:5;
assume Z is compact;
then reconsider Z as non empty compact Subset of TOP-REAL 2;
(E-min Z)`2 = lower_bound (proj2|E-most Z) &
(E-max Z)`2 = upper_bound (proj2|E-most Z )
by EUCLID:52;
hence thesis by A3,Lm3;
end;
theorem Th48:
E-most X c= LSeg(E-min X, E-max X)
proof
let x be object;
assume
A1: x in E-most X;
then reconsider p = x as Point of TOP-REAL 2;
A2: p`2 <=(E-max X)`2 by A1,Th47;
A3: (E-min X)`1 = (E-max X)`1 by Th45;
p`1 = (E-min X)`1 & (E-min X)`2 <= p`2 by A1,Th47;
hence thesis by A3,A2,GOBOARD7:7;
end;
theorem
LSeg(E-min X, E-max X) c= LSeg(SE-corner X, NE-corner X)
proof
A1: (SE-corner X)`1 = E-bound X & (NE-corner X)`1 = E-bound X by EUCLID:52;
A2: (E-max X)`2 <= (NE-corner X)`2 by Th46;
(E-max X)`1 = E-bound X & (SE-corner X)`2 <= (E-max X)`2 by Th46,EUCLID:52;
then
A3: E-max X in LSeg(SE-corner X, NE-corner X) by A1,A2,GOBOARD7:7;
A4: (E-min X)`2 <= (NE-corner X)`2 by Th46;
(E-min X)`1 = E-bound X & (SE-corner X)`2 <= (E-min X)`2 by Th46,EUCLID:52;
then E-min X in LSeg(SE-corner X, NE-corner X) by A1,A4,GOBOARD7:7;
hence thesis by A3,TOPREAL1:6;
end;
theorem Th50:
E-min X in E-most X & E-max X in E-most X
proof
set p2W = (proj2|E-most X), c = the carrier of (TOP-REAL 2)|E-most X;
A1: (SE-corner X)`1 = E-bound X & (NE-corner X)`1 = E-bound X by EUCLID:52;
p2W.:c is with_min by MEASURE6:def 13;
then lower_bound (p2W.:c) in p2W.:c;
then consider p being object such that
A2: p in c and
p in c and
A3: lower_bound (p2W.:c) = p2W.p by FUNCT_2:64;
A4: c = E-most X by PRE_TOPC:8;
then reconsider p as Point of TOP-REAL 2 by A2;
p in LSeg(SE-corner X, NE-corner X) by A4,A2,XBOOLE_0:def 4;
then
A5: p`1 = E-bound X by A1,GOBOARD7:5;
A6: (SE-corner X)`1 = E-bound X & (NE-corner X)`1 = E-bound X by EUCLID:52;
p2W.p = p`2 by A4,A2,Th23;
hence E-min X in E-most X by A4,A2,A3,A5,EUCLID:53;
p2W.:c is with_max by MEASURE6:def 12;
then upper_bound (p2W.:c) in p2W.:c;
then consider p being object such that
A7: p in c and
p in c and
A8: upper_bound (p2W.:c) = p2W.p by FUNCT_2:64;
reconsider p as Point of TOP-REAL 2 by A4,A7;
p in LSeg(SE-corner X, NE-corner X) by A4,A7,XBOOLE_0:def 4;
then
A9: p`1 = E-bound X by A6,GOBOARD7:5;
p2W.p = p`2 by A4,A7,Th23;
hence thesis by A4,A7,A8,A9,EUCLID:53;
end;
theorem
LSeg(SE-corner X, E-min X)/\X = {E-min X} & LSeg(E-max X, NE-corner X)
/\X = {E-max X}
proof
now
let x be object;
A1: E-min X in LSeg(SE-corner X, E-min X) by RLTOPSP1:68;
hereby
E-min X in E-most X by Th50;
then SE-corner X in LSeg(SE-corner X, NE-corner X) & E-min X in LSeg(
SE-corner X, NE-corner X) by RLTOPSP1:68,XBOOLE_0:def 4;
then
A2: LSeg
(SE-corner X, E-min X) c= LSeg(SE-corner X, NE-corner X) by TOPREAL1:6;
assume
A3: x in LSeg(SE-corner X, E-min X)/\X;
then
A4: x in LSeg(SE-corner X, E-min X) by XBOOLE_0:def 4;
reconsider p = x as Point of TOP-REAL 2 by A3;
x in X by A3,XBOOLE_0:def 4;
then p in E-most X by A4,A2,XBOOLE_0:def 4;
then
A5: (E-min X)`2 <= p`2 by Th47;
(SE-corner X)`2 <= (E-min X)`2 by Th46;
then p`2 <= (E-min X)`2 by A4,TOPREAL1:4;
then
A6: p`2 = (E-min X)`2 by A5,XXREAL_0:1;
(SE-corner X)`1 = (E-min X)`1 by Th45;
then
A7: p`1 = (E-min X)`1 by A4,GOBOARD7:5;
p = |[p`1, p`2]| by EUCLID:53;
hence x = E-min X by A7,A6,EUCLID:53;
end;
E-min X in E-most X by Th50;
then
A8: E-min X in X by XBOOLE_0:def 4;
assume x = E-min X;
hence x in LSeg(SE-corner X, E-min X)/\X by A8,A1,XBOOLE_0:def 4;
end;
hence LSeg(SE-corner X, E-min X)/\X = {E-min X} by TARSKI:def 1;
now
let x be object;
A9: E-max X in LSeg(E-max X, NE-corner X) by RLTOPSP1:68;
hereby
E-max X in E-most X by Th50;
then NE-corner X in LSeg(SE-corner X, NE-corner X) & E-max X in LSeg(
SE-corner X, NE-corner X) by RLTOPSP1:68,XBOOLE_0:def 4;
then
A10: LSeg
(E-max X, NE-corner X) c= LSeg(SE-corner X, NE-corner X) by TOPREAL1:6;
assume
A11: x in LSeg(E-max X, NE-corner X)/\X;
then
A12: x in LSeg(E-max X, NE-corner X) by XBOOLE_0:def 4;
reconsider p = x as Point of TOP-REAL 2 by A11;
x in X by A11,XBOOLE_0:def 4;
then p in E-most X by A12,A10,XBOOLE_0:def 4;
then
A13: p`2 <= (E-max X)`2 by Th47;
(E-max X)`2 <= (NE-corner X)`2 by Th46;
then (E-max X)`2 <= p`2 by A12,TOPREAL1:4;
then
A14: p`2 = (E-max X)`2 by A13,XXREAL_0:1;
(NE-corner X)`1 = (E-max X)`1 by Th45;
then
A15: p`1 = (E-max X)`1 by A12,GOBOARD7:5;
p = |[p`1, p`2]| by EUCLID:53;
hence x = E-max X by A15,A14,EUCLID:53;
end;
E-max X in E-most X by Th50;
then
A16: E-max X in X by XBOOLE_0:def 4;
assume x = E-max X;
hence x in LSeg(E-max X, NE-corner X)/\X by A16,A9,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem
E-min X = E-max X implies E-most X = {E-min X}
proof
assume E-min X = E-max X;
then E-most X c= LSeg(E-min X, E-min X) by Th48;
then E-most X c= {E-min X} by RLTOPSP1:70;
hence thesis by ZFMISC_1:33;
end;
theorem Th53:
(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
proof
(S-min P)`2 = S-bound P & (S-max P)`2 = S-bound P by EUCLID:52;
hence thesis by EUCLID:52;
end;
theorem Th54:
(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
proof
set LX = S-most X;
A1: (S-min X)`1 = lower_bound (proj1|LX) by EUCLID:52;
A2: (SW-corner X)`1 = lower_bound (proj1|X) by EUCLID:52;
hence (SW-corner X)`1 <= (S-min X)`1 by A1,Th16,XBOOLE_1:17;
A3: (S-max X)`1 = upper_bound (proj1|LX) by EUCLID:52;
then
A4: (S-min X)`1 <= (S-max X)`1 by A1,Th7;
(SW-corner X)`1 <= (S-min X)`1 by A2,A1,Th16,XBOOLE_1:17;
hence
A5: (SW-corner X)`1 <= (S-max X)`1 by A4,XXREAL_0:2;
A6: (SE-corner X)`1 = upper_bound (proj1|X) by EUCLID:52;
then
A7: (S-max X)`1 <= (SE-corner X)`1 by A3,Th17,XBOOLE_1:17;
hence (SW-corner X)`1 <= (SE-corner X)`1 by A5,XXREAL_0:2;
thus (S-min X)`1 <= (S-max X)`1 by A1,A3,Th7;
thus (S-min X)`1 <= (SE-corner X)`1 by A4,A7,XXREAL_0:2;
thus thesis by A3,A6,Th17,XBOOLE_1:17;
end;
theorem Th55:
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)
proof
A1: (SW-corner Z)`2 = S-bound Z & (S-min Z)`2 = S-bound Z by EUCLID:52;
A2: (SE-corner Z)`2 = S-bound Z by EUCLID:52;
assume
A3: p in S-most Z;
then p in LSeg(SW-corner Z, SE-corner Z) by XBOOLE_0:def 4;
hence p`2 = (S-min Z)`2 by A1,A2,GOBOARD7:6;
assume Z is compact;
then reconsider Z as non empty compact Subset of TOP-REAL 2;
(S-min Z)`1 = lower_bound (proj1|S-most Z) &
(S-max Z)`1 = upper_bound (proj1|S-most Z )
by EUCLID:52;
hence thesis by A3,Lm3;
end;
theorem Th56:
S-most X c= LSeg(S-min X, S-max X)
proof
let x be object;
assume
A1: x in S-most X;
then reconsider p = x as Point of TOP-REAL 2;
A2: p`1 <=(S-max X)`1 by A1,Th55;
A3: (S-min X)`2 = (S-max X)`2 by Th53;
p`2 = (S-min X)`2 & (S-min X)`1 <= p`1 by A1,Th55;
hence thesis by A3,A2,GOBOARD7:8;
end;
theorem
LSeg(S-min X, S-max X) c= LSeg(SW-corner X, SE-corner X)
proof
A1: (SW-corner X)`2 = S-bound X & (SE-corner X)`2 = S-bound X by EUCLID:52;
A2: (S-max X)`1 <= (SE-corner X)`1 by Th54;
(S-max X)`2 = S-bound X & (SW-corner X)`1 <= (S-max X)`1 by Th54,EUCLID:52;
then
A3: S-max X in LSeg(SW-corner X, SE-corner X) by A1,A2,GOBOARD7:8;
A4: (S-min X)`1 <= (SE-corner X)`1 by Th54;
(S-min X)`2 = S-bound X & (SW-corner X)`1 <= (S-min X)`1 by Th54,EUCLID:52;
then S-min X in LSeg(SW-corner X, SE-corner X) by A1,A4,GOBOARD7:8;
hence thesis by A3,TOPREAL1:6;
end;
theorem Th58:
S-min X in S-most X & S-max X in S-most X
proof
set p2W = (proj1|S-most X), c = the carrier of (TOP-REAL 2)|S-most X;
A1: (SW-corner X)`2 = S-bound X & (SE-corner X)`2 = S-bound X by EUCLID:52;
p2W.:c is with_min by MEASURE6:def 13;
then lower_bound (p2W.:c) in p2W.:c;
then consider p being object such that
A2: p in c and
p in c and
A3: lower_bound (p2W.:c) = p2W.p by FUNCT_2:64;
A4: c = S-most X by PRE_TOPC:8;
then reconsider p as Point of TOP-REAL 2 by A2;
p in LSeg(SW-corner X, SE-corner X) by A4,A2,XBOOLE_0:def 4;
then
A5: p`2 = S-bound X by A1,GOBOARD7:6;
A6: (SW-corner X)`2 = S-bound X & (SE-corner X)`2 = S-bound X by EUCLID:52;
p2W.p = p`1 by A4,A2,Th22;
hence S-min X in S-most X by A4,A2,A3,A5,EUCLID:53;
p2W.:c is with_max by MEASURE6:def 12;
then upper_bound (p2W.:c) in p2W.:c;
then consider p being object such that
A7: p in c and
p in c and
A8: upper_bound (p2W.:c) = p2W.p by FUNCT_2:64;
reconsider p as Point of TOP-REAL 2 by A4,A7;
p in LSeg(SW-corner X, SE-corner X) by A4,A7,XBOOLE_0:def 4;
then
A9: p`2 = S-bound X by A6,GOBOARD7:6;
p2W.p = p`1 by A4,A7,Th22;
hence thesis by A4,A7,A8,A9,EUCLID:53;
end;
theorem
LSeg(SW-corner X, S-min X)/\X = {S-min X} & LSeg(S-max X, SE-corner X)
/\X = {S-max X}
proof
now
let x be object;
A1: S-min X in LSeg(SW-corner X, S-min X) by RLTOPSP1:68;
hereby
S-min X in S-most X by Th58;
then SW-corner X in LSeg(SW-corner X, SE-corner X) & S-min X in LSeg(
SW-corner X, SE-corner X) by RLTOPSP1:68,XBOOLE_0:def 4;
then
A2: LSeg
(SW-corner X, S-min X) c= LSeg(SW-corner X, SE-corner X) by TOPREAL1:6;
assume
A3: x in LSeg(SW-corner X, S-min X)/\X;
then
A4: x in LSeg(SW-corner X, S-min X) by XBOOLE_0:def 4;
reconsider p = x as Point of TOP-REAL 2 by A3;
x in X by A3,XBOOLE_0:def 4;
then p in S-most X by A4,A2,XBOOLE_0:def 4;
then
A5: (S-min X)`1 <= p`1 by Th55;
(SW-corner X)`1 <= (S-min X)`1 by Th54;
then p`1 <= (S-min X)`1 by A4,TOPREAL1:3;
then
A6: p`1 = (S-min X)`1 by A5,XXREAL_0:1;
(SW-corner X)`2 = (S-min X)`2 by Th53;
then
A7: p`2 = (S-min X)`2 by A4,GOBOARD7:6;
p = |[p`1, p`2]| by EUCLID:53;
hence x = S-min X by A7,A6,EUCLID:53;
end;
S-min X in S-most X by Th58;
then
A8: S-min X in X by XBOOLE_0:def 4;
assume x = S-min X;
hence x in LSeg(SW-corner X, S-min X)/\X by A8,A1,XBOOLE_0:def 4;
end;
hence LSeg(SW-corner X, S-min X)/\X = {S-min X} by TARSKI:def 1;
now
let x be object;
A9: S-max X in LSeg(S-max X, SE-corner X) by RLTOPSP1:68;
hereby
S-max X in S-most X by Th58;
then SE-corner X in LSeg(SW-corner X, SE-corner X) & S-max X in LSeg(
SW-corner X, SE-corner X) by RLTOPSP1:68,XBOOLE_0:def 4;
then
A10: LSeg
(S-max X, SE-corner X) c= LSeg(SW-corner X, SE-corner X) by TOPREAL1:6;
assume
A11: x in LSeg(S-max X, SE-corner X)/\X;
then
A12: x in LSeg(S-max X, SE-corner X) by XBOOLE_0:def 4;
reconsider p = x as Point of TOP-REAL 2 by A11;
x in X by A11,XBOOLE_0:def 4;
then p in S-most X by A12,A10,XBOOLE_0:def 4;
then
A13: p`1 <= (S-max X)`1 by Th55;
(S-max X)`1 <= (SE-corner X)`1 by Th54;
then (S-max X)`1 <= p`1 by A12,TOPREAL1:3;
then
A14: p`1 = (S-max X)`1 by A13,XXREAL_0:1;
(SE-corner X)`2 = (S-max X)`2 by Th53;
then
A15: p`2 = (S-max X)`2 by A12,GOBOARD7:6;
p = |[p`1, p`2]| by EUCLID:53;
hence x = S-max X by A15,A14,EUCLID:53;
end;
S-max X in S-most X by Th58;
then
A16: S-max X in X by XBOOLE_0:def 4;
assume x = S-max X;
hence x in LSeg(S-max X, SE-corner X)/\X by A16,A9,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem
S-min X = S-max X implies S-most X = {S-min X}
proof
assume S-min X = S-max X;
then S-most X c= LSeg(S-min X, S-min X) by Th56;
then S-most X c= {S-min X} by RLTOPSP1:70;
hence thesis by ZFMISC_1:33;
end;
:: Degenerate cases
theorem
W-max P = N-min P implies W-max P = NW-corner P
proof
A1: (W-max P)`1 = W-bound P by EUCLID:52;
assume W-max P = N-min P;
hence thesis by A1,EUCLID:52;
end;
theorem
N-max P = E-max P implies N-max P = NE-corner P
proof
A1: (N-max P)`2 = N-bound P by EUCLID:52;
assume N-max P = E-max P;
hence thesis by A1,EUCLID:52;
end;
theorem
E-min P = S-max P implies E-min P = SE-corner P
proof
A1: (E-min P)`1 = E-bound P by EUCLID:52;
assume E-min P = S-max P;
hence thesis by A1,EUCLID:52;
end;
theorem
S-min P = W-min P implies S-min P = SW-corner P
proof
A1: (S-min P)`2 = S-bound P by EUCLID:52;
assume S-min P = W-min P;
hence thesis by A1,EUCLID:52;
end;
theorem
proj2. |[r,s]| = s & proj1. |[r,s]| = r
proof
thus proj2. |[r,s]| = |[r,s]|`2 by Def6
.= s by EUCLID:52;
thus proj1. |[r,s]| = |[r,s]|`1 by Def5
.= r by EUCLID:52;
end;
:: Moved from JORDAN1E, AK, 23.02.2006
theorem
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 by Th17;
theorem
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 by Th17;
theorem
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 by Th16;
theorem
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 by Th16;