:: Properties of Connected Subsets of the Real Line
:: by Artur Korni{\l}owicz
::
:: Received February 22, 2005
:: Copyright (c) 2005-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, XBOOLE_0, SUBSET_1, MEMBERED, PRE_TOPC, METRIC_1,
STRUCT_0, XXREAL_2, RCOMP_1, TARSKI, ORDINAL2, SEQ_4, TOPMETR, XXREAL_1,
RELAT_2, CARD_1, ARYTM_3, XXREAL_0, REAL_1, ARYTM_1, LIMFUNC1, ZFMISC_1,
TOPS_1, RELAT_1, SETFAM_1, FINSET_1, ORDERS_1, WELLORD1, FINSEQ_1,
PARTFUN1, WELLORD2, FUNCT_1, NAT_1, RCOMP_3, MEASURE5, FUNCT_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, RELAT_1, SETFAM_1, FUNCT_1,
RELSET_1, PARTFUN1, FINSET_1, WELLORD1, ORDERS_1, WELLORD2, RELAT_2,
CARD_1, MEMBERED, NUMBERS, XCMPLX_0, XXREAL_0, MEASURE6, XREAL_0, NAT_1,
NAT_D, LIMFUNC1, XXREAL_1, XXREAL_2, SEQM_3, FINSEQ_1, VALUED_0,
VALUED_1, FUNCT_2, SEQ_4, RCOMP_1, STRUCT_0, PRE_TOPC, TOPS_1, METRIC_1,
TOPS_2, COMPTS_1, CONNSP_1, TOPMETR, TOPALG_2, TOPREALB;
constructors WELLORD1, WELLORD2, ORDERS_1, PROB_1, LIMFUNC1, BINARITH, TOPS_1,
CONNSP_1, COMPTS_1, MEASURE6, TOPREALB, BORSUK_6, NAT_D, SEQ_4, FUNCT_2,
BINOP_1;
registrations SUBSET_1, RELAT_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
MEMBERED, FINSEQ_1, RCOMP_1, FCONT_3, STRUCT_0, PRE_TOPC, TOPS_1,
METRIC_1, TOPMETR, MEASURE6, BORSUK_2, SPRECT_1, TOPREAL6, TOPALG_2,
TOPREALB, FINSET_1, VALUED_0, XXREAL_2, CARD_1, XXREAL_1, SEQ_4,
WELLORD2, RELSET_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions FUNCT_1, TOPS_2, RELAT_2, ORDERS_1, TARSKI, XBOOLE_0, SEQM_3,
CONNSP_1, STRUCT_0, SETFAM_1, TOPMETR, XXREAL_2;
equalities XBOOLE_0, SUBSET_1, WELLORD1, STRUCT_0, LIMFUNC1, PROB_1, ORDINAL1;
expansions FUNCT_1, TOPS_2, RELAT_2, ORDERS_1, TARSKI, XBOOLE_0, SEQM_3,
TOPALG_2, SUBSET_1, XXREAL_2, FUNCT_2;
theorems PRE_TOPC, XREAL_0, FUNCT_2, INT_1, FUNCT_1, TOPMETR, RELAT_1, TARSKI,
ZFMISC_1, JORDAN5A, FINSEQ_1, XBOOLE_1, COMPTS_1, SETFAM_1, XBOOLE_0,
FINSEQ_3, NAT_1, RCOMP_1, FINSEQ_5, HEINE, TOPS_1, CONNSP_1, TOPREALA,
TOPREALB, ORDINAL1, ORDERS_1, CARD_2, MEMBERED, SEQ_4, FINSEQ_4,
TOPREAL6, TREAL_1, BORSUK_5, TOPS_3, TEX_1, XREAL_1, WELLORD2, XXREAL_0,
XXREAL_1, PARTFUN1, XXREAL_2, MEASURE6, SUBSET_1;
schemes NAT_1, RELSET_1, FINSET_1, FRAENKEL, FINSEQ_1, RECDEF_1;
begin :: Preliminaries
registration
let X be non empty set;
cluster [#]X -> non empty;
coherence;
end;
registration
cluster -> real-membered for SubSpace of RealSpace;
coherence
proof
let T be SubSpace of RealSpace;
the carrier of T is Subset of RealSpace by TOPMETR:def 1;
hence the carrier of T is real-membered;
end;
end;
theorem Th1:
for X being non empty bounded_below real-membered set, Y being
closed Subset of REAL st X c= Y holds lower_bound X in Y
proof
let X be non empty bounded_below real-membered set;
let Y be closed Subset of REAL;
assume
A1: X c= Y;
reconsider X as non empty bounded_below Subset of REAL by MEMBERED:3;
A2: lower_bound X = lower_bound Cl X & lower_bound Cl X in Cl X by RCOMP_1:13
,TOPREAL6:68;
Cl X c= Y by A1,MEASURE6:57;
hence thesis by A2;
end;
theorem Th2:
for X being non empty bounded_above real-membered set, Y being
closed Subset of REAL st X c= Y holds upper_bound X in Y
proof
let X be non empty bounded_above real-membered set;
let Y be closed Subset of REAL;
assume
A1: X c= Y;
reconsider X as non empty bounded_above Subset of REAL by MEMBERED:3;
A2: upper_bound X = upper_bound Cl X & upper_bound Cl X in Cl X by RCOMP_1:12
,TOPREAL6:69;
Cl X c= Y by A1,MEASURE6:57;
hence thesis by A2;
end;
theorem Th3:
for X, Y being Subset of REAL holds Cl(X \/ Y) = Cl X \/ Cl Y
proof
let X, Y be Subset of REAL;
reconsider A = X, B = Y as Subset of R^1 by TOPMETR:17;
thus Cl(X \/ Y) = Cl(A \/ B) by JORDAN5A:24
.= Cl A \/ Cl B by PRE_TOPC:20
.= Cl X \/ Cl B by JORDAN5A:24
.= Cl X \/ Cl Y by JORDAN5A:24;
end;
begin :: Intervals
reserve a, b, r, s for Real;
registration
let r be Real, s be ExtReal;
cluster [.r,s.[ -> bounded_below;
coherence
proof
take r;
let x be ExtReal;
thus thesis by XXREAL_1:3;
end;
cluster ].s,r.] -> bounded_above;
coherence
proof
take r;
let x be ExtReal;
thus thesis by XXREAL_1:2;
end;
end;
registration
let r, s;
cluster [.r,s.[ -> real-bounded;
coherence
proof
[.r,s.[ is bounded_above
proof
take s;
let x be ExtReal;
thus thesis by XXREAL_1:3;
end;
hence thesis;
end;
cluster ].r,s.] -> real-bounded;
coherence
proof
].r,s.] is bounded_below
proof
take r;
let x be ExtReal;
thus thesis by XXREAL_1:2;
end;
hence thesis;
end;
cluster ].r,s.[ -> real-bounded;
coherence
proof
A1: ].r,s.[ is bounded_above
proof
take s;
let x be ExtReal;
thus thesis by XXREAL_1:4;
end;
].r,s.[ is bounded_below
proof
take r;
let x be ExtReal;
thus thesis by XXREAL_1:4;
end;
hence thesis by A1;
end;
end;
registration
cluster open real-bounded interval non empty for Subset of REAL;
existence
proof
take ].0,1.[;
thus thesis;
end;
end;
theorem Th4:
r < s implies lower_bound [.r,s.[ = r
proof
set X = [.r,s.[;
assume
A1: r < s;
A2: for a st a in X holds r <= a by XXREAL_1:3;
A3: (r+s)/2 < s by A1,XREAL_1:226;
A4: r < (r+s)/2 by A1,XREAL_1:226;
A5: for b st 0 < b ex a st a in X & a < r+b
proof
let b such that
A6: 0 < b and
A7: for a st a in X holds a >= r+b;
per cases;
suppose
r + b > s;
then
A8: (r+s)/2 < r+b by A3,XXREAL_0:2;
(r+s)/2 in X by A4,A3,XXREAL_1:3;
hence thesis by A7,A8;
end;
suppose
A9: r + b <= s;
A10: r < r + b by A6,XREAL_1:29;
then (r+(r+b))/2 < r+b by XREAL_1:226;
then
A11: (r+(r+b))/2 < s by A9,XXREAL_0:2;
r < (r+(r+b))/2 by A10,XREAL_1:226;
then (r+(r+b))/2 in X by A11,XXREAL_1:3;
hence thesis by A7,A10,XREAL_1:226;
end;
end;
X is non empty by A1,XXREAL_1:3;
hence thesis by A2,A5,SEQ_4:def 2;
end;
theorem Th5:
r < s implies upper_bound [.r,s.[ = s
proof
set X = [.r,s.[;
assume
A1: r < s;
A2: for a st a in X holds a <= s by XXREAL_1:3;
A3: r < (r+s)/2 by A1,XREAL_1:226;
A4: (r+s)/2 < s by A1,XREAL_1:226;
A5: for b st 0 < b ex a st a in X & s-b < a
proof
let b such that
A6: 0 < b and
A7: for a st a in X holds a <= s-b;
per cases;
suppose
s - b <= r;
then
A8: (r+s)/2 > s-b by A3,XXREAL_0:2;
(r+s)/2 in X by A3,A4,XXREAL_1:3;
hence thesis by A7,A8;
end;
suppose
A9: s - b > r;
A10: s - b < s - 0 by A6,XREAL_1:15;
then s-b < (s+(s-b))/2 by XREAL_1:226;
then
A11: r < (s+(s-b))/2 by A9,XXREAL_0:2;
(s+(s-b))/2 < s by A10,XREAL_1:226;
then (s+(s-b))/2 in X by A11,XXREAL_1:3;
hence thesis by A7,A10,XREAL_1:226;
end;
end;
X is non empty by A1,XXREAL_1:3;
hence thesis by A2,A5,SEQ_4:def 1;
end;
theorem Th6:
r < s implies lower_bound ].r,s.] = r
proof
set X = ].r,s.];
assume
A1: r < s;
A2: for a st a in X holds r <= a by XXREAL_1:2;
A3: (r+s)/2 < s by A1,XREAL_1:226;
A4: r < (r+s)/2 by A1,XREAL_1:226;
A5: for b st 0 < b ex a st a in X & a < r+b
proof
let b such that
A6: 0 < b and
A7: for a st a in X holds a >= r+b;
per cases;
suppose
r + b > s;
then
A8: (r+s)/2 < r+b by A3,XXREAL_0:2;
(r+s)/2 in X by A4,A3,XXREAL_1:2;
hence thesis by A7,A8;
end;
suppose
A9: r + b <= s;
A10: r < r + b by A6,XREAL_1:29;
then (r+(r+b))/2 < r+b by XREAL_1:226;
then
A11: (r+(r+b))/2 < s by A9,XXREAL_0:2;
r < (r+(r+b))/2 by A10,XREAL_1:226;
then (r+(r+b))/2 in X by A11,XXREAL_1:2;
hence thesis by A7,A10,XREAL_1:226;
end;
end;
X is non empty by A1,XXREAL_1:2;
hence thesis by A2,A5,SEQ_4:def 2;
end;
theorem Th7:
r < s implies upper_bound ].r,s.] = s
proof
set X = ].r,s.];
assume
A1: r < s;
A2: for a st a in X holds a <= s by XXREAL_1:2;
A3: r < (r+s)/2 by A1,XREAL_1:226;
A4: (r+s)/2 < s by A1,XREAL_1:226;
A5: for b st 0 < b ex a st a in X & s-b < a
proof
let b such that
A6: 0 < b and
A7: for a st a in X holds a <= s-b;
per cases;
suppose
s - b <= r;
then
A8: (r+s)/2 > s-b by A3,XXREAL_0:2;
(r+s)/2 in X by A3,A4,XXREAL_1:2;
hence thesis by A7,A8;
end;
suppose
A9: s - b > r;
A10: s - b < s - 0 by A6,XREAL_1:15;
then s-b < (s+(s-b))/2 by XREAL_1:226;
then
A11: r < (s+(s-b))/2 by A9,XXREAL_0:2;
(s+(s-b))/2 < s by A10,XREAL_1:226;
then (s+(s-b))/2 in X by A11,XXREAL_1:2;
hence thesis by A7,A10,XREAL_1:226;
end;
end;
X is non empty by A1,XXREAL_1:2;
hence thesis by A2,A5,SEQ_4:def 1;
end;
begin :: Halflines
theorem Th8:
a <= b implies [.a,b.] /\ (left_closed_halfline(a) \/
right_closed_halfline(b)) = {a,b}
proof
set A = left_closed_halfline(a);
set B = right_closed_halfline(b);
assume a <= b;
then
A1: a in [.a,b.] & b in [.a,b.] by XXREAL_1:1;
thus [.a,b.] /\ (A \/ B) c= {a,b}
proof
let x be object;
assume
A2: x in [.a,b.] /\ (A \/ B);
then reconsider x as Real;
x in A \/ B by A2,XBOOLE_0:def 4;
then x in A or x in B by XBOOLE_0:def 3;
then
A3: x <= a or x >= b by XXREAL_1:234,236;
x in [.a,b.] by A2,XBOOLE_0:def 4;
then a <= x & x <= b by XXREAL_1:1;
then x = a or x = b by A3,XXREAL_0:1;
hence thesis by TARSKI:def 2;
end;
let x be object;
a in A by XXREAL_1:234;
then
A4: a in A \/ B by XBOOLE_0:def 3;
b in B by XXREAL_1:236;
then
A5: b in A \/ B by XBOOLE_0:def 3;
assume x in {a,b};
then x = a or x = b by TARSKI:def 2;
hence thesis by A1,A4,A5,XBOOLE_0:def 4;
end;
Lm1: now
let a;
assume left_open_halfline(a) is bounded_below;
then consider b such that
A1: b is LowerBound of left_open_halfline(a);
A2: for r st r in left_open_halfline(a) holds b <= r by A1,XXREAL_2:def 2;
A3: a-1 < a-0 by XREAL_1:15;
then a-1 in left_open_halfline(a) by XXREAL_1:233;
then b-1 < a-1-0 by A2,XREAL_1:15;
then b-1 < a by A3,XXREAL_0:2;
then b-1 in left_open_halfline(a) by XXREAL_1:233;
then b-0 <= b-1 by A1,XXREAL_2:def 2;
hence contradiction by XREAL_1:15;
end;
Lm2: now
let a;
assume right_open_halfline(a) is bounded_above;
then consider b such that
A1: b is UpperBound of right_open_halfline(a);
A2: a+0 < a+1 by XREAL_1:6;
then a+1 in right_open_halfline(a) by XXREAL_1:235;
then a+1 <= b by A1,XXREAL_2:def 1;
then a+1+0 <= b+1 by XREAL_1:7;
then a < b+1 by A2,XXREAL_0:2;
then b+1 in right_open_halfline(a) by XXREAL_1:235;
then b+1 <= b+0 by A1,XXREAL_2:def 1;
hence contradiction by XREAL_1:6;
end;
registration
let a;
cluster left_closed_halfline(a) -> non bounded_below bounded_above interval;
coherence
proof
set A = left_closed_halfline(a);
left_open_halfline a is not bounded_below by Lm1;
hence A is non bounded_below by XXREAL_1:21,XXREAL_2:44;
thus A is bounded_above;
let r,s be ExtReal;
assume
A1: r in A & s in A;
then reconsider rr=r, ss=s as Real;
A2: s <= a by A1,XXREAL_1:234;
let x be object;
assume
A3: x in [.r,s.];
then x in [.rr,ss.];
then reconsider x as Real;
x <= s by A3,XXREAL_1:1;
then x <= a by A2,XXREAL_0:2;
hence thesis by XXREAL_1:234;
end;
cluster left_open_halfline(a) -> non bounded_below bounded_above interval;
coherence
proof
set A = left_open_halfline(a);
thus A is non bounded_below by Lm1;
thus A is bounded_above
proof
take a;
let x be ExtReal;
thus thesis by XXREAL_1:233;
end;
let r, s be ExtReal;
assume
A4: r in A;
assume
A5: s in A;
then
A6: s < a by XXREAL_1:233;
reconsider rr=r, ss=s as Real by A4,A5;
let x be object;
assume
A7: x in [.r,s.];
then x in [.rr,ss.];
then reconsider x as Real;
x <= s by A7,XXREAL_1:1;
then x < a by A6,XXREAL_0:2;
hence thesis by XXREAL_1:233;
end;
cluster right_closed_halfline(a) -> bounded_below non bounded_above interval;
coherence
proof
set A = right_closed_halfline(a);
thus A is bounded_below;
right_open_halfline a is not bounded_above by Lm2;
hence A is non bounded_above by XXREAL_1:22,XXREAL_2:43;
let r, s be ExtReal;
assume
A8: r in A;
then
A9: a <= r by XXREAL_1:236;
assume s in A;
then reconsider rr=r, ss=s as Real by A8;
let x be object;
assume
A10: x in [.r,s.];
then x in [.rr,ss.];
then reconsider x as Real;
r <= x by A10,XXREAL_1:1;
then a <= x by A9,XXREAL_0:2;
hence thesis by XXREAL_1:236;
end;
cluster right_open_halfline(a) -> bounded_below non bounded_above interval;
coherence
proof
set A = right_open_halfline(a);
thus A is bounded_below
proof
take a;
let x be ExtReal;
thus thesis by XXREAL_1:235;
end;
thus A is non bounded_above by Lm2;
let r, s be ExtReal;
assume
A11: r in A;
then
A12: a < r by XXREAL_1:235;
assume s in A;
then reconsider rr=r, ss=s as Real by A11;
let x be object;
assume
A13: x in [.r,s.];
then x in [.rr,ss.];
then reconsider x as Real;
r <= x by A13,XXREAL_1:1;
then a < x by A12,XXREAL_0:2;
hence thesis by XXREAL_1:235;
end;
end;
theorem Th9:
upper_bound left_closed_halfline(a) = a
proof
set X = left_closed_halfline(a);
A1: for s st 0 < s ex r st r in X & a-s < r
proof
let s;
assume 0 < s;
then
A2: a-s < a-0 by XREAL_1:15;
take a;
thus a in X by XXREAL_1:234;
thus thesis by A2;
end;
for r st r in X holds r <= a by XXREAL_1:234;
hence thesis by A1,SEQ_4:def 1;
end;
theorem Th10:
upper_bound left_open_halfline(a) = a
proof
set X = left_open_halfline(a);
A1: for s st 0 < s ex r st r in X & a-s < r
proof
let s;
assume 0 < s;
then
A2: a-s < a-0 by XREAL_1:15;
take (a-s+a)/2;
(a-s+a)/2 < a by A2,XREAL_1:226;
hence thesis by A2,XREAL_1:226,XXREAL_1:233;
end;
for r st r in X holds r <= a by XXREAL_1:233;
hence thesis by A1,SEQ_4:def 1;
end;
theorem Th11:
lower_bound right_closed_halfline(a) = a
proof
set X = right_closed_halfline(a);
A1: for s st 0 < s ex r st r in X & r < a+s
proof
let s;
assume 0 < s;
then
A2: a+0 < a+s by XREAL_1:6;
take a;
thus a in X by XXREAL_1:236;
thus thesis by A2;
end;
for r st r in X holds a <= r by XXREAL_1:236;
hence thesis by A1,SEQ_4:def 2;
end;
theorem Th12:
lower_bound right_open_halfline(a) = a
proof
set X = right_open_halfline(a);
A1: for s st 0 < s ex r st r in X & r < a+s
proof
let s;
assume 0 < s;
then
A2: a+0 < a+s by XREAL_1:6;
take (a+a+s)/2;
a < (a+(a+s))/2 by A2,XREAL_1:226;
hence thesis by A2,XREAL_1:226,XXREAL_1:235;
end;
for r st r in X holds a <= r by XXREAL_1:235;
hence thesis by A1,SEQ_4:def 2;
end;
begin :: Connectedness
registration
cluster [#]REAL -> interval non bounded_below non bounded_above;
coherence;
end;
theorem Th13:
for X being real-bounded interval Subset of REAL st lower_bound X in
X & upper_bound X in X holds X = [.lower_bound X,upper_bound X.]
proof
let X be real-bounded interval Subset of REAL such that
A1: lower_bound X in X & upper_bound X in X;
reconsider X1=X as non empty real-bounded interval Subset of REAL by A1;
X1 c= [.lower_bound X1,upper_bound X1.] by XXREAL_2:69;
hence X c= [.lower_bound X,upper_bound X.];
thus thesis by A1,XXREAL_2:def 12;
end;
theorem Th14:
for X being real-bounded Subset of REAL st not lower_bound X in X
holds X c= ].lower_bound X,upper_bound X.]
proof
let X be real-bounded Subset of REAL such that
A1: not lower_bound X in X;
let x be object;
assume
A2: x in X;
then reconsider x as Real;
lower_bound X <= x by A2,SEQ_4:def 2;
then
A3: lower_bound X < x by A1,A2,XXREAL_0:1;
x <= upper_bound X by A2,SEQ_4:def 1;
hence thesis by A3,XXREAL_1:2;
end;
theorem Th15:
for X being real-bounded interval Subset of REAL st not lower_bound
X in X & upper_bound X in X holds X = ].lower_bound X,upper_bound X.]
proof
let X be real-bounded interval Subset of REAL such that
A1: not lower_bound X in X and
A2: upper_bound X in X;
thus X c= ].lower_bound X,upper_bound X.] by A1,Th14;
let x be object;
assume
A3: x in ].lower_bound X,upper_bound X.];
then reconsider x as Real;
lower_bound X < x by A3,XXREAL_1:2;
then lower_bound X - lower_bound X < x - lower_bound X by XREAL_1:14;
then consider r such that
A4: r in X and
A5: r < lower_bound X + (x - lower_bound X) by A2,SEQ_4:def 2;
x <= upper_bound X by A3,XXREAL_1:2;
then
A6: x in [.r,upper_bound X.] by A5,XXREAL_1:1;
[.r,upper_bound X.] c= X by A2,A4,XXREAL_2:def 12;
hence thesis by A6;
end;
theorem Th16:
for X being real-bounded Subset of REAL st not upper_bound X in X
holds X c= [.lower_bound X,upper_bound X.[
proof
let X be real-bounded Subset of REAL such that
A1: not upper_bound X in X;
let x be object;
assume
A2: x in X;
then reconsider x as Real;
x <= upper_bound X by A2,SEQ_4:def 1;
then
A3: x < upper_bound X by A1,A2,XXREAL_0:1;
lower_bound X <= x by A2,SEQ_4:def 2;
hence thesis by A3,XXREAL_1:3;
end;
theorem Th17:
for X being real-bounded interval Subset of REAL st lower_bound X in
X & not upper_bound X in X holds X = [.lower_bound X,upper_bound X.[
proof
let X be real-bounded interval Subset of REAL such that
A1: lower_bound X in X and
A2: not upper_bound X in X;
thus X c= [.lower_bound X,upper_bound X.[ by A2,Th16;
let x be object;
assume
A3: x in [.lower_bound X,upper_bound X.[;
then reconsider x as Real;
x < upper_bound X by A3,XXREAL_1:3;
then x - x < upper_bound X - x by XREAL_1:14;
then consider r such that
A4: r in X and
A5: upper_bound X - (upper_bound X - x) < r by A1,SEQ_4:def 1;
lower_bound X <= x by A3,XXREAL_1:3;
then
A6: x in [.lower_bound X,r.] by A5,XXREAL_1:1;
[.lower_bound X,r.] c= X by A1,A4,XXREAL_2:def 12;
hence thesis by A6;
end;
theorem Th18:
for X being real-bounded Subset of REAL st not lower_bound X in X &
not upper_bound X in X holds X c= ].lower_bound X,upper_bound X.[
proof
let X be real-bounded Subset of REAL such that
A1: not lower_bound X in X and
A2: not upper_bound X in X;
let x be object;
assume
A3: x in X;
then reconsider x as Real;
x <= upper_bound X by A3,SEQ_4:def 1;
then
A4: x < upper_bound X by A2,A3,XXREAL_0:1;
lower_bound X <= x by A3,SEQ_4:def 2;
then lower_bound X < x by A1,A3,XXREAL_0:1;
hence thesis by A4,XXREAL_1:4;
end;
theorem Th19:
for X being non empty real-bounded interval Subset of REAL st not
lower_bound X in X & not upper_bound X in X holds X = ].lower_bound X,
upper_bound X.[
proof
let X be non empty real-bounded interval Subset of REAL;
assume ( not lower_bound X in X)& not upper_bound X in X;
hence X c= ].lower_bound X,upper_bound X.[ by Th18;
let x be object;
assume
A1: x in ].lower_bound X,upper_bound X.[;
then reconsider x as Real;
lower_bound X < x by A1,XXREAL_1:4;
then lower_bound X - lower_bound X < x - lower_bound X by XREAL_1:14;
then consider s such that
A2: s in X & s < lower_bound X + (x - lower_bound X) by SEQ_4:def 2;
x < upper_bound X by A1,XXREAL_1:4;
then x - x < upper_bound X - x by XREAL_1:14;
then consider r such that
A3: r in X & upper_bound X - (upper_bound X - x) < r by SEQ_4:def 1;
[.s,r.] c= X & x in [.s,r.] by A2,A3,XXREAL_1:1,XXREAL_2:def 12;
hence thesis;
end;
theorem Th20:
for X being Subset of REAL st X is bounded_above holds X c=
left_closed_halfline(upper_bound X)
proof
let X be Subset of REAL such that
A1: X is bounded_above;
let x be object;
assume
A2: x in X;
then reconsider x as Real;
x <= upper_bound X by A1,A2,SEQ_4:def 1;
hence thesis by XXREAL_1:234;
end;
theorem Th21:
for X being interval Subset of REAL st X is not bounded_below &
X is bounded_above & upper_bound X in X holds X = left_closed_halfline(
upper_bound X)
proof
let X be interval Subset of REAL such that
A1: X is not bounded_below and
A2: X is bounded_above and
A3: upper_bound X in X;
thus X c= left_closed_halfline(upper_bound X) by A2,Th20;
let x be object;
assume
A4: x in left_closed_halfline(upper_bound X);
then reconsider x as Real;
x is not LowerBound of X by A1;
then consider r being ExtReal such that
A5: r in X and
A6: x > r by XXREAL_2:def 2;
reconsider r as Real by A5;
x <= upper_bound X by A4,XXREAL_1:234;
then
A7: x in [.r,upper_bound X.] by A6,XXREAL_1:1;
[.r,upper_bound X.] c= X by A3,A5,XXREAL_2:def 12;
hence thesis by A7;
end;
theorem Th22:
for X being Subset of REAL st X is bounded_above & not
upper_bound X in X holds X c= left_open_halfline(upper_bound X)
proof
let X be Subset of REAL such that
A1: X is bounded_above and
A2: not upper_bound X in X;
let x be object;
assume
A3: x in X;
then reconsider x as Real;
x <= upper_bound X by A1,A3,SEQ_4:def 1;
then x < upper_bound X by A2,A3,XXREAL_0:1;
hence thesis by XXREAL_1:233;
end;
theorem Th23:
for X being non empty interval Subset of REAL st X is not
bounded_below & X is bounded_above & not upper_bound X in X holds X =
left_open_halfline(upper_bound X)
proof
let X be non empty interval Subset of REAL such that
A1: X is not bounded_below and
A2: X is bounded_above and
A3: not upper_bound X in X;
thus X c= left_open_halfline(upper_bound X) by A2,A3,Th22;
let x be object;
assume
A4: x in left_open_halfline(upper_bound X);
then reconsider x as Real;
x is not LowerBound of X by A1;
then consider r being ExtReal such that
A5: r in X & x > r by XXREAL_2:def 2;
reconsider r as Real by A5;
x < upper_bound X by A4,XXREAL_1:233;
then x - x < upper_bound X - x by XREAL_1:14;
then consider s such that
A6: s in X & upper_bound X - (upper_bound X - x) < s by A2,SEQ_4:def 1;
[.r,s.] c= X & x in [.r,s.] by A5,A6,XXREAL_1:1,XXREAL_2:def 12;
hence thesis;
end;
theorem Th24:
for X being Subset of REAL st X is bounded_below holds X c=
right_closed_halfline(lower_bound X)
proof
let X be Subset of REAL such that
A1: X is bounded_below;
let x be object;
assume
A2: x in X;
then reconsider x as Real;
lower_bound X <= x by A1,A2,SEQ_4:def 2;
hence thesis by XXREAL_1:236;
end;
theorem Th25:
for X being interval Subset of REAL st X is bounded_below & X
is not bounded_above & lower_bound X in X holds X = right_closed_halfline(
lower_bound X)
proof
let X be interval Subset of REAL such that
A1: X is bounded_below and
A2: X is not bounded_above and
A3: lower_bound X in X;
thus X c= right_closed_halfline(lower_bound X) by A1,Th24;
let x be object;
assume
A4: x in right_closed_halfline(lower_bound X);
then reconsider x as Real;
x is not UpperBound of X by A2;
then consider r being ExtReal such that
A5: r in X and
A6: x < r by XXREAL_2:def 1;
reconsider r as Real by A5;
lower_bound X <= x by A4,XXREAL_1:236;
then
A7: x in [.lower_bound X,r.] by A6,XXREAL_1:1;
[.lower_bound X,r.] c= X by A3,A5,XXREAL_2:def 12;
hence thesis by A7;
end;
theorem Th26:
for X being Subset of REAL st X is bounded_below & not
lower_bound X in X holds X c= right_open_halfline(lower_bound X)
proof
let X be Subset of REAL such that
A1: X is bounded_below and
A2: not lower_bound X in X;
let x be object;
assume
A3: x in X;
then reconsider x as Real;
lower_bound X <= x by A1,A3,SEQ_4:def 2;
then lower_bound X < x by A2,A3,XXREAL_0:1;
hence thesis by XXREAL_1:235;
end;
theorem Th27:
for X being non empty interval Subset of REAL st X is
bounded_below & X is not bounded_above & not lower_bound X in X holds X =
right_open_halfline(lower_bound X)
proof
let X be non empty interval Subset of REAL such that
A1: X is bounded_below and
A2: X is not bounded_above and
A3: not lower_bound X in X;
thus X c= right_open_halfline(lower_bound X) by A1,A3,Th26;
let x be object;
assume
A4: x in right_open_halfline(lower_bound X);
then reconsider x as Real;
x is not UpperBound of X by A2;
then consider r being ExtReal such that
A5: r in X & x < r by XXREAL_2:def 1;
lower_bound X < x by A4,XXREAL_1:235;
then lower_bound X - lower_bound X < x - lower_bound X by XREAL_1:14;
then consider s such that
A6: s in X & s < lower_bound X + (x - lower_bound X) by A1,SEQ_4:def 2;
reconsider r as Real by A5;
[.s,r.] c= X & x in [.s,r.] by A5,A6,XXREAL_1:1,XXREAL_2:def 12;
hence thesis;
end;
theorem Th28:
for X being interval Subset of REAL st X is not bounded_above &
X is not bounded_below holds X = REAL
proof
let X be interval Subset of REAL;
assume that
A1: X is not bounded_above and
A2: X is not bounded_below;
thus X c= REAL;
let x be object;
assume x in REAL;
then reconsider x as Real;
x is not UpperBound of X by A1;
then consider r being ExtReal such that
A3: r in X & r > x by XXREAL_2:def 1;
reconsider r as Real by A3;
x is not LowerBound of X by A2;
then consider s being ExtReal such that
A4: s in X & s < x by XXREAL_2:def 2;
reconsider s as Real by A4;
[.s,r.] c= X & x in [.s,r.] by A3,A4,XXREAL_1:1,XXREAL_2:def 12;
hence thesis;
end;
theorem Th29:
for X being interval Subset of REAL holds X is empty or X =
REAL or (ex a st X = left_closed_halfline(a)) or (ex a st X =
left_open_halfline(a)) or (ex a st X = right_closed_halfline(a)) or (ex a st X
= right_open_halfline(a)) or (ex a, b st a <= b & X = [.a,b.]) or (ex a, b st a
< b & X = [.a,b.[) or (ex a, b st a < b & X = ].a,b.]) or ex a, b st a < b & X
= ].a,b.[
proof
let X be interval Subset of REAL;
assume X is non empty;
then reconsider X as non empty interval Subset of REAL;
per cases;
suppose
X is real-bounded;
then reconsider X as non empty real-bounded interval Subset of REAL;
per cases;
suppose
X is trivial;
then consider x being object such that
A1: X = {x} by ZFMISC_1:131;
x in X by A1,TARSKI:def 1;
then reconsider x as Real;
X = [.x,x.] by A1,XXREAL_1:17;
hence thesis;
end;
suppose
X is non trivial;
then ex p, q being object st p in X & q in X & p <> q;
then
A2: lower_bound X < upper_bound X by SEQ_4:12;
per cases;
suppose
upper_bound X in X & lower_bound X in X;
then X = [.lower_bound X,upper_bound X.] by Th13;
hence thesis by A2;
end;
suppose
upper_bound X in X & not lower_bound X in X;
then X = ].lower_bound X,upper_bound X.] by Th15;
hence thesis by A2;
end;
suppose
not upper_bound X in X & lower_bound X in X;
then X = [.lower_bound X,upper_bound X.[ by Th17;
hence thesis by A2;
end;
suppose
not upper_bound X in X & not lower_bound X in X;
then X = ].lower_bound X,upper_bound X.[ by Th19;
hence thesis by A2;
end;
end;
end;
suppose
A3: X is not real-bounded;
per cases by A3;
suppose
A4: X is not bounded_below & X is bounded_above;
per cases;
suppose
upper_bound X in X;
then X = left_closed_halfline(upper_bound X) by A4,Th21;
hence thesis;
end;
suppose
not upper_bound X in X;
then X = left_open_halfline(upper_bound X) by A4,Th23;
hence thesis;
end;
end;
suppose
A5: X is not bounded_above & X is bounded_below;
per cases;
suppose
lower_bound X in X;
then X = right_closed_halfline(lower_bound X) by A5,Th25;
hence thesis;
end;
suppose
not lower_bound X in X;
then X = right_open_halfline(lower_bound X) by A5,Th27;
hence thesis;
end;
end;
suppose
X is not bounded_above & X is not bounded_below;
hence thesis by Th28;
end;
end;
end;
theorem Th30:
for X being non empty interval Subset of REAL st not r in X
holds r <= lower_bound X or upper_bound X <= r
proof
let X be non empty interval Subset of REAL such that
A1: not r in X;
per cases by Th29;
suppose
X = REAL;
hence thesis by A1,XREAL_0:def 1;
end;
suppose
ex a st X = left_closed_halfline(a);
then consider a such that
A2: X = left_closed_halfline(a);
upper_bound X = a by A2,Th9;
hence thesis by A1,A2,XXREAL_1:234;
end;
suppose
ex a st X = left_open_halfline(a);
then consider a such that
A3: X = left_open_halfline(a);
upper_bound X = a by A3,Th10;
hence thesis by A1,A3,XXREAL_1:233;
end;
suppose
ex a st X = right_closed_halfline(a);
then consider a such that
A4: X = right_closed_halfline(a);
lower_bound X = a by A4,Th11;
hence thesis by A1,A4,XXREAL_1:236;
end;
suppose
ex a st X = right_open_halfline(a);
then consider a such that
A5: X = right_open_halfline(a);
lower_bound X = a by A5,Th12;
hence thesis by A1,A5,XXREAL_1:235;
end;
suppose
ex a, b st a <= b & X = [.a,b.];
then consider a, b such that
A6: a <= b and
A7: X = [.a,b.];
lower_bound X = a & upper_bound X = b by A6,A7,JORDAN5A:19;
hence thesis by A1,A7,XXREAL_1:1;
end;
suppose
ex a, b st a < b & X = [.a,b.[;
then consider a, b such that
A8: a < b and
A9: X = [.a,b.[;
lower_bound X = a & upper_bound X = b by A8,A9,Th4,Th5;
hence thesis by A1,A9,XXREAL_1:3;
end;
suppose
ex a, b st a < b & X = ].a,b.];
then consider a, b such that
A10: a < b and
A11: X = ].a,b.];
lower_bound X = a & upper_bound X = b by A10,A11,Th6,Th7;
hence thesis by A1,A11,XXREAL_1:2;
end;
suppose
ex a, b st a < b & X = ].a,b.[;
then consider a, b such that
A12: a < b and
A13: X = ].a,b.[;
lower_bound X = a & upper_bound X = b by A12,A13,TOPREAL6:17;
hence thesis by A1,A13,XXREAL_1:4;
end;
end;
theorem Th31:
for X, Y being non empty real-bounded interval Subset of REAL st
lower_bound X <= lower_bound Y & upper_bound Y <= upper_bound X & (lower_bound
X = lower_bound Y & lower_bound Y in Y implies lower_bound X in X) & (
upper_bound X = upper_bound Y & upper_bound Y in Y implies upper_bound X in X)
holds Y c= X
proof
let X, Y be non empty real-bounded interval Subset of REAL such that
A1: lower_bound X <= lower_bound Y and
A2: upper_bound Y <= upper_bound X and
A3: lower_bound X = lower_bound Y & lower_bound Y in Y implies
lower_bound X in X and
A4: upper_bound X = upper_bound Y & upper_bound Y in Y implies
upper_bound X in X;
let x be object;
assume
A5: x in Y;
then reconsider x as Real;
A6: Y c= [.lower_bound Y,upper_bound Y.] by XXREAL_2:69;
then
A7: lower_bound Y <= x by A5,XXREAL_1:1;
then
A8: lower_bound X <= x by A1,XXREAL_0:2;
A9: x <= upper_bound Y by A5,A6,XXREAL_1:1;
then
A10: x <= upper_bound X by A2,XXREAL_0:2;
per cases by Th29;
suppose
X = [#]REAL;
hence thesis;
end;
suppose
(ex a st X = left_closed_halfline(a)) or (ex a st X =
left_open_halfline(a)) or (ex a st X = right_closed_halfline(a)) or ex a st X =
right_open_halfline(a);
hence thesis;
end;
suppose
ex a, b st a <= b & X = [.a,b.];
then consider a, b such that
A11: a <= b and
A12: X = [.a,b.];
lower_bound X = a & upper_bound X = b by A11,A12,JORDAN5A:19;
hence thesis by A8,A10,A12,XXREAL_1:1;
end;
suppose
ex a, b st a < b & X = [.a,b.[;
then consider a, b such that
A13: a < b and
A14: X = [.a,b.[;
A15: lower_bound X = a by A13,A14,Th4;
A16: upper_bound X = b by A13,A14,Th5;
per cases by Th29;
suppose
Y = [#]REAL;
hence thesis;
end;
suppose
(ex a st Y = left_closed_halfline(a)) or (ex a st Y =
left_open_halfline(a)) or (ex a st Y = right_closed_halfline(a)) or ex a st Y =
right_open_halfline(a);
hence thesis;
end;
suppose
ex a, b st a <= b & Y = [.a,b.];
then consider a1, b1 being Real such that
A17: a1 <= b1 & Y = [.a1,b1.];
A18: upper_bound Y = b1 by A17,JORDAN5A:19;
then b1 < b by A2,A4,A14,A16,A17,XXREAL_0:1,XXREAL_1:1,3;
then x < b by A9,A18,XXREAL_0:2;
hence thesis by A8,A14,A15,XXREAL_1:3;
end;
suppose
ex a, b st a < b & Y = [.a,b.[;
then consider a1, b1 being Real such that
A19: a1 < b1 & Y = [.a1,b1.[;
upper_bound Y = b1 & x < b1 by A5,A19,Th5,XXREAL_1:3;
then x < b by A2,A16,XXREAL_0:2;
hence thesis by A8,A14,A15,XXREAL_1:3;
end;
suppose
ex a, b st a < b & Y = ].a,b.];
then consider a1, b1 being Real such that
A20: a1 < b1 & Y = ].a1,b1.];
A21: upper_bound Y = b1 by A20,Th7;
then b1 < b by A2,A4,A14,A16,A20,XXREAL_0:1,XXREAL_1:2,3;
then x < b by A9,A21,XXREAL_0:2;
hence thesis by A8,A14,A15,XXREAL_1:3;
end;
suppose
ex a, b st a < b & Y = ].a,b.[;
then consider a1, b1 being Real such that
A22: a1 < b1 & Y = ].a1,b1.[;
upper_bound Y = b1 & x < b1 by A5,A22,TOPREAL6:17,XXREAL_1:4;
then x < b by A2,A16,XXREAL_0:2;
hence thesis by A8,A14,A15,XXREAL_1:3;
end;
end;
suppose
ex a, b st a < b & X = ].a,b.];
then consider a, b such that
A23: a < b and
A24: X = ].a,b.];
A25: lower_bound X = a by A23,A24,Th6;
A26: upper_bound X = b by A23,A24,Th7;
per cases by Th29;
suppose
Y = [#]REAL;
hence thesis;
end;
suppose
(ex a st Y = left_closed_halfline(a)) or (ex a st Y =
left_open_halfline(a)) or (ex a st Y = right_closed_halfline(a)) or ex a st Y =
right_open_halfline(a);
hence thesis;
end;
suppose
ex a, b st a <= b & Y = [.a,b.];
then consider a1, b1 being Real such that
A27: a1 <= b1 & Y = [.a1,b1.];
A28: lower_bound Y = a1 by A27,JORDAN5A:19;
then a < a1 by A1,A3,A24,A25,A27,XXREAL_0:1,XXREAL_1:1,2;
then a < x by A7,A28,XXREAL_0:2;
hence thesis by A10,A24,A26,XXREAL_1:2;
end;
suppose
ex a, b st a < b & Y = [.a,b.[;
then consider a1, b1 being Real such that
A29: a1 < b1 and
A30: Y = [.a1,b1.[;
lower_bound Y = a1 by A29,A30,Th4;
then
A31: a < a1 by A1,A3,A24,A25,A29,A30,XXREAL_0:1,XXREAL_1:2,3;
a1 <= x by A5,A30,XXREAL_1:3;
then a < x by A31,XXREAL_0:2;
hence thesis by A10,A24,A26,XXREAL_1:2;
end;
suppose
ex a, b st a < b & Y = ].a,b.];
then consider a1, b1 being Real such that
A32: a1 < b1 & Y = ].a1,b1.];
lower_bound Y = a1 & a1 < x by A5,A32,Th6,XXREAL_1:2;
then a < x by A1,A25,XXREAL_0:2;
hence thesis by A10,A24,A26,XXREAL_1:2;
end;
suppose
ex a, b st a < b & Y = ].a,b.[;
then consider a1, b1 being Real such that
A33: a1 < b1 & Y = ].a1,b1.[;
lower_bound Y = a1 & a1 < x by A5,A33,TOPREAL6:17,XXREAL_1:4;
then a < x by A1,A25,XXREAL_0:2;
hence thesis by A10,A24,A26,XXREAL_1:2;
end;
end;
suppose
ex a, b st a < b & X = ].a,b.[;
then consider a, b such that
A34: a < b and
A35: X = ].a,b.[;
A36: lower_bound X = a by A34,A35,TOPREAL6:17;
A37: upper_bound X = b by A34,A35,TOPREAL6:17;
per cases by Th29;
suppose
Y = [#]REAL;
hence thesis;
end;
suppose
(ex a st Y = left_closed_halfline(a)) or (ex a st Y =
left_open_halfline(a)) or (ex a st Y = right_closed_halfline(a)) or ex a st Y =
right_open_halfline(a);
hence thesis;
end;
suppose
ex a, b st a <= b & Y = [.a,b.];
then consider a1, b1 being Real such that
A38: a1 <= b1 and
A39: Y = [.a1,b1.];
upper_bound Y = b1 by A38,A39,JORDAN5A:19;
then
A40: b1 < b by A2,A4,A35,A37,A38,A39,XXREAL_0:1,XXREAL_1:1,4;
x <= b1 by A5,A39,XXREAL_1:1;
then
A41: x < b by A40,XXREAL_0:2;
A42: lower_bound Y = a1 by A38,A39,JORDAN5A:19;
then a < a1 by A1,A3,A35,A36,A38,A39,XXREAL_0:1,XXREAL_1:1,4;
then a < x by A7,A42,XXREAL_0:2;
hence thesis by A35,A41,XXREAL_1:4;
end;
suppose
ex a, b st a < b & Y = [.a,b.[;
then consider a1, b1 being Real such that
A43: a1 < b1 and
A44: Y = [.a1,b1.[;
lower_bound Y = a1 by A43,A44,Th4;
then
A45: a < a1 by A1,A3,A35,A36,A43,A44,XXREAL_0:1,XXREAL_1:3,4;
a1 <= x by A5,A44,XXREAL_1:3;
then
A46: a < x by A45,XXREAL_0:2;
upper_bound Y = b1 & x < b1 by A5,A43,A44,Th5,XXREAL_1:3;
then x < b by A2,A37,XXREAL_0:2;
hence thesis by A35,A46,XXREAL_1:4;
end;
suppose
ex a, b st a < b & Y = ].a,b.];
then consider a1, b1 being Real such that
A47: a1 < b1 and
A48: Y = ].a1,b1.];
upper_bound Y = b1 by A47,A48,Th7;
then
A49: b1 < b by A2,A4,A35,A37,A47,A48,XXREAL_0:1,XXREAL_1:2,4;
x <= b1 by A5,A48,XXREAL_1:2;
then
A50: x < b by A49,XXREAL_0:2;
lower_bound Y = a1 & a1 < x by A5,A47,A48,Th6,XXREAL_1:2;
then a < x by A1,A36,XXREAL_0:2;
hence thesis by A35,A50,XXREAL_1:4;
end;
suppose
ex a, b st a < b & Y = ].a,b.[;
then consider a1, b1 being Real such that
A51: a1 < b1 & Y = ].a1,b1.[;
lower_bound Y = a1 & a1 < x by A5,A51,TOPREAL6:17,XXREAL_1:4;
then
A52: a < x by A1,A36,XXREAL_0:2;
upper_bound Y = b1 & x < b1 by A5,A51,TOPREAL6:17,XXREAL_1:4;
then x < b by A2,A37,XXREAL_0:2;
hence thesis by A35,A52,XXREAL_1:4;
end;
end;
end;
registration
cluster open closed interval non empty non real-bounded for Subset of REAL;
existence
proof
take [#]REAL;
thus thesis;
end;
end;
begin :: R^1
theorem Th32:
for X being Subset of R^1 st a <= b & X = [.a,b.] holds Fr X = { a,b}
proof
let X be Subset of R^1 such that
A1: a <= b and
A2: X = [.a,b.];
A3: Cl X = Cl [.a,b.] by A2,JORDAN5A:24
.= [.a,b.] by MEASURE6:59;
A4: [.a,b.] /\ (left_closed_halfline(a) \/ right_closed_halfline(b)) = {a,b
} by A1,Th8;
set LO = R^1(left_open_halfline(a)), RC = R^1(right_closed_halfline(b)), RO
= R^1(right_open_halfline(b)), LC = R^1(left_closed_halfline(a));
A5: RC = right_closed_halfline(b) by TOPREALB:def 3;
A6: LC = left_closed_halfline(a) by TOPREALB:def 3;
A7: RO = right_open_halfline(b) by TOPREALB:def 3;
A8: LO = left_open_halfline(a) by TOPREALB:def 3;
then
A9: [.a,b.]` = LO \/ RO by A7,XXREAL_1:385;
Cl X` = Cl [.a,b.]` by A2,JORDAN5A:24,TOPMETR:17
.= Cl left_open_halfline(a) \/ Cl right_open_halfline(b) by A8,A7,A9,Th3
.= Cl LO \/ Cl right_open_halfline(b) by A8,JORDAN5A:24
.= Cl LO \/ Cl RO by A7,JORDAN5A:24
.= LC \/ Cl RO by A6,BORSUK_5:51,TOPREALB:def 3
.= LC \/ RC by A5,BORSUK_5:49,TOPREALB:def 3
.= left_closed_halfline(a) \/ right_closed_halfline(b) by A5,TOPREALB:def 3
;
hence thesis by A3,A4,TOPS_1:def 2;
end;
theorem
for X being Subset of R^1 st a < b & X = ].a,b.[ holds Fr X = {a,b}
proof
let X be Subset of R^1 such that
A1: a < b and
A2: X = ].a,b.[;
A3: Cl X = Cl ].a,b.[ by A2,JORDAN5A:24
.= [.a,b.] by A1,JORDAN5A:26;
set RC = R^1(right_closed_halfline(b)), LC = R^1(left_closed_halfline(a));
A4: RC = right_closed_halfline(b) & LC = left_closed_halfline(a) by
TOPREALB:def 3;
then
A5: ].a,b.[` = LC \/ RC by XXREAL_1:398;
A6: [.a,b.] /\ (left_closed_halfline(a) \/ right_closed_halfline(b)) = {a,b}
by A1,Th8;
Cl X` = Cl ].a,b.[` by A2,JORDAN5A:24,TOPMETR:17
.= Cl left_closed_halfline(a) \/ Cl right_closed_halfline(b) by A4,A5,Th3
.= Cl left_closed_halfline(a) \/ right_closed_halfline(b) by MEASURE6:59
.= left_closed_halfline(a) \/ right_closed_halfline(b) by MEASURE6:59;
hence thesis by A3,A6,TOPS_1:def 2;
end;
theorem Th34:
for X being Subset of R^1 st a < b & X = [.a,b.[ holds Fr X = {a ,b}
proof
let X be Subset of R^1 such that
A1: a < b and
A2: X = [.a,b.[;
A3: Cl X = [.a,b.] & [.a,b.] /\ (left_closed_halfline(a) \/
right_closed_halfline(b)) = {a,b} by A1,A2,Th8,BORSUK_5:35;
set LO = R^1(left_open_halfline(a)), RC = R^1(right_closed_halfline(b)), LC
= R^1(left_closed_halfline(a));
A4: RC = right_closed_halfline(b) by TOPREALB:def 3;
A5: LO = left_open_halfline(a) by TOPREALB:def 3;
then
A6: [.a,b.[` = LO \/ RC by A4,XXREAL_1:382;
A7: LC = left_closed_halfline(a) by TOPREALB:def 3;
Cl X` = Cl [.a,b.[` by A2,JORDAN5A:24,TOPMETR:17
.= Cl left_open_halfline(a) \/ Cl right_closed_halfline(b) by A5,A4,A6,Th3
.= Cl LO \/ Cl right_closed_halfline(b) by A5,JORDAN5A:24
.= Cl LO \/ Cl RC by A4,JORDAN5A:24
.= LC \/ Cl RC by A7,BORSUK_5:51,TOPREALB:def 3
.= left_closed_halfline(a) \/ right_closed_halfline(b) by A4,A7,PRE_TOPC:22
;
hence thesis by A3,TOPS_1:def 2;
end;
theorem Th35:
for X being Subset of R^1 st a < b & X = ].a,b.] holds Fr X = {a ,b}
proof
let X be Subset of R^1 such that
A1: a < b and
A2: X = ].a,b.];
A3: Cl X = [.a,b.] & [.a,b.] /\ (left_closed_halfline(a) \/
right_closed_halfline(b)) = {a,b} by A1,A2,Th8,BORSUK_5:36;
A4: ].a,b.]` = left_closed_halfline(a) \/ right_open_halfline(b) by
XXREAL_1:399;
set RO = R^1(right_open_halfline(b)), LC = R^1(left_closed_halfline(a));
A5: RO = right_open_halfline(b) by TOPREALB:def 3;
A6: LC = left_closed_halfline(a) by TOPREALB:def 3;
Cl X` = Cl ].a,b.]` by A2,JORDAN5A:24,TOPMETR:17
.= Cl left_closed_halfline(a) \/ Cl right_open_halfline(b) by A4,Th3
.= Cl LC \/ Cl right_open_halfline(b) by A6,JORDAN5A:24
.= Cl LC \/ Cl RO by A5,JORDAN5A:24
.= LC \/ Cl RO by PRE_TOPC:22
.= left_closed_halfline(a) \/ right_closed_halfline(b) by A6,BORSUK_5:49
,TOPREALB:def 3;
hence thesis by A3,TOPS_1:def 2;
end;
theorem
for X being Subset of R^1 st X = [.a,b.] holds Int X = ].a,b.[
proof
let X be Subset of R^1 such that
A1: X = [.a,b.];
A2: Int X c= X by TOPS_1:16;
thus Int X c= ].a,b.[
proof
let x be object;
assume
A3: x in Int X;
then reconsider x as Point of R^1;
A4: now
now
assume a > b;
then X = {}R^1 by A1,XXREAL_1:29;
hence contradiction by A3;
end;
then Fr X = {a,b} by A1,Th32;
then
A5: a in Fr X & b in Fr X by TARSKI:def 2;
A6: Int X misses Fr X by TOPS_1:39;
assume x = a or x = b;
hence contradiction by A3,A6,A5,XBOOLE_0:3;
end;
x <= b by A1,A2,A3,XXREAL_1:1;
then
A7: x < b by A4,XXREAL_0:1;
a <= x by A1,A2,A3,XXREAL_1:1;
then a < x by A4,XXREAL_0:1;
hence thesis by A7,XXREAL_1:4;
end;
reconsider Y = ].a,b.[ as open Subset of R^1 by BORSUK_5:39,TOPMETR:17;
Y c= Int X by A1,TOPS_1:24,XXREAL_1:37;
hence thesis;
end;
theorem
for X being Subset of R^1 st X = ].a,b.[ holds Int X = ].a,b.[
proof
let X be Subset of R^1;
assume
A1: X = ].a,b.[;
then reconsider X as open Subset of R^1 by BORSUK_5:39;
Int X = X by TOPS_1:23;
hence thesis by A1;
end;
theorem Th38:
for X being Subset of R^1 st X = [.a,b.[ holds Int X = ].a,b.[
proof
let X be Subset of R^1 such that
A1: X = [.a,b.[;
A2: Int X c= X by TOPS_1:16;
thus Int X c= ].a,b.[
proof
let x be object;
assume
A3: x in Int X;
then reconsider x as Point of R^1;
A4: now
now
assume a >= b;
then X = {}R^1 by A1,XXREAL_1:27;
hence contradiction by A3;
end;
then Fr X = {a,b} by A1,Th34;
then
A5: Int X misses Fr X & a in Fr X by TARSKI:def 2,TOPS_1:39;
assume x = a;
hence contradiction by A3,A5,XBOOLE_0:3;
end;
a <= x by A1,A2,A3,XXREAL_1:3;
then
A6: a < x by A4,XXREAL_0:1;
x < b by A1,A2,A3,XXREAL_1:3;
hence thesis by A6,XXREAL_1:4;
end;
reconsider Y = ].a,b.[ as open Subset of R^1 by BORSUK_5:39,TOPMETR:17;
Y c= Int X by A1,TOPS_1:24,XXREAL_1:45;
hence thesis;
end;
theorem Th39:
for X being Subset of R^1 st X = ].a,b.] holds Int X = ].a,b.[
proof
let X be Subset of R^1 such that
A1: X = ].a,b.];
A2: Int X c= X by TOPS_1:16;
thus Int X c= ].a,b.[
proof
let x be object;
assume
A3: x in Int X;
then reconsider x as Point of R^1;
A4: now
now
assume a >= b;
then X = {}R^1 by A1,XXREAL_1:26;
hence contradiction by A3;
end;
then Fr X = {a,b} by A1,Th35;
then
A5: Int X misses Fr X & b in Fr X by TARSKI:def 2,TOPS_1:39;
assume x = b;
hence contradiction by A3,A5,XBOOLE_0:3;
end;
x <= b by A1,A2,A3,XXREAL_1:2;
then
A6: x < b by A4,XXREAL_0:1;
a < x by A1,A2,A3,XXREAL_1:2;
hence thesis by A6,XXREAL_1:4;
end;
reconsider Y = ].a,b.[ as open Subset of R^1 by BORSUK_5:39,TOPMETR:17;
Y c= Int X by A1,TOPS_1:24,XXREAL_1:41;
hence thesis;
end;
registration let T be real-membered TopStruct, X be interval Subset of T;
cluster T|X -> interval;
coherence
by PRE_TOPC:def 5;
end;
registration
let A be interval Subset of REAL;
cluster R^1(A) -> interval;
coherence by TOPREALB:def 3;
end;
registration
cluster connected -> interval for Subset of R^1;
coherence
by BORSUK_5:77;
cluster interval -> connected for Subset of R^1;
coherence
proof let X be Subset of R^1 such that
A1: X is interval;
A2: X is Subset of REAL by MEMBERED:3;
per cases by A1,A2,Th29;
suppose
X is empty;
then reconsider A=X as empty Subset of R^1;
A is interval;
hence thesis;
end;
suppose
X = REAL;
then reconsider A=X as non empty interval Subset of R^1;
R^1|A is connected;
hence R^1|X is connected;
end;
suppose
ex a st X = left_closed_halfline(a);
then consider a such that
A3: X = left_closed_halfline(a);
reconsider A=X as non empty interval Subset of R^1 by A3;
R^1|A is connected;
hence R^1|X is connected;
end;
suppose
ex a st X = left_open_halfline(a);
then consider a such that
A4: X = left_open_halfline(a);
reconsider A=X as non empty interval Subset of R^1 by A4;
R^1|A is connected;
hence R^1|X is connected;
end;
suppose
ex a st X = right_closed_halfline(a);
then consider a such that
A5: X = right_closed_halfline(a);
reconsider A=X as non empty interval Subset of R^1 by A5;
R^1|A is connected;
hence R^1|X is connected;
end;
suppose
ex a st X = right_open_halfline(a);
then consider a such that
A6: X = right_open_halfline(a);
reconsider A=X as non empty interval Subset of R^1 by A6;
R^1|A is connected;
hence R^1|X is connected;
end;
suppose
ex a, b st a <= b & X = [.a,b.];
then reconsider A=X as non empty interval Subset of R^1 by XXREAL_1:1;
R^1|A is connected;
hence R^1|X is connected;
end;
suppose
ex a, b st a < b & X = [.a,b.[;
then reconsider A=X as non empty interval Subset of R^1 by XXREAL_1:3;
R^1|A is connected;
hence R^1|X is connected;
end;
suppose
ex a, b st a < b & X = ].a,b.];
then reconsider A=X as non empty interval Subset of R^1 by XXREAL_1:2;
R^1|A is connected;
hence R^1|X is connected;
end;
suppose
ex a, b st a < b & X = ].a,b.[;
then reconsider A=X as non empty interval Subset of R^1 by XXREAL_1:33;
R^1|A is connected;
hence R^1|X is connected;
end;
end;
end;
begin :: Closed Interval TSpace
registration
let r;
cluster Closed-Interval-TSpace(r,r) -> 1-element;
coherence
proof
{r} is 1-element & the carrier of Closed-Interval-TSpace(r,r) = [.r,r.]
by TOPMETR:18;
hence the carrier of Closed-Interval-TSpace(r,r) is 1-element
by XXREAL_1:17;
end;
end;
theorem
r <= s implies for A being Subset of Closed-Interval-TSpace(r,s) holds
A is real-bounded Subset of REAL
proof
assume r <= s;
then
A1: the carrier of Closed-Interval-TSpace(r,s) = [.r,s.] by TOPMETR:18;
let A be Subset of Closed-Interval-TSpace(r,s);
A is bounded_above bounded_below by A1,XXREAL_2:43,44;
hence thesis by A1,XBOOLE_1:1;
end;
theorem Th41:
r <= s implies for X being Subset of Closed-Interval-TSpace(r,s)
st X = [.a,b.[ & r < a & b <= s holds Int X = ].a,b.[
proof
set L = Closed-Interval-TSpace(r,s);
set c = (r+a)/2;
set C1 = R^1(].c,b.[);
A1: C1 = ].c,b.[ by TOPREALB:def 3;
assume r <= s;
then
A2: the carrier of L = [.r,s.] by TOPMETR:18;
let X be Subset of Closed-Interval-TSpace(r,s) such that
A3: X = [.a,b.[ and
A4: r < a and
A5: b <= s;
A6: r < c by A4,XREAL_1:226;
A7: C1 c= the carrier of L
proof
let x be object;
assume
A8: x in C1;
then reconsider x as Real;
x < b by A1,A8,XXREAL_1:4;
then
A9: x <= s by A5,XXREAL_0:2;
c < x by A1,A8,XXREAL_1:4;
then r <= x by A6,XXREAL_0:2;
hence thesis by A2,A9,XXREAL_1:1;
end;
reconsider A = X as Subset of R^1 by PRE_TOPC:11;
A10: c < a by A4,XREAL_1:226;
A c= C1
proof
let x be object;
assume
A11: x in A;
then reconsider x as Real;
a <= x by A3,A11,XXREAL_1:3;
then
A12: c < x by A10,XXREAL_0:2;
x < b by A3,A11,XXREAL_1:3;
hence thesis by A1,A12,XXREAL_1:4;
end;
then Int A = Int X by A7,TOPS_3:57;
hence thesis by A3,Th38;
end;
theorem Th42:
r <= s implies for X being Subset of Closed-Interval-TSpace(r,s)
st X = ].a,b.] & r <= a & b < s holds Int X = ].a,b.[
proof
set L = Closed-Interval-TSpace(r,s);
set c = (b+s)/2;
set C1 = R^1(].a,c.[);
A1: C1 = ].a,c.[ by TOPREALB:def 3;
assume r <= s;
then
A2: the carrier of L = [.r,s.] by TOPMETR:18;
let X be Subset of Closed-Interval-TSpace(r,s) such that
A3: X = ].a,b.] and
A4: r <= a and
A5: b < s;
A6: c < s by A5,XREAL_1:226;
A7: C1 c= the carrier of L
proof
let x be object;
assume
A8: x in C1;
then reconsider x as Real;
x < c by A1,A8,XXREAL_1:4;
then
A9: x <= s by A6,XXREAL_0:2;
a < x by A1,A8,XXREAL_1:4;
then r <= x by A4,XXREAL_0:2;
hence thesis by A2,A9,XXREAL_1:1;
end;
reconsider A = X as Subset of R^1 by PRE_TOPC:11;
A10: b < c by A5,XREAL_1:226;
A c= C1
proof
let x be object;
assume
A11: x in A;
then reconsider x as Real;
x <= b by A3,A11,XXREAL_1:2;
then
A12: x < c by A10,XXREAL_0:2;
a < x by A3,A11,XXREAL_1:2;
hence thesis by A1,A12,XXREAL_1:4;
end;
then Int A = Int X by A7,TOPS_3:57;
hence thesis by A3,Th39;
end;
theorem Th43:
for X being Subset of Closed-Interval-TSpace(r,s), Y being
Subset of REAL st X = Y holds X is connected iff Y is interval
proof
let X be Subset of Closed-Interval-TSpace(r,s), Y be Subset of REAL such
that
A1: X = Y;
reconsider Z = X as Subset of R^1 by A1,TOPMETR:17;
hereby
assume X is connected;
then Z is connected by CONNSP_1:23;
hence Y is interval by A1;
end;
assume Y is interval;
then Z is connected by A1;
hence thesis by CONNSP_1:23;
end;
registration
let T be TopSpace;
cluster open closed connected for Subset of T;
existence
proof
take {}T;
thus thesis;
end;
end;
registration
let T be non empty connected TopSpace;
cluster non empty open closed connected for Subset of T;
existence
proof
take [#]T;
thus thesis by CONNSP_1:27;
end;
end;
theorem Th44:
r <= s implies for X being open connected Subset of
Closed-Interval-TSpace(r,s) holds X is empty or X = [.r,s.] or (ex a being Real
st r < a & a <= s & X = [.r,a.[) or (ex a being Real st r <= a &
a < s & X = ].a,s.]) or ex a, b being Real st r <= a & a < b & b <= s &
X = ].a,b.[
proof
set L = Closed-Interval-TSpace(r,s);
assume
A1: r <= s;
then
A2: the carrier of L = [.r,s.] by TOPMETR:18;
let X be open connected Subset of L;
X is bounded_above bounded_below Subset of REAL by A2,XBOOLE_1:1,XXREAL_2:43
,44;
then reconsider Y = X as real-bounded interval Subset of REAL by Th43;
A3: the carrier of L = [#]L & L is connected by A1,TREAL_1:20;
A4: s in [.r,s.] by A1,XXREAL_1:1;
A5: r in [.r,s.] by A1,XXREAL_1:1;
per cases by Th29;
suppose
Y is empty or Y = [#]REAL;
hence thesis;
end;
suppose
(ex a st Y = left_closed_halfline(a)) or (ex a st Y =
left_open_halfline(a)) or (ex a st Y = right_closed_halfline(a)) or ex a st Y =
right_open_halfline(a);
hence thesis;
end;
suppose
ex a, b st a <= b & Y = [.a,b.];
then consider a, b such that
A6: a <= b and
A7: Y = [.a,b.];
A8: X <> {}L by A6,A7,XXREAL_1:1;
A9: r <= a & b <= s by A2,A6,A7,XXREAL_1:50;
then
A10: X is closed by A7,TOPREALA:23;
now
assume
A11: r <> a or b <> s;
per cases by A9,A11,XXREAL_0:1;
suppose
r < a;
then not r in X by A7,XXREAL_1:1;
hence contradiction by A2,A3,A5,A8,A10,CONNSP_1:13;
end;
suppose
b < s;
then not s in X by A7,XXREAL_1:1;
hence contradiction by A2,A3,A4,A8,A10,CONNSP_1:13;
end;
end;
hence thesis by A7;
end;
suppose
ex a, b st a < b & Y = [.a,b.[;
then consider a, b such that
A12: a < b and
A13: Y = [.a,b.[;
A14: b <= s by A2,A12,A13,XXREAL_1:52;
A15: r <= a by A2,A12,A13,XXREAL_1:52;
now
assume r <> a;
then
A16: r < a by A15,XXREAL_0:1;
now
Int X = ].a,b.[ by A1,A13,A14,A16,Th41;
then
A17: not a in Int X by XXREAL_1:4;
assume Int X = X;
hence contradiction by A12,A13,A17,XXREAL_1:3;
end;
hence contradiction by TOPS_1:23;
end;
hence thesis by A12,A13,A14;
end;
suppose
ex a, b st a < b & Y = ].a,b.];
then consider a, b such that
A18: a < b and
A19: Y = ].a,b.];
A20: r <= a by A2,A18,A19,XXREAL_1:53;
A21: b <= s by A2,A18,A19,XXREAL_1:53;
now
assume b <> s;
then
A22: b < s by A21,XXREAL_0:1;
now
Int X = ].a,b.[ by A1,A19,A20,A22,Th42;
then
A23: not b in Int X by XXREAL_1:4;
assume Int X = X;
hence contradiction by A18,A19,A23,XXREAL_1:2;
end;
hence contradiction by TOPS_1:23;
end;
hence thesis by A18,A19,A20;
end;
suppose
ex a, b st a < b & Y = ].a,b.[;
then consider a, b such that
A24: a < b & Y = ].a,b.[;
r <= a & b <= s by A2,A24,XXREAL_1:51;
hence thesis by A24;
end;
end;
begin :: Minimal cover of an interval
deffunc F(set) = $1;
defpred P[set,set] means $1 c= $2;
theorem Th45:
for T being 1-sorted, F being finite Subset-Family of T for F1
being Subset-Family of T st F is Cover of T & F1 = F \ {X where X is Subset of
T: X in F & ex Y being Subset of T st Y in F & X c< Y} holds F1 is Cover of T
proof
let T be 1-sorted, F be finite Subset-Family of T, F1 be Subset-Family of T
such that
A1: the carrier of T c= union F and
A2: F1 = F \ {X where X is Subset of T: X in F & ex Y being Subset of T
st Y in F & X c< Y};
set ZAW = {X where X is Subset of T: X in F & ex Y being Subset of T st Y in
F & X c< Y};
thus the carrier of T c= union F1
proof
let t be object;
assume t in the carrier of T;
then consider Z being set such that
A3: t in Z and
A4: Z in F by A1,TARSKI:def 4;
set ALL = {X where X is Subset of T: Z c< X & X in F};
per cases;
suppose
A5: ALL is empty;
now
assume Z in ZAW;
then consider X being Subset of T such that
A6: Z = X and
X in F and
A7: ex Y being Subset of T st Y in F & X c< Y;
consider Y being Subset of T such that
A8: Y in F & X c< Y by A7;
Y in ALL by A6,A8;
hence contradiction by A5;
end;
then Z in F1 by A2,A4,XBOOLE_0:def 5;
hence thesis by A3,TARSKI:def 4;
end;
suppose
ALL is non empty;
then consider w being object such that
A9: w in ALL;
consider R being Relation of ALL such that
A10: for x, y being set holds [x,y] in R iff x in ALL & y in ALL & P
[x,y] from RELSET_1:sch 5;
A11: R is_reflexive_in ALL
by A10;
then
A12: field R = ALL by ORDERS_1:13;
A13: R partially_orders ALL
proof
thus R is_reflexive_in ALL by A11;
thus R is_transitive_in ALL
proof
let x, y, z be object;
assume that
A14: x in ALL and
y in ALL and
A15: z in ALL;
assume
A16: [x,y] in R & [y,z] in R;
reconsider x,y,z as set by TARSKI:1;
x c= y & y c= z by A10,A16;
then x c= z;
hence thesis by A10,A14,A15;
end;
let x, y be object;
assume that
x in ALL and
y in ALL;
assume
A17: [x,y] in R & [y,x] in R;
reconsider x,y as set by TARSKI:1;
x c= y & y c= x by A10,A17;
hence thesis by XBOOLE_0:def 10;
end;
A18: R is reflexive by A11,A12;
ALL has_upper_Zorn_property_wrt R
proof
let Y be set such that
A19: Y c= ALL and
A20: R |_2 Y is being_linear-order;
per cases;
suppose
A21: Y is non empty;
defpred U[set] means $1 is non empty & $1 c= Y implies union $1 in Y;
take union Y;
A22: U[{}];
A23: for A, B being set st A in Y & B in Y holds A \/ B in Y
proof
A24: R |_2 Y c= R by XBOOLE_1:17;
R |_2 Y is connected by A20;
then
A25: R |_2 Y is_connected_in field (R |_2 Y);
let A, B be set such that
A26: A in Y & B in Y;
field(R |_2 Y) = Y by A12,A18,A19,ORDERS_1:71;
then [A,B] in R |_2 Y or [B,A] in R |_2 Y or A = B by A26,A25;
then A c= B or B c= A by A10,A24;
hence thesis by A26,XBOOLE_1:12;
end;
A27: for x, B being set st x in Y & B c= Y & U[B] holds U[B \/ {x}]
proof
let x, B be set such that
A28: x in Y and
A29: B c= Y & U[B] and
B \/ {x} is non empty and
B \/ {x} c= Y;
A30: union {x} = x by ZFMISC_1:25;
per cases;
suppose
B is empty;
hence thesis by A28,ZFMISC_1:25;
end;
suppose
B is non empty;
then x \/ union B in Y by A23,A28,A29;
hence thesis by A30,ZFMISC_1:78;
end;
end;
consider y being object such that
A31: y in Y by A21;
y in ALL by A19,A31;
then consider X being Subset of T such that
A32: X = y and
A33: Z c< X and
X in F;
A34: X c= union Y by A31,A32,ZFMISC_1:74;
then
A35: Z <> union Y by A33,XBOOLE_0:def 8;
Z c= X by A33;
then Z c= union Y by A34;
then
A36: Z c< union Y by A35;
A37: ALL c= F
proof
let x be object;
assume x in ALL;
then ex X being Subset of T st X = x & Z c< X & X in F;
hence thesis;
end;
then
A38: Y c= F by A19;
A39: Y is finite by A19,A37;
U[Y] from FINSET_1:sch 2(A39,A22,A27);
then union Y in F by A21,A38;
hence
A40: union Y in ALL by A36;
let z be set;
assume
A41: z in Y;
then P[z,union Y] by ZFMISC_1:74;
hence thesis by A10,A19,A40,A41;
end;
suppose
A42: Y is empty;
reconsider w as set by TARSKI:1;
take w;
thus w in ALL by A9;
thus thesis by A42;
end;
end;
then consider M being set such that
A43: M is_maximal_in R by A12,A13,ORDERS_1:63;
A44: M in field R by A43;
then
A45: ex X being Subset of T st X = M & Z c< X & X in F by A12;
now
assume M in ZAW;
then consider H being Subset of T such that
A46: M = H and
H in F and
A47: ex Y being Subset of T st Y in F & H c< Y;
consider Y being Subset of T such that
A48: Y in F and
A49: H c< Y by A47;
Z c< Y by A45,A46,A49,XBOOLE_1:56;
then
A50: Y in ALL by A48;
H c= Y by A49;
then [M,Y] in R by A10,A12,A44,A46,A50;
hence contradiction by A12,A43,A46,A49,A50;
end;
then
A51: M in F1 by A2,A45,XBOOLE_0:def 5;
Z c= M by A45;
hence thesis by A3,A51,TARSKI:def 4;
end;
end;
end;
theorem Th46:
for S being 1-element 1-sorted, s being Point of S, F
being Subset-Family of S st F is Cover of S holds {s} in F
proof
let S be 1-element 1-sorted, s be Point of S, F be Subset-Family of
S such that
A1: the carrier of S c= union F;
consider d being Element of S such that
A2: the carrier of S = {d} by TEX_1:def 1;
s in the carrier of S;
then consider Z being set such that
A3: s in Z and
A4: Z in F by A1,TARSKI:def 4;
A5: s = d by ZFMISC_1:def 10;
Z = {s}
proof
thus for x being object st x in Z holds x in {s} by A4,A2,A5;
let x be object;
thus thesis by A3,TARSKI:def 1;
end;
hence thesis by A4;
end;
definition
let T be TopStruct, F be Subset-Family of T;
attr F is connected means
for X being Subset of T st X in F holds X is connected;
end;
registration
let T be TopSpace;
cluster non empty open closed connected for Subset-Family of T;
existence
proof
{{}T} c= bool the carrier of T
proof
let x be object;
assume x in {{}T};
then x = {}T by TARSKI:def 1;
hence thesis;
end;
then reconsider F = {{}T} as Subset-Family of T;
take F;
thus F is non empty;
thus for P being Subset of T holds P in F implies P is open by TARSKI:def 1
;
thus for P being Subset of T holds P in F implies P is closed by
TARSKI:def 1;
thus for P being Subset of T holds P in F implies P is connected by
TARSKI:def 1;
end;
end;
reserve n, m for Nat,
F for Subset-Family of Closed-Interval-TSpace (r,s);
Lm3: [.r,s.] in F & r <= s implies rng <*[.r,s.]*> c= F & union rng <*[.r,s.]
*> = [.r,s.] & for n being Nat st 1 <= n holds (n <= len <*[.r,s.]*>
implies <*[.r,s.]*>/.n is non empty) & (n+1 <= len <*[.r,s.]*> implies
lower_bound(<*[.r,s.]*>/.n) <= lower_bound(<*[.r,s.]*>/.(n+1)) & upper_bound(<*
[.r,s.]*>/.n) <= upper_bound(<*[.r,s.]*>/.(n+1)) & lower_bound(<*[.r,s.]*>/.(n+
1)) < upper_bound(<*[.r,s.]*>/.n)) & (n+2 <= len <*[.r,s.]*> implies
upper_bound(<*[.r,s.]*>/.n) <= lower_bound(<*[.r,s.]*>/.(n+2)))
proof
assume that
A1: [.r,s.] in F and
A2: r <= s;
set f = <*[.r,s.]*>;
A3: rng f = {[.r,s.]} by FINSEQ_1:38;
thus rng f c= F
by A1,A3,TARSKI:def 1;
thus union rng f = [.r,s.] by A3,ZFMISC_1:25;
let n be Nat;
assume
A4: 1 <= n;
hereby
assume n <= len f;
then n <= 1 by FINSEQ_1:39;
then n = 1 by A4,XXREAL_0:1;
then f/.n = [.r,s.] by FINSEQ_4:16;
hence f/.n is non empty by A2,XXREAL_1:1;
end;
hereby
assume n+1 <= len f;
then n+1 <= 0+1 by FINSEQ_1:39;
hence lower_bound(f/.n) <= lower_bound(f/.(n+1)) & upper_bound(f/.n) <=
upper_bound(f/.(n+1)) & lower_bound(f/.(n+1)) < upper_bound(f/.n) by A4,
XREAL_1:6;
end;
assume n+2 <= len f;
then n+1+1 <= 0+1 by FINSEQ_1:39;
hence thesis by XREAL_1:6;
end;
theorem Th47:
for L being TopSpace, G, G1 being Subset-Family of L st G is
Cover of L & G is finite for ALL being set st G1 = G \ {X where X is Subset of
L: X in G & ex Y being Subset of L st Y in G & X c< Y} & ALL = {C where C is
Subset-Family of L: C is Cover of L & C c= G1} holds ALL
has_lower_Zorn_property_wrt RelIncl ALL
proof
let L be TopSpace;
let G, G1 be Subset-Family of L;
assume that
A1: G is Cover of L and
A2: G is finite;
let ALL be set;
set ZAW = {X where X is Subset of L: X in G & ex Y being Subset of L st Y in
G & X c< Y};
assume that
A3: G1 = G \ ZAW and
A4: ALL = {C where C is Subset-Family of L: C is Cover of L & C c= G1};
A5: G1 is Cover of L by A1,A2,A3,Th45;
set R = RelIncl ALL;
A6: field R = ALL by WELLORD2:def 1;
let Y be set such that
A7: Y c= ALL and
A8: R |_2 Y is being_linear-order;
per cases;
suppose
A9: Y is non empty;
defpred A[set] means $1 is non empty implies meet $1 in Y;
set E = {F(D) where D is Subset-Family of L: D in bool G1};
take x = meet Y;
A10: ALL c= E
proof
let a be object;
assume a in ALL;
then ex C being Subset-Family of L st a = C & C is Cover of L & C c= G1
by A4;
hence thesis;
end;
A11: bool G1 is finite by A2,A3;
E is finite from FRAENKEL:sch 21(A11);
then
A12: Y is finite by A7,A10;
A13: for x, B being set st x in Y & B c= Y & A[B] holds A[B \/ {x}]
proof
let x, B be set such that
A14: x in Y and
B c= Y and
A15: A[B] and
B \/ {x} is non empty;
per cases;
suppose
B is empty;
hence thesis by A14,SETFAM_1:10;
end;
suppose
A16: B is non empty;
R |_2 Y is connected by A8;
then
A17: R |_2 Y is_connected_in field (R |_2 Y);
field (R |_2 Y) = Y by A6,A7,ORDERS_1:71;
then [x,meet B] in R |_2 Y or [meet B,x] in R |_2 Y or x = meet B by
A14,A15,A16,A17;
then [x,meet B] in R or [meet B,x] in R or x = meet B by XBOOLE_0:def 4
;
then
A18: meet B c= x or x c= meet B by A7,A14,A15,A16,WELLORD2:def 1;
meet (B \/ {x}) = meet B /\ meet {x} by A16,SETFAM_1:9
.= meet B /\ x by SETFAM_1:10;
hence thesis by A14,A15,A16,A18,XBOOLE_1:28;
end;
end;
consider y being object such that
A19: y in Y by A9;
y in ALL by A7,A19;
then
A20: ex C being Subset-Family of L st y = C & C is Cover of L & C c= G1 by A4;
then reconsider X = x as Subset-Family of L by A19,SETFAM_1:7;
A21: A[{}];
A22: A[Y] from FINSET_1:sch 2(A12,A21,A13);
A23: X is Cover of L
proof
let a be object;
assume
A24: a in the carrier of L;
meet Y in ALL by A7,A9,A22;
then consider C being Subset-Family of L such that
A25: meet Y = C and
A26: C is Cover of L and
C c= G1 by A4;
the carrier of L c= union C by A26,SETFAM_1:def 11;
hence thesis by A24,A25;
end;
x c= G1 by A19,A20,SETFAM_1:7;
hence
A27: x in ALL by A4,A23;
let y be set;
assume
A28: y in Y;
then x c= y by SETFAM_1:7;
hence thesis by A7,A27,A28,WELLORD2:def 1;
end;
suppose
A29: Y is empty;
take G1;
thus thesis by A4,A5,A29;
end;
end;
theorem Th48:
for L being TopSpace, G, ALL being set st ALL = {C where C is
Subset-Family of L: C is Cover of L & C c= G} for M being set st M
is_minimal_in RelIncl ALL & M in field RelIncl ALL for A1 being Subset of L st
A1 in M holds not ex A2, A3 being Subset of L st A2 in M & A3 in M & A1 c= A2
\/ A3 & A1 <> A2 & A1 <> A3
proof
let L be TopSpace;
let G be set;
let ALL be set such that
A1: ALL = {C where C is Subset-Family of L: C is Cover of L & C c= G};
set R = RelIncl ALL;
let M be set such that
A2: M is_minimal_in RelIncl ALL and
A3: M in field RelIncl ALL;
A4: field R = ALL by WELLORD2:def 1;
then consider C being Subset-Family of L such that
A5: M = C and
A6: C is Cover of L and
A7: C c= G by A1,A3;
let A1 be Subset of L such that
A8: A1 in M;
set Y = C \ {A1};
A9: Y <> M by A8,ZFMISC_1:56;
given A2, A3 being Subset of L such that
A10: A2 in M and
A11: A3 in M and
A12: A1 c= A2 \/ A3 and
A13: A1 <> A2 and
A14: A1 <> A3;
A15: union C = [#]L by A6,SETFAM_1:45;
union Y = the carrier of L
proof
thus union Y c= the carrier of L;
let x be object;
assume
A16: x in the carrier of L;
per cases;
suppose
A17: x in A1;
per cases by A12,A17,XBOOLE_0:def 3;
suppose
A18: x in A2;
A2 in Y by A5,A10,A13,ZFMISC_1:56;
hence thesis by A18,TARSKI:def 4;
end;
suppose
A19: x in A3;
A3 in Y by A5,A11,A14,ZFMISC_1:56;
hence thesis by A19,TARSKI:def 4;
end;
end;
suppose
A20: not x in A1;
consider Z being set such that
A21: x in Z and
A22: Z in C by A15,A16,TARSKI:def 4;
Z in Y by A20,A21,A22,ZFMISC_1:56;
hence thesis by A21,TARSKI:def 4;
end;
end;
then
A23: Y is Cover of L by SETFAM_1:def 11;
A24: Y c= M by A5,XBOOLE_1:36;
then Y c= G by A5,A7;
then
A25: Y in ALL by A1,A23;
then [Y,M] in R by A4,A3,A24,WELLORD2:def 1;
hence contradiction by A4,A2,A9,A25;
end;
registration let X be Subset-Family of REAL;
cluster -> real-membered for Element of X;
coherence
proof let S be Element of X;
per cases;
suppose X is non empty;
then S in X;
then S in bool REAL;
then S c= REAL;
hence thesis;
end;
suppose X is empty;
then S = {} by SUBSET_1:def 1;
then S c= REAL;
hence thesis;
end;
end;
end;
definition
let r, s be Real;
let F be Subset-Family of Closed-Interval-TSpace(r,s) such that
A1: F is Cover of Closed-Interval-TSpace(r,s) and
A2: F is open and
A3: F is connected and
A4: r <= s;
mode IntervalCover of F -> FinSequence of bool REAL means
:Def2:
rng it c= F
& union rng it = [.r,s.] & (for n being Nat st 1 <= n holds (n <=
len it implies it/.n is non empty) & (n+1 <= len it implies lower_bound(it/.n)
<= lower_bound(it/.(n+1)) & upper_bound(it/.n) <= upper_bound(it/.(n+1)) &
lower_bound(it/.(n+1)) < upper_bound(it/.n)) & (n+2 <= len it implies
upper_bound(it/.n) <= lower_bound(it/.(n+2)))) & ([.r,s.] in F implies it = <*
[.r,s.]*>) & (not [.r,s.] in F implies (ex p being Real st r < p & p <=
s & it.1 = [.r,p.[) & (ex p being Real st r <= p & p < s & it.len it =
].p,s.]) & for n being Nat st 1 < n & n < len it ex p, q being Real
st r <= p & p < q & q <= s & it.n = ].p,q.[ );
existence
proof
per cases;
suppose
A5: [.r,s.] in F;
take f = <*[.r,s.]*>;
A6: rng f = {[.r,s.]} by FINSEQ_1:38;
thus rng f c= F
by A5,A6,TARSKI:def 1;
thus union rng f = [.r,s.] by A6,ZFMISC_1:25;
thus thesis by A4,A5,Lm3;
end;
suppose
A7: not [.r,s.] in F;
set L = Closed-Interval-TSpace(r,s);
A8: the carrier of L = [.r,s.] by A4,TOPMETR:18;
A9: now
let A be Subset of L;
thus A is bounded_above bounded_below by A8,XXREAL_2:43,44;
hence A is real-bounded Subset of REAL by A8,XBOOLE_1:1;
end;
L is compact by A4,HEINE:4;
then [#]L is compact by COMPTS_1:1;
then consider G being Subset-Family of L such that
A10: G c= F and
A11: G is Cover of [#]L and
A12: G is finite by A1,A2,COMPTS_1:def 4;
set ZAW = {X where X is Subset of L: X in G & ex Y being Subset of L st
Y in G & X c< Y};
set G1 = G \ ZAW;
set ALL = {C where C is Subset-Family of L: C is Cover of L & C c= G1};
set R = RelIncl ALL;
A13: R is_antisymmetric_in ALL by WELLORD2:21;
set RM = {lower_bound ].c,s.] where c is Real: ].c,s.] in G1};
set LM = {upper_bound [.r,b.[ where b is Real: [.r,b.[ in G1};
A14: G1 c= G by XBOOLE_1:36;
then
A15: G1 c= F by A10;
A16: for X being set st X in G1 holds X is interval Subset of REAL
proof
let X be set;
assume X in G1;
then reconsider X as connected Subset of L by A3,A15;
reconsider Y = X as Subset of REAL by A8,XBOOLE_1:1;
Y is interval by Th43;
hence thesis;
end;
reconsider T = L as non empty connected TopSpace by A4,TREAL_1:20;
set LM1 = {upper_bound E where E is Subset of L: E in G1};
A17: LM c= LM1
proof
let x be object;
assume x in LM;
then ex b being Real st x = upper_bound [.r,b.[ & [.r,b.[ in G1;
hence thesis;
end;
A18: LM c= REAL
proof
let x be object;
assume x in LM;
then ex b being Real st x = upper_bound [.r,b.[ & [.r,b.[ in G1;
hence thesis by XREAL_0:def 1;
end;
set RM1 = {lower_bound E where E is Subset of L: E in G1};
A19: RM c= RM1
proof
let x be object;
assume x in RM;
then ex b being Real st x = lower_bound ].b,s.] & ].b,s.] in G1;
hence thesis;
end;
A20: RM c= REAL
proof
let x be object;
assume x in RM;
then ex b being Real st x = lower_bound ].b,s.] & ].b,s.] in G1;
hence thesis by XREAL_0:def 1;
end;
A21: field R = ALL by WELLORD2:def 1;
R is_reflexive_in ALL & R is_transitive_in ALL by WELLORD2:19,20;
then R partially_orders ALL by A13;
then consider M being set such that
A22: M is_minimal_in R by A11,A12,A21,Th47,ORDERS_1:64;
A23: M in field R by A22;
then consider C being Subset-Family of L such that
A24: M = C and
A25: C is Cover of L and
A26: C c= G1 by A21;
A27: union C = [#]L by A25,SETFAM_1:45;
A28: s in [.r,s.] by A4,XXREAL_1:1;
then consider R2 being set such that
A29: s in R2 and
A30: R2 in C by A8,A27,TARSKI:def 4;
r in [.r,s.] by A4,XXREAL_1:1;
then consider R1 being set such that
A31: r in R1 and
A32: R1 in C by A8,A27,TARSKI:def 4;
A33: R1 in G1 by A26,A32;
then
A34: R1 in F by A15;
A35: R2 in G1 by A26,A30;
then
A36: R2 in F by A15;
reconsider R1, R2 as open connected Subset of L by A2,A3,A15,A33,A35;
A37: now
per cases by A4,A7,A29,A36,Th44;
suppose
ex a being Real st r < a & a <= s & R2 = [.r,a.[;
hence RM is non empty by A29,XXREAL_1:3;
end;
suppose
ex a being Real st r <= a & a < s & R2 = ].a,s.];
then consider a being Real such that
r <= a and
a < s and
A38: R2 = ].a,s.];
lower_bound ].a,s.] in RM by A26,A30,A38;
hence RM is non empty;
end;
suppose
ex a, b being Real st r <= a & a < b & b <= s & R2 = ].a,b.[;
hence RM is non empty by A29,XXREAL_1:4;
end;
end;
A39: now
per cases by A4,A7,A31,A34,Th44;
suppose
ex a being Real st r < a & a <= s & R1 = [.r,a.[;
then consider a being Real such that
r < a and
a <= s and
A40: R1 = [.r,a.[;
upper_bound [.r,a.[ in LM by A26,A32,A40;
hence LM is non empty;
end;
suppose
ex a being Real st r <= a & a < s & R1 = ].a,s.];
hence LM is non empty by A31,XXREAL_1:2;
end;
suppose
ex a, b being Real st r <= a & a < b & b <= s & R1 = ].a,b.[;
hence LM is non empty by A31,XXREAL_1:4;
end;
end;
A41: G1 is finite by A12;
RM1 is finite from FRAENKEL:sch 21(A41);
then reconsider RM as non empty finite Subset of REAL by A19,A37,A20;
F c= bool REAL
proof
let a be object;
reconsider aa=a as set by TARSKI:1;
assume a in F;
then aa c= REAL by A8,XBOOLE_1:1;
hence thesis;
end;
then G1 c= bool REAL by A15;
then reconsider X = C as non empty finite Subset-Family of REAL
by A12,A26,A32,XBOOLE_1:1;
LM1 is finite from FRAENKEL:sch 21(A41);
then reconsider LM as non empty finite Subset of REAL by A17,A39,A18;
reconsider kL = max LM as Real;
set LEWY = [.r,kL.[;
kL in LM by XXREAL_2:def 8;
then consider b being Real such that
A42: kL = upper_bound [.r,b.[ and
A43: [.r,b.[ in G1;
A44: union G = [#]L by A11,SETFAM_1:45;
A45: now
consider x being object such that
A46: x in the carrier of L by XBOOLE_0:def 1;
consider g being set such that
A47: x in g and
A48: g in G by A44,A46,TARSKI:def 4;
{} c= g;
then
A49: {} c< g by A47;
assume
A50: {} in G1;
then {} in G by XBOOLE_0:def 5;
then {} in ZAW by A48,A49;
hence contradiction by A50,XBOOLE_0:def 5;
end;
then
A51: upper_bound LEWY = kL by A42,A43,Th5,XXREAL_1:27;
A52: r < b by A45,A43,XXREAL_1:27;
then r < kL by A42,Th5;
then
A53: lower_bound LEWY = r by Th4;
reconsider LEWY as non empty Subset of L by A45,A42,A43,Th5,XXREAL_1:27;
A54: kL = b by A45,A42,A43,Th5,XXREAL_1:27;
A55: for A being Subset of L st r in A & A in G1 holds A = LEWY
proof
let A be Subset of L;
assume that
A56: r in A and
A57: A in G1;
A58: A in F & A is open by A2,A15,A57;
A59: now
assume
A60: (ex a being Real st r <= a & a < s & A = ].a,s.])
or ex a, b being Real st r <= a & a < b & b <= s & A = ].a,b.[;
per cases by A60;
suppose
ex a being Real st r <= a & a < s & A = ].a,s.];
hence contradiction by A56,XXREAL_1:2;
end;
suppose
ex a, b being Real st r <= a & a < b & b <= s & A = ].a,b.[;
hence contradiction by A56,XXREAL_1:4;
end;
end;
A is connected by A3,A15,A57;
then consider ak being Real such that
A61: r < ak and
ak <= s and
A62: A = [.r,ak.[ by A4,A7,A56,A58,A59,Th44;
A63: A c= LEWY
proof
upper_bound A = ak by A61,A62,Th5;
then ak in LM by A57,A62;
then
A64: ak <= kL by XXREAL_2:def 8;
let a be object;
assume
A65: a in A;
then a in [.r,s.] by A8;
then reconsider a as Real;
a < ak by A62,A65,XXREAL_1:3;
then
A66: a < kL by A64,XXREAL_0:2;
r <= a by A62,A65,XXREAL_1:3;
hence thesis by A66,XXREAL_1:3;
end;
assume A <> LEWY;
then A c< LEWY by A63;
then A in ZAW by A14,A43,A54,A57;
hence contradiction by A57,XBOOLE_0:def 5;
end;
then reconsider LLEWY = LEWY as Element of X by A26,A31,A32;
reconsider pP = min RM as Real;
set PRAWY = ].pP,s.];
pP in RM by XXREAL_2:def 7;
then consider b being Real such that
A67: pP = lower_bound ].b,s.] and
A68: ].b,s.] in G1;
A69: lower_bound PRAWY = pP by A45,A67,A68,Th6,XXREAL_1:26;
A70: b < s by A45,A68,XXREAL_1:26;
then pP < s by A67,Th6;
then
A71: upper_bound PRAWY = s by Th7;
reconsider PRAWY as non empty Subset of L by A45,A67,A68,Th6,XXREAL_1:26;
A72: pP = b by A45,A67,A68,Th6,XXREAL_1:26;
A73: for A being Subset of L st A in G1 & A <> LEWY & A <> PRAWY ex a,
b being Real st a < b & A = ].a,b.[
proof
let A be Subset of L such that
A74: A in G1 and
A75: A <> LEWY and
A76: A <> PRAWY;
A77: A in F & A is open connected by A3,A2,A15,A74;
per cases by A4,A7,A45,A74,A77,Th44;
suppose
ex a being Real st r < a & a <= s & A = [.r,a.[;
then consider a being Real such that
r < a and
a <= s and
A78: A = [.r,a.[;
per cases;
suppose
a <= kL;
then A c= LEWY by A78,XXREAL_1:38;
then A c< LEWY by A75;
then A in ZAW by A14,A43,A54,A74;
hence thesis by A74,XBOOLE_0:def 5;
end;
suppose
a > kL;
then LEWY c= A by A78,XXREAL_1:38;
then LEWY c< A by A75;
then LEWY in ZAW by A14,A43,A54,A74;
hence thesis by A43,A54,XBOOLE_0:def 5;
end;
end;
suppose
ex a being Real st r <= a & a < s & A = ].a,s.];
then consider a being Real such that
r <= a and
a < s and
A79: A = ].a,s.];
per cases;
suppose
a >= pP;
then A c= PRAWY by A79,XXREAL_1:42;
then A c< PRAWY by A76;
then A in ZAW by A14,A68,A72,A74;
hence thesis by A74,XBOOLE_0:def 5;
end;
suppose
a < pP;
then PRAWY c= A by A79,XXREAL_1:42;
then PRAWY c< A by A76;
then PRAWY in ZAW by A14,A68,A72,A74;
hence thesis by A68,A72,XBOOLE_0:def 5;
end;
end;
suppose
ex a, b being Real st r <= a & a < b & b <= s & A = ].a,b.[;
then consider a, b being Real such that
r <= a and
A80: a < b and
b <= s and
A81: A = ].a,b.[;
reconsider a, b as Real;
take a, b;
thus thesis by A80,A81;
end;
end;
A82: for A being Subset of L st A in G1 & upper_bound A in A holds A = PRAWY
proof
let A be Subset of L such that
A83: A in G1 and
A84: upper_bound A in A and
A85: A <> PRAWY;
A <> LEWY by A51,A84,XXREAL_1:3;
then consider a, b being Real such that
A86: a < b and
A87: A = ].a,b.[ by A73,A83,A85;
upper_bound A = b by A86,A87,TOPREAL6:17;
hence contradiction by A84,A87,XXREAL_1:4;
end;
defpred F[set,set,set] means ex S being Element of X st S = $2 &
upper_bound( S qua real-membered set) in $3;
A88: X c= F by A15,A26;
A89: for Z being Subset of REAL st Z in X holds Z is non empty open
connected Subset of T
proof
let Z be Subset of REAL;
assume
A90: Z in X;
then Z is non empty interval by A45,A16,A26;
hence thesis by A2,A88,A90,Th43;
end;
A91: for n being Nat st 1 <= n & n < card X for x being
Element of X ex y being Element of X st F[n,x,y]
proof
let n be Nat such that
1 <= n and
n < card X;
let x be Element of X;
reconsider x1 = x as Subset of REAL;
A92: x1 is non empty by A89;
A93: x c= union X by ZFMISC_1:74;
then x c= [.r,s.] by A8,A27;
then x1 is bounded_above by XXREAL_2:43;
then upper_bound x is Element of L by A8,A27,A92,A93,Th2;
then consider y being set such that
A94: upper_bound x in y and
A95: y in X by A27,TARSKI:def 4;
reconsider y as Element of X by A95;
take y, x;
thus thesis by A94;
end;
consider IT being FinSequence of X such that
A96: len IT = card X and
A97: IT.1 = LLEWY or card X = 0 and
A98: for n being Nat st 1 <= n & n < card X holds F[n,IT
.n,IT.(n+1)] from RECDEF_1:sch 4(A91);
A99: rng IT c= X;
rng IT c= bool REAL by XBOOLE_1:1;
then reconsider IT as FinSequence of bool REAL by FINSEQ_1:def 4;
A100: IT is non empty by A96;
then
A101: rng IT is non empty;
then
A102: 1 in dom IT by FINSEQ_3:32;
then
A103: IT/.1 = IT.1 by PARTFUN1:def 6;
A104: for n being Nat st n in dom IT holds IT.n in X & IT/.n in X
proof
let n be Nat;
assume n in dom IT;
then IT.n = IT/.n & IT.n in rng IT by FUNCT_1:def 3,PARTFUN1:def 6;
hence thesis by A99;
end;
A105: for n being Nat st n in dom IT holds IT.n in G1 & IT/.n in G1
by A104,A26;
A106: for i being Nat st i in dom IT for x being Point of L
st x < upper_bound(IT/.i) ex j being Nat st j in dom IT & j <= i & x
in IT/.j
proof
defpred Q[Nat] means $1 in dom IT implies for x being Point
of L st x < upper_bound(IT/.$1) ex j being Nat st j in dom IT & j <=
$1 & x in IT/.j;
A107: Q[n] implies Q[n+1]
proof
assume that
A108: Q[n] and
A109: n+1 in dom IT;
A110: IT/.(n+1) = IT.(n+1) by A109,PARTFUN1:def 6;
let x be Point of L such that
A111: x < upper_bound(IT/.(n+1));
per cases by A109,TOPREALA:2;
suppose
A112: n = 0;
take 1;
thus 1 in dom IT by A101,FINSEQ_3:32;
thus 1 <= n+1 by A112;
r <= x by A8,XXREAL_1:1;
hence thesis by A51,A97,A111,A110,A112,XXREAL_1:3;
end;
suppose
A113: n in dom IT;
n+1 <= len IT by A109,FINSEQ_3:25;
then
A114: n < len IT by NAT_1:13;
1 <= n by A113,FINSEQ_3:25;
then
A115: ex S being Element of X st S = IT.n & upper_bound S in IT. (
n+1) by A96,A98,A114;
IT/.(n+1) in X by A104,A109;
then
A116: IT/.(n+1) is bounded_below by A9;
IT/.n = IT.n by A113,PARTFUN1:def 6;
then
A117: lower_bound(IT/.(n+1)) <= upper_bound(IT/.n) by A110,A116,A115,
SEQ_4:def 2;
A118: IT/.(n+1) is interval Subset of REAL & IT/.(n+1) is non
empty by A45,A16,A105,A109;
per cases by XXREAL_0:1;
suppose
x < upper_bound(IT/.n);
then consider j being Nat such that
A119: j in dom IT and
A120: j <= n and
A121: x in IT/.j by A108,A113;
take j;
thus j in dom IT by A119;
j+0 < n+1 by A120,XREAL_1:8;
hence j <= n+1;
thus thesis by A121;
end;
suppose
A122: x = upper_bound(IT/.n);
take n+1;
thus n+1 in dom IT by A109;
thus n+1 <= n+1;
thus thesis by A110,A113,A115,A122,PARTFUN1:def 6;
end;
suppose
A123: x > upper_bound(IT/.n);
take n+1;
thus n+1 in dom IT by A109;
thus n+1 <= n+1;
lower_bound(IT/.(n+1)) < x by A117,A123,XXREAL_0:2;
hence thesis by A111,A118,Th30;
end;
end;
end;
A124: Q[0] by FINSEQ_3:24;
A125: Q[n] from NAT_1:sch 2(A124,A107);
let i be Nat;
assume i in dom IT;
hence thesis by A125;
end;
A126: s in ].b,s.] by A70,XXREAL_1:2;
A127: for i being Nat st i in dom IT for j being Nat
st j in dom IT & i < j ex y being Point of L st y in IT/.j & for x being
Point of L st x in IT/.i holds x < y
proof
let i be Nat such that
A128: i in dom IT;
defpred W[Nat] means $1 in dom IT & i < $1 implies ex y
being Point of L st y in IT/.$1 & for x being Point of L st x in IT/.i holds x
< y;
A129: for n holds W[n] implies W[n+1]
proof
let n;
assume that
A130: W[n] and
A131: n+1 in dom IT;
A132: IT/.(n+1) = IT.(n+1) by A131,PARTFUN1:def 6;
assume
A133: i < n+1;
then
A134: i <= n by NAT_1:13;
per cases by A131,TOPREALA:2;
suppose
n = 0;
then i = 0 by A133,NAT_1:13;
hence thesis by A128,FINSEQ_3:24;
end;
suppose
A135: n in dom IT;
then
A136: IT/.n in X by A104;
then
A137: IT/.n is bounded_above by A9;
A138: IT/.n = IT.n by A135,PARTFUN1:def 6;
then IT/.n in rng IT by A135,FUNCT_1:def 3;
then
A139: IT/.n is non empty & IT/.n is Subset of L by A89,A99;
then upper_bound(IT/.n) in [.r,s.] by A8,A137,Th2;
then
A140: upper_bound(IT/.n) <= s by XXREAL_1:1;
A141: IT/.(n+1) in X by A104,A131;
A142: 1 <= n by A135,FINSEQ_3:25;
A143: IT/.(n+1) in rng IT by A131,A132,FUNCT_1:def 3;
then
A144: IT/.(n+1) is open connected Subset of L by A89,A99;
then
A145: IT/.(n+1) is interval Subset of REAL by Th43;
A146: n+1 <= len IT by A131,FINSEQ_3:25;
then n is Element of NAT & n < card X by A96,NAT_1:13
,ORDINAL1:def 12;
then consider S being Element of X such that
A147: S = IT.n and
A148: upper_bound S in IT.(n+1) by A98,A142;
IT/.(n+1) is bounded_below by A9,A144;
then
A149: lower_bound(IT/.(n+1)) <= upper_bound S by A132,A148,SEQ_4:def 2;
A150: IT/.(n+1) is bounded_above by A9,A144;
then
A151: upper_bound S <= upper_bound(IT/.(n+1)) by A132,A148,SEQ_4:def 1;
A152: IT/.(n+1) is non empty by A89,A99,A143;
then upper_bound(IT/.(n+1)) in [.r,s.] by A8,A144,A150,Th2;
then
A153: upper_bound(IT/.(n+1)) <= s by XXREAL_1:1;
per cases by A134,XXREAL_0:1;
suppose
i < n;
then consider y being Point of L such that
A154: y in IT/.n and
A155: for x being Point of L st x in IT/.i holds x < y by A130,A135;
A156: y <= upper_bound(IT/.n) by A137,A154,SEQ_4:def 1;
per cases by A151,XXREAL_0:1;
suppose
A157: upper_bound S < upper_bound(IT/.(n+1));
set y1 = (upper_bound S + upper_bound(IT/.(n+1))) / 2;
A158: upper_bound S < y1 by A157,XREAL_1:226;
upper_bound S in [.r,s.] by A8,A138,A137,A139,A147,Th2;
then r <= upper_bound S by XXREAL_1:1;
then
A159: r <= y1 by A158,XXREAL_0:2;
y1 < upper_bound(IT/.(n+1)) by A157,XREAL_1:226;
then y1 < s by A153,XXREAL_0:2;
then reconsider y1 as Point of L by A8,A159,XXREAL_1:1;
take y1;
lower_bound(IT/.(n+1)) < y1 by A149,A158,XXREAL_0:2;
hence y1 in IT/.(n+1) by A145,A152,A157,Th30,XREAL_1:226;
let x be Point of L;
assume x in IT/.i;
then x < upper_bound(IT/.n) by A155,A156,XXREAL_0:2;
hence thesis by A138,A147,A158,XXREAL_0:2;
end;
suppose
A160: upper_bound S = upper_bound(IT/.(n+1));
reconsider y1 = s as Point of L by A4,A8,XXREAL_1:1;
take y1;
IT/.(n+1) = PRAWY by A26,A82,A132,A148,A141,A160;
hence y1 in IT/.(n+1) by A70,A72,XXREAL_1:2;
let x be Point of L;
assume x in IT/.i;
then x < upper_bound(IT/.n) by A155,A156,XXREAL_0:2;
hence thesis by A140,XXREAL_0:2;
end;
end;
suppose
A161: i = n;
reconsider y1 = upper_bound(IT/.n) as Element of L by A8,A137
,A139,Th2;
take y1;
thus y1 in IT/.(n+1) by A132,A135,A147,A148,PARTFUN1:def 6;
let x be Point of L;
assume
A162: x in IT/.i;
A163: now
set IT1 = IT|Seg n;
A164: rng IT1 c= rng IT by RELAT_1:70;
rng IT1 c= bool the carrier of L
proof
let A be object;
assume A in rng IT1;
then A in rng IT by A164;
then A in X by A99;
hence thesis;
end;
then reconsider FI = rng IT1 as Subset-Family of L;
assume x = upper_bound(IT/.n);
then
A165: IT/.n = PRAWY by A26,A82,A136,A161,A162;
A166: now
union FI = the carrier of L
proof
thus union FI c= the carrier of L;
let l be object;
assume l in the carrier of L;
then reconsider l as Point of L;
per cases;
suppose
l < upper_bound(IT/.n);
then consider j being Nat such that
A167: j in dom IT and
A168: j <= n and
A169: l in IT/.j by A106,A135;
1 <= j by A167,FINSEQ_3:25;
then j in Seg n by A168,FINSEQ_1:1;
then
A170: IT.j in FI by A167,FUNCT_1:50;
IT.j = IT/.j by A167,PARTFUN1:def 6;
hence thesis by A169,A170,TARSKI:def 4;
end;
suppose
A171: l >= upper_bound(IT/.n);
n in Seg n by A142,FINSEQ_1:1;
then
A172: IT.n in FI by A135,FUNCT_1:50;
l <= s by A8,XXREAL_1:1;
then l = s by A71,A165,A171,XXREAL_0:1;
hence thesis by A72,A126,A138,A165,A172,TARSKI:def 4;
end;
end;
then
A173: FI is Cover of L by SETFAM_1:def 11;
assume
A174: FI <> X;
A175: FI c= X by A99,A164;
then FI c= G1 by A26;
then
A176: FI in ALL by A173;
then [FI,M] in R by A21,A23,A24,A175,WELLORD2:def 1;
hence contradiction by A21,A22,A24,A174,A176;
end;
Seg n c= dom IT
proof
let x be object;
A177: n+0 <= n+1 by XREAL_1:6;
assume
A178: x in Seg n;
then reconsider x as Nat;
x <= n by A178,FINSEQ_1:1;
then x <= n+1 by A177,XXREAL_0:2;
then
A179: x <= len IT by A146,XXREAL_0:2;
1 <= x by A178,FINSEQ_1:1;
hence thesis by A179,FINSEQ_3:25;
end;
then dom IT1 = Seg n by RELAT_1:62;
then card rng IT1 <= card dom IT1 & card dom IT1 = n by
CARD_2:47,FINSEQ_1:57;
then n+1 <= n+0 by A96,A146,A166,XXREAL_0:2;
hence contradiction by XREAL_1:6;
end;
x <= upper_bound(IT/.n) by A137,A161,A162,SEQ_4:def 1;
hence thesis by A163,XXREAL_0:1;
end;
end;
end;
A180: W[0];
for n holds W[n] from NAT_1:sch 2(A180,A129);
hence thesis;
end;
A181: IT is one-to-one
proof
let i, j be object such that
A182: i in dom IT & j in dom IT and
A183: IT.i = IT.j;
A184: IT/.i = IT.i & IT/.j = IT.j by A182,PARTFUN1:def 6;
assume
A185: i <> j;
reconsider i, j as Nat by A182;
per cases by A185,XXREAL_0:1;
suppose
i < j;
then ex y being Point of L st y in IT/.j & for x being Point of L
st x in IT/.i holds x < y by A127,A182;
hence thesis by A183,A184;
end;
suppose
j < i;
then ex y being Point of L st y in IT/.i & for x being Point of L
st x in IT/.j holds x < y by A127,A182;
hence thesis by A183,A184;
end;
end;
A186: for i, j being Nat st i in dom IT & j in dom IT & i <>
j holds IT/.i <> IT/.j
proof
let i, j be Nat such that
A187: i in dom IT & j in dom IT and
A188: i <> j;
IT/.i = IT.i & IT/.j = IT.j by A187,PARTFUN1:def 6;
hence thesis by A181,A187,A188;
end;
A189: for A being Subset of L st s in A & A in G1 holds A = PRAWY
proof
let A be Subset of L;
assume that
A190: s in A and
A191: A in G1;
A192: A in F & A is open by A2,A15,A191;
A193: now
assume
A194: (ex a being Real st r < a & a <= s & A = [.r,a.[)
or ex a, b being Real st r <= a & a < b & b <= s & A = ].a,b.[;
per cases by A194;
suppose
ex a being Real st r < a & a <= s & A = [.r,a.[;
hence contradiction by A190,XXREAL_1:3;
end;
suppose
ex a, b being Real st r <= a & a < b & b <= s & A = ].a,b.[;
hence contradiction by A190,XXREAL_1:4;
end;
end;
A is connected by A3,A15,A191;
then consider ak being Real such that
r <= ak and
A195: ak < s and
A196: A = ].ak,s.] by A4,A7,A190,A192,A193,Th44;
A197: A c= PRAWY
proof
lower_bound A = ak by A195,A196,Th6;
then ak in RM by A191,A196;
then
A198: pP <= ak by XXREAL_2:def 7;
let a be object;
assume
A199: a in A;
then a in [.r,s.] by A8;
then reconsider a as Real;
ak < a by A196,A199,XXREAL_1:2;
then
A200: pP < a by A198,XXREAL_0:2;
a <= s by A196,A199,XXREAL_1:2;
hence thesis by A200,XXREAL_1:2;
end;
assume A <> PRAWY;
then A c< PRAWY by A197;
then A in ZAW by A14,A68,A72,A191;
hence contradiction by A191,XBOOLE_0:def 5;
end;
take IT;
thus rng IT c= F by A88,A99;
dom IT = Seg len IT by FINSEQ_1:def 3;
then
A201: card dom IT = card X by A96,FINSEQ_1:57;
reconsider IT1 = IT as Function of dom IT,X by A99,FUNCT_2:2;
IT1 is onto by A201,A181,FINSEQ_4:63; then
A202: rng IT = X;
hence union rng IT = [.r,s.] by A8,A27;
ex Z being set st s in Z & Z in C by A28,A8,A27,TARSKI:def 4;
then PRAWY in X by A26,A189;
then consider i being object such that
A203: i in dom IT and
A204: IT.i = PRAWY by A202,FUNCT_1:def 3;
reconsider i as Element of NAT by A203;
A205: i <= len IT by A203,FINSEQ_3:25;
A206: IT/.i = IT.i by A203,PARTFUN1:def 6;
A207: 1 <= i by A203,FINSEQ_3:25;
A208: now
assume i <> len IT;
then
A209: i < len IT by A205,XXREAL_0:1;
then
A210: ex S being Element of X st S = IT.i & upper_bound S in IT.(i+1)
by A96,A98,A207;
0+1 <= i+1 & i+1 <= len IT by A209,NAT_1:13;
then
A211: i+1 in dom IT by FINSEQ_3:25;
then IT/.(i+1) = IT.(i+1) & IT/.(i+1) in G1 by A105,PARTFUN1:def 6;
then i+0 = i+1 by A71,A189,A186,A203,A204,A206,A210,A211;
hence contradiction;
end;
A212: len IT in dom IT by A100,FINSEQ_5:6;
A213: for n being Nat st 1 < n & n < len IT ex a, b being
Real st r <= a & a < b & b <= s & IT/.n = ].a,b.[
proof
let n be Nat such that
A214: 1 < n and
A215: n < len IT;
A216: n in dom IT by A214,A215,FINSEQ_3:25;
then IT.n in rng IT by FUNCT_1:def 3;
then
A217: IT/.n in rng IT by A216,PARTFUN1:def 6;
then
A218: IT/.n in X by A99;
then
A219: IT/.n in G1 & IT/.n in F by A26,A88;
A220: IT/.n is open connected Subset of L by A89,A99,A217;
per cases by A4,A7,A45,A219,A220,Th44;
suppose
ex a being Real st r < a & a <= s & IT/.n = [.r,a.[;
then consider a being Real such that
A221: r < a and
a <= s and
A222: IT/.n = [.r,a.[;
r in [.r,a.[ by A221,XXREAL_1:3;
hence thesis by A26,A55,A97,A102,A103,A186,A214,A216,A218,A222;
end;
suppose
ex a being Real st r <= a & a < s & IT/.n = ].a,s.];
then consider a being Real such that
r <= a and
A223: a < s and
A224: IT/.n = ].a,s.];
upper_bound ].a,s.] = s & s in ].a,s.] by A223,Th7,XXREAL_1:2;
hence
thesis by A26,A82,A212,A186,A204,A206,A208,A215,A216,A218,A224;
end;
suppose
ex a, b being Real st r <= a & a < b & b <= s & IT
/.n = ].a,b.[;
then consider a, b being Real such that
A225: r <= a & a < b & b <= s & IT/.n = ].a,b.[;
reconsider a, b as Real;
take a, b;
thus thesis by A225;
end;
end;
A226: now
let n be Nat such that
A227: 1 <= n;
reconsider m = n as Element of NAT by ORDINAL1:def 12;
hereby
assume n <= len IT;
then m in dom IT & IT/.n = IT.n by A227,FINSEQ_3:25,FINSEQ_4:15;
then IT/.n in rng IT by FUNCT_1:def 3;
then IT/.n in X by A99;
hence IT/.n is non empty by A45,A26;
end;
hereby
assume
A228: n+1 <= len IT;
then
A229: m < len IT by NAT_1:13;
then
A230: IT/.n = IT.n by A227,FINSEQ_4:15;
A231: m in dom IT by A227,A229,FINSEQ_3:25;
then IT/.n in rng IT by A230,FUNCT_1:def 3;
then
A232: IT/.n in X by A99;
then
A233: IT/.n in G1 by A26;
A234: IT /.n is non empty real-bounded interval Subset of REAL
by A9,A45,A16,A26,A232;
A235: ex S being Element of X st S = IT.n & upper_bound S in IT.(n+1
) by A96,A98,A227,A229;
A236: 1 < m+1 by A227,NAT_1:13;
then
A237: IT/.(m+1) = IT.(m+1) by A228,FINSEQ_4:15;
A238: n+1 in dom IT by A228,A236,FINSEQ_3:25;
then
A239: IT/.(n+1) in rng IT by A237,FUNCT_1:def 3;
then
A240: IT/.(n+1) in X by A99;
then
A241: IT/.(n+1) in G1 by A26;
n+0 < n+1 by XREAL_1:6;
then
A242: IT/.n <> IT/.(n+1) by A186,A231,A238;
A243: IT/.(n+1) is non empty real-bounded interval Subset of REAL
by A9,A45,A16,A26,A240;
IT/.(n+1) c= union X by A99,A239,ZFMISC_1:74;
then IT/.(n+1) c= [.r,s.] by A8,A27;
then
A244: IT/.(n+1) is bounded_above by XXREAL_2:43;
then
A245: upper_bound(IT/.n) <= upper_bound(IT/.(n+1)) by A235,A230,A237,
SEQ_4:def 1;
hereby
assume
A246: lower_bound(IT/.n) > lower_bound(IT/.(n+1));
upper_bound(IT/.(n+1)) = upper_bound(IT/.n) & upper_bound(IT
/.n) in IT/.n implies upper_bound(IT/.(n+1)) in IT/.(n+1) by A26,A82,A212,A186
,A204,A206,A208,A229,A231,A232;
then IT/.n c= IT/.(n+1) by A234,A243,A245,A246,Th31;
then IT/.n c< IT/.(n+1) by A242;
then IT/.n in ZAW by A14,A233,A241;
hence contradiction by A26,A232,XBOOLE_0:def 5;
end;
thus upper_bound(IT/.n) <= upper_bound(IT/.(n+1)) by A235,A230,A237
,A244,SEQ_4:def 1;
per cases by A228,XXREAL_0:1;
suppose
A247: n+1 = len IT;
then pP < upper_bound(IT/.n) by A204,A208,A235,A230,XXREAL_1:2;
hence
lower_bound(IT/.(n+1)) < upper_bound(IT/.n) by A204,A206,A208,A247
,Th6,XXREAL_1:26;
end;
suppose
n+1 < len IT;
then consider a1, b1 being Real such that
r <= a1 and
A248: a1 < b1 and
b1 <= s and
A249: IT/.(n+1) = ].a1,b1.[ by A213,A236;
a1 < upper_bound(IT/.n) by A235,A230,A237,A249,XXREAL_1:4;
hence lower_bound(IT/.(n+1)) < upper_bound(IT/.n) by A248,A249,
TOPREAL6:17;
end;
end;
end;
hereby
let n be Nat such that
A250: 1 <= n;
thus
A251: (n <= len IT implies IT/.n is non empty) & (n+1 <= len IT
implies lower_bound(IT/.n) <= lower_bound(IT/.(n+1)) & upper_bound(IT/.n) <=
upper_bound(IT/.(n+1)) & lower_bound(IT/.(n+1)) < upper_bound(IT/.n)) by A226
,A250;
reconsider m = n as Nat;
A252: n+0 < n+1 by XREAL_1:6;
then
A253: 1 < m+1 by A250,XXREAL_0:2;
assume
A254: n+2 <= len IT;
then
A255: n+1+1 <= len IT;
then
A256: m+1 < len IT by NAT_1:13;
then
A257: n+1 in dom IT by A253,FINSEQ_3:25;
then IT/.(n+1) = IT.(n+1) by PARTFUN1:def 6;
then IT/.(n+1) in rng IT by A257,FUNCT_1:def 3;
then
A258: IT/.(n+1) in X by A99;
0+1 <= n+1 by XREAL_1:6;
then
A259: upper_bound(IT/.(n+1)) <= upper_bound(IT/.(n+1+1)) by A226,A254;
assume
A260: upper_bound(IT/.n) > lower_bound(IT/.(n+2));
consider a1, b1 being Real such that
r <= a1 and
A261: a1 < b1 and
b1 <= s and
A262: IT/.(n+1) = ].a1,b1.[ by A213,A253,A256;
A263: lower_bound ].a1,b1.[ = a1 by A261,TOPREAL6:17;
A264: upper_bound ].a1,b1.[ = b1 by A261,TOPREAL6:17;
A265: IT/.(n+1) c= IT/.n \/ IT/.(n+2)
proof
let x be object;
assume
A266: x in IT/.(n+1);
then reconsider x as Real;
A267: a1 < x by A262,A266,XXREAL_1:4;
A268: x < b1 by A262,A266,XXREAL_1:4;
per cases;
suppose
A269: x < upper_bound(IT/.n);
per cases;
suppose
A270: n = 1;
then lower_bound(IT/.n) <= x by A8,A53,A97,A103,A258,A266,
XXREAL_1:1;
then x in IT/.n by A42,A54,A53,A97,A103,A269,A270,XXREAL_1:3;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A271: n <> 1;
n+0 < n+2 by XREAL_1:6;
then
A272: n < len IT by A254,XXREAL_0:2;
A273: lower_bound(IT/.n) < x by A251,A255,A262,A263,A267,NAT_1:13
,XXREAL_0:2;
1 < n by A250,A271,XXREAL_0:1;
then consider a, b being Real such that
r <= a and
A274: a < b and
b <= s and
A275: IT/.n = ].a,b.[ by A213,A272;
lower_bound(IT/.n) = a & upper_bound(IT/.n) = b by A274,A275,
TOPREAL6:17;
then x in IT/.n by A269,A275,A273,XXREAL_1:4;
hence thesis by XBOOLE_0:def 3;
end;
end;
suppose
x >= upper_bound(IT/.n);
then
A276: x > lower_bound(IT/.(n+2)) by A260,XXREAL_0:2;
per cases;
suppose
A277: len IT = n+2;
x <= s by A8,A258,A266,XXREAL_1:1;
then x in IT/.(n+2) by A69,A204,A206,A208,A276,A277,XXREAL_1:2;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A278: len IT <> n+2;
n+1 < n+2 by XREAL_1:6;
then
A279: 1 < n+2 by A253,XXREAL_0:2;
n+1+1 < len IT by A254,A278,XXREAL_0:1;
then consider a2, b2 being Real such that
r <= a2 and
A280: a2 < b2 and
b2 <= s and
A281: IT/.(n+2) = ].a2,b2.[ by A213,A279;
upper_bound ].a2,b2.[ = b2 by A280,TOPREAL6:17;
then
A282: x < b2 by A259,A262,A264,A268,A281,XXREAL_0:2;
lower_bound ].a2,b2.[ = a2 by A280,TOPREAL6:17;
then x in IT/.(n+2) by A276,A281,A282,XXREAL_1:4;
hence thesis by XBOOLE_0:def 3;
end;
end;
end;
m+1 <= m+2 by XREAL_1:6;
then 1 <= m+2 by A253,XXREAL_0:2;
then
A283: m+2 in dom IT by A254,FINSEQ_3:25;
then IT/.(n+2) = IT.(n+2) by PARTFUN1:def 6;
then IT/.(n+2) in rng IT by A283,FUNCT_1:def 3;
then
A284: IT/.(n+2) in X by A99;
m <= len IT by A252,A256,XXREAL_0:2;
then
A285: n in dom IT by A250,FINSEQ_3:25;
then IT/.n = IT.n by PARTFUN1:def 6;
then IT/.n in rng IT by A285,FUNCT_1:def 3;
then
A286: IT/.n in X by A99;
n+1 < n+2 by XREAL_1:6;
then
A287: IT/.(n+2) <> IT/.(n+1) by A186,A257,A283;
n+0 < n+1 by XREAL_1:6;
then IT/.n <> IT/.(n+1) by A186,A285,A257;
hence contradiction by A22,A24,A286,A258,A284,A287,A265,Th48;
end;
thus [.r,s.] in F implies IT = <*[.r,s.]*> by A7;
assume not [.r,s.] in F;
thus ex p being Real st r < p & p <= s & IT.1 = [.r,p.[
proof
take kL;
thus r < kL by A42,A52,Th5;
upper_bound LEWY <= upper_bound [.r,s.] by A8,SEQ_4:48;
hence kL <= s by A4,A51,JORDAN5A:19;
thus thesis by A97;
end;
thus ex p being Real st r <= p & p < s & IT.len IT = ].p,s.]
proof
take pP;
lower_bound [.r,s.] <= lower_bound PRAWY by A8,SEQ_4:47;
hence r <= pP by A4,A69,JORDAN5A:19;
thus pP < s by A67,A70,Th6;
thus thesis by A204,A208;
end;
let n be Nat such that
A288: 1 < n & n < len IT;
consider a, b being Real such that
A289: r <= a & a < b & b <= s & IT/.n = ].a,b.[ by A213,A288;
take a, b;
thus thesis by A288,A289,FINSEQ_4:15;
end;
end;
end;
theorem
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected & r <=
s & [.r,s.] in F implies <*[.r,s.]*> is IntervalCover of F
proof
assume that
A1: F is Cover of Closed-Interval-TSpace(r,s) & F is open & F is connected and
A2: r <= s & [.r,s.] in F;
set f = <*[.r,s.]*>;
A3: for n being Nat st 1 <= n holds (n <= len f implies f/.n is
non empty) & (n+1 <= len f implies lower_bound(f/.n) <= lower_bound(f/.(n+1)) &
upper_bound(f/.n) <= upper_bound(f/.(n+1)) & lower_bound(f/.(n+1)) <
upper_bound(f/.n)) & (n+2 <= len f implies upper_bound(f/.n) <= lower_bound(f/.
(n+2))) by A2,Lm3;
rng f c= F & union rng f = [.r,s.] by A2,Lm3;
hence thesis by A1,A2,A3,Def2;
end;
reserve C for IntervalCover of F;
theorem Th50:
for F being Subset-Family of Closed-Interval-TSpace(r,r), C
being IntervalCover of F holds F is Cover of Closed-Interval-TSpace(r,r) & F is
open connected implies C = <*[.r,r.]*>
proof
set L = Closed-Interval-TSpace(r,r);
let F be Subset-Family of L, C be IntervalCover of F;
assume that
A1: F is Cover of L and
A2: F is open & F is connected;
A3: [.r,r.] = {r} by XXREAL_1:17;
the carrier of L = [.r,r.] by TOPMETR:18;
then r in the carrier of L by A3,TARSKI:def 1;
then {r} in F by A1,Th46;
hence thesis by A1,A2,A3,Def2;
end;
theorem Th51:
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
& r <= s implies 1 <= len C
proof
assume that
A1: F is Cover of Closed-Interval-TSpace(r,s) & F is open & F is connected and
A2: r <= s;
assume not thesis;
then len C+1 <= 0+1 by NAT_1:13;
then
A3: C is empty by XREAL_1:6;
union rng C = [.r,s.] by A1,A2,Def2;
hence thesis by A2,A3,RELAT_1:38,XXREAL_1:1,ZFMISC_1:2;
end;
theorem Th52:
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
& r <= s & len C = 1 implies C = <*[.r,s.]*>
proof
assume that
A1: F is Cover of Closed-Interval-TSpace(r,s) & F is open & F is
connected & r <= s and
A2: len C = 1;
A3: union rng C = [.r,s.] by A1,Def2;
C is non empty by A2;
then rng C is non empty;
then 1 in dom C by FINSEQ_3:32;
then
A4: C.1 in rng C by FUNCT_1:def 3;
C.1 = [.r,s.]
proof
thus for a being object st a in C.1 holds a in [.r,s.]
by A3,A4,TARSKI:def 4;
let a be object;
A5: dom C = {1} by A2,FINSEQ_1:2,def 3;
assume a in [.r,s.];
then consider Z being set such that
A6: a in Z and
A7: Z in rng C by A3,TARSKI:def 4;
ex x being object st x in dom C & C.x = Z by A7,FUNCT_1:def 3;
hence thesis by A6,A5,TARSKI:def 1;
end;
hence thesis by A2,FINSEQ_1:40;
end;
theorem
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected & r <=
s & n in dom C & m in dom C & n < m implies lower_bound(C/.n) <= lower_bound(C
/.m)
proof
assume that
A1: F is Cover of Closed-Interval-TSpace(r,s) & F is open & F is
connected & r <= s and
A2: n in dom C and
A3: m in dom C & n < m;
defpred P[Nat] means $1 in dom C & n < $1 implies lower_bound(C/.
n) <= lower_bound(C/.$1);
A4: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A5: P[k] and
A6: k+1 in dom C and
A7: n < k+1;
per cases by A6,TOPREALA:2;
suppose
k = 0;
then n = 0 by A7,NAT_1:13;
hence thesis by A2,FINSEQ_3:24;
end;
suppose
A8: k in dom C;
A9: k+1 <= len C by A6,FINSEQ_3:25;
A10: n <= k by A7,NAT_1:13;
1 <= k by A8,FINSEQ_3:25;
then lower_bound(C/.k) <= lower_bound(C/.(k+1)) by A1,A9,Def2;
hence thesis by A5,A8,A10,XXREAL_0:1,2;
end;
end;
A11: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A11,A4);
hence thesis by A3;
end;
theorem
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected & r <=
s & n in dom C & m in dom C & n < m implies upper_bound(C/.n) <= upper_bound(C
/.m)
proof
assume that
A1: F is Cover of Closed-Interval-TSpace(r,s) & F is open & F is
connected & r <= s and
A2: n in dom C and
A3: m in dom C & n < m;
defpred P[Nat] means $1 in dom C & n < $1 implies upper_bound(C/.
n) <= upper_bound(C/.$1);
A4: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A5: P[k] and
A6: k+1 in dom C and
A7: n < k+1;
per cases by A6,TOPREALA:2;
suppose
k = 0;
then n = 0 by A7,NAT_1:13;
hence thesis by A2,FINSEQ_3:24;
end;
suppose
A8: k in dom C;
A9: k+1 <= len C by A6,FINSEQ_3:25;
A10: n <= k by A7,NAT_1:13;
1 <= k by A8,FINSEQ_3:25;
then upper_bound(C/.k) <= upper_bound(C/.(k+1)) by A1,A9,Def2;
hence thesis by A5,A8,A10,XXREAL_0:1,2;
end;
end;
A11: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A11,A4);
hence thesis by A3;
end;
theorem Th55:
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
& r <= s & 1 <= n & n+1 <= len C implies ].lower_bound(C/.(n+1)),upper_bound(C
/.n).[ is non empty
proof
assume F is Cover of Closed-Interval-TSpace(r,s) & F is open & F is
connected & r <= s & 1 <= n & n+1 <= len C;
then lower_bound(C/.(n+1)) < upper_bound(C/.n) by Def2;
hence thesis by XXREAL_1:33;
end;
theorem
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected & r <=
s implies lower_bound(C/.1) = r
proof
assume that
A1: F is Cover of Closed-Interval-TSpace(r,s) & F is open & F is connected and
A2: r <= s;
1 <= len C by A1,A2,Th51;
then
A3: C.1 = C/.1 by FINSEQ_4:15;
per cases;
suppose
[.r,s.] in F;
then C = <*[.r,s.]*> by A1,A2,Def2;
then C/.1 = [.r,s.] by FINSEQ_4:16;
hence thesis by A2,JORDAN5A:19;
end;
suppose
not [.r,s.] in F;
then ex p being Real st r < p & p <= s & C.1 = [.r,p.[ by A1,A2,Def2;
hence thesis by A3,Th4;
end;
end;
theorem Th57:
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
& r <= s implies r in C/.1
proof
assume that
A1: F is Cover of Closed-Interval-TSpace(r,s) & F is open & F is connected and
A2: r <= s;
1 <= len C by A1,A2,Th51;
then
A3: C.1 = C/.1 by FINSEQ_4:15;
per cases;
suppose
[.r,s.] in F;
then C = <*[.r,s.]*> by A1,A2,Def2;
then C/.1 = [.r,s.] by FINSEQ_4:16;
hence thesis by A2,XXREAL_1:1;
end;
suppose
not [.r,s.] in F;
then ex p being Real st r < p & p <= s & C.1 = [.r,p.[ by A1,A2,Def2;
hence thesis by A3,XXREAL_1:3;
end;
end;
theorem
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected & r <=
s implies upper_bound(C/.len C) = s
proof
assume that
A1: F is Cover of Closed-Interval-TSpace(r,s) & F is open & F is connected and
A2: r <= s;
1 <= len C by A1,A2,Th51;
then
A3: C.len C = C/.len C by FINSEQ_4:15;
per cases;
suppose
[.r,s.] in F;
then C = <*[.r,s.]*> by A1,A2,Def2;
then C/.1 = [.r,s.] & len C = 1 by FINSEQ_1:39,FINSEQ_4:16;
hence thesis by A2,JORDAN5A:19;
end;
suppose
not [.r,s.] in F;
then
ex p being Real st r <= p & p < s & C.len C = ].p,s.] by A1,A2,Def2;
hence thesis by A3,Th7;
end;
end;
theorem Th59:
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
& r <= s implies s in C/.len C
proof
assume that
A1: F is Cover of Closed-Interval-TSpace(r,s) & F is open & F is connected and
A2: r <= s;
1 <= len C by A1,A2,Th51;
then
A3: C.len C = C/.len C by FINSEQ_4:15;
per cases;
suppose
[.r,s.] in F;
then C = <*[.r,s.]*> by A1,A2,Def2;
then C/.1 = [.r,s.] & len C = 1 by FINSEQ_1:39,FINSEQ_4:16;
hence thesis by A2,XXREAL_1:1;
end;
suppose
not [.r,s.] in F;
then
ex p being Real st r <= p & p < s & C.len C = ].p,s.] by A1,A2,Def2;
hence thesis by A3,XXREAL_1:2;
end;
end;
definition
let r, s be Real;
let F be Subset-Family of Closed-Interval-TSpace(r,s), C be IntervalCover of
F such that
A1: F is Cover of Closed-Interval-TSpace(r,s) & F is open & F is
connected & r <= s;
mode IntervalCoverPts of C -> FinSequence of REAL means
:Def3:
len it = len
C + 1 & it.1 = r & it.len it = s & for n being Nat st 1 <= n & n+1 <
len it holds it.(n+1) in ].lower_bound(C/.(n+1)),upper_bound(C/.n).[;
existence
proof
set A = len C + 1;
defpred P[Nat,set] means ($1 = 1 implies $2 = r) & ($1 = A
implies $2 = s) & (2 <= $1 & $1 <= len C implies $2 in ].lower_bound(C/.$1),
upper_bound(C/.($1-1)).[);
A2: 0+1 <= len C by A1,Th51;
then
A3: 0+1 < A by XREAL_1:6;
A4: for k being Nat st k in Seg A ex x being Element of REAL st P[k,x]
proof
reconsider r, s as Element of REAL by XREAL_0:def 1;
let k be Nat;
A5: len C + 0 < A by XREAL_1:6;
assume k in Seg A;
then
A6: 1 <= k & k <= A by FINSEQ_1:1;
per cases by A6,XXREAL_0:1;
suppose
A7: k = 1;
take r;
thus thesis by A2,A7;
end;
suppose
A8: k = A;
take s;
thus thesis by A2,A5,A8;
end;
suppose that
A9: 1 < k and
A10: k < A;
A11: k-1 in NAT by A9,INT_1:5;
A12: k <= len C by A10,NAT_1:13;
1-1 < k-1 by A9,XREAL_1:14;
then 0+1 <= k-1 by A11,NAT_1:13;
then
].lower_bound(C/.(k-1+1)),upper_bound(C/.(k-1)).[ is non empty by A1
,A11,A12,Th55;
then consider x being object such that
A13: x in ].lower_bound(C/.(k-1+1)),upper_bound(C/.(k-1)).[;
reconsider x as Real by A13;
take x;
thus thesis by A9,A10,A13;
end;
end;
consider p being FinSequence of REAL such that
A14: dom p = Seg A and
A15: for k being Nat st k in Seg A holds P[k,p.k] from FINSEQ_1:sch 5(
A4);
take p;
thus
A16: len p = len C + 1 by A14,FINSEQ_1:def 3;
1 in Seg A by A3,FINSEQ_1:1;
hence p.1 = r by A15;
len p in Seg A by A3,A16,FINSEQ_1:1;
hence p.len p = s by A15,A16;
let n be Nat;
assume 1 <= n;
then
A17: 1+1 <= n+1 by XREAL_1:6;
assume
A18: n+1 < len p;
0+1 <= n+1 by XREAL_1:6;
then
A19: n+1 in Seg A by A16,A18,FINSEQ_1:1;
n+1 <= len C by A16,A18,NAT_1:13;
then p.(n+1) in ].lower_bound(C/.(n+1)),upper_bound(C/.(n+1-1)).[ by A15
,A19,A17;
hence thesis;
end;
end;
reserve G for IntervalCoverPts of C;
theorem Th60:
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
& r <= s implies 2 <= len G
proof
assume
A1: F is Cover of Closed-Interval-TSpace(r,s) & F is open & F is
connected & r <= s;
then 1 <= len C by Th51;
then 1+1 <= len C + 1 by XREAL_1:6;
hence thesis by A1,Def3;
end;
theorem Th61:
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
& r <= s & len C = 1 implies G = <*r,s*>
proof
assume that
A1: F is Cover of Closed-Interval-TSpace(r,s) & F is open & F is
connected & r <= s and
A2: len C = 1;
A3: G.1 = r by A1,Def3;
A4: len G = len C + 1 by A1,Def3;
then G.2 = s by A1,A2,Def3;
hence thesis by A2,A4,A3,FINSEQ_1:44;
end;
theorem Th62:
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
& r <= s & 1 <= n & n+1 < len G implies G.(n+1) < upper_bound(C/.n)
proof
assume F is Cover of Closed-Interval-TSpace(r,s) & F is open & F is
connected & r <= s & 1 <= n & n+1 < len G;
then G.(n+1) in ].lower_bound(C/.(n+1)),upper_bound(C/.n).[ by Def3;
hence thesis by XXREAL_1:4;
end;
theorem Th63:
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
& r <= s & 1 < n & n <= len C implies lower_bound(C/.n) < G.n
proof
set w = n-'1;
assume
A1: F is Cover of Closed-Interval-TSpace(r,s) & F is open & F is
connected & r <= s;
then
A2: len G = len C + 1 by Def3;
assume that
A3: 1 < n and
A4: n <= len C;
A5: n < len C + 1 by A4,NAT_1:13;
1-1 <= n-1 by A3,XREAL_1:9;
then
A6: w = n-1 by XREAL_0:def 2;
then n = w+1;
then 1 <= w by A3,NAT_1:13;
then G.(w+1) in ].lower_bound(C/.(w+1)),upper_bound(C/.w).[ by A1,A2,A6,A5
,Def3;
hence thesis by A6,XXREAL_1:4;
end;
theorem Th64:
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
& r <= s & 1 <= n & n < len C implies G.n <= lower_bound(C/.(n+1))
proof
assume that
A1: F is Cover of Closed-Interval-TSpace(r,s) & F is open & F is connected and
A2: r <= s;
set w = n-'1;
assume that
A3: 1 <= n and
A4: n < len C;
A5: n+1 <= len C by A4,NAT_1:13;
per cases by A3,XXREAL_0:1;
suppose
A6: n = 1;
0+1 <= n+1 by XREAL_1:6;
then
A7: C/.(n+1) is non empty by A1,A2,A5,Def2;
A8: G.1 = r by A1,A2,Def3;
A9: rng C c= F by A1,A2,Def2;
1+1 <= len C by A4,A6,NAT_1:13;
then
A10: 2 in dom C by FINSEQ_3:25;
then C.2 in rng C by FUNCT_1:def 3;
then C.2 in F by A9;
then C/.2 in F by A10,PARTFUN1:def 6;
then C/.(n+1) c= the carrier of Closed-Interval-TSpace(r,s) by A6;
then
A11: C/.(n+1) c= [.r,s.] by A2,TOPMETR:18;
then C/.(n+1) is bounded_below by XXREAL_2:44;
then lower_bound(C/.(n+1)) in [.r,s.] by A7,A11,Th1;
hence thesis by A6,A8,XXREAL_1:1;
end;
suppose
1 < n;
then
A12: 1-1 < n-1 by XREAL_1:9;
then
A13: w = n-1 by XREAL_0:def 2;
then
A14: 0+1 <= w by A12,NAT_1:13;
len G = len C + 1 by A1,A2,Def3;
then
A15: n+1 < len G - 1+1 by A4,XREAL_1:6;
n-1 < n-0 by XREAL_1:15;
then w+1 < n+1 by A13,XREAL_1:6;
then w+1 < len G by A15,XXREAL_0:2;
then
A16: G.(w+1) < upper_bound(C/.w) by A1,A2,A14,Th62;
n+1 <= len C by A4,NAT_1:13;
then upper_bound(C/.w) <= lower_bound(C/.(w+2)) by A1,A2,A13,A14,Def2;
hence thesis by A13,A16,XXREAL_0:2;
end;
end;
theorem Th65:
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
& r < s implies G is increasing
proof
assume that
A1: F is Cover of Closed-Interval-TSpace(r,s) & F is open & F is connected and
A2: r < s;
let m, n be Nat such that
A3: m in dom G & n in dom G & m < n;
defpred P[Nat] means m < $1 & m in dom G & $1 in dom G implies G.m < G.$1;
A4: for k being Nat st P[k] holds P[k+1]
proof
A5: len G = len C + 1 by A1,A2,Def3;
let k be Nat such that
A6: P[k] and
A7: m < k+1 and
A8: m in dom G and
A9: k+1 in dom G;
A10: 1 <= m by A8,FINSEQ_3:25;
A11: k+1 <= len G by A9,FINSEQ_3:25;
k+0 <= k+1 by XREAL_1:6;
then
A12: k <= len G by A11,XXREAL_0:2;
A13: m <= k by A7,NAT_1:13;
then
A14: 1 <= k by A10,XXREAL_0:2;
per cases by A14,A11,XXREAL_0:1;
suppose that
A15: 1 < k and
A16: k+1 < len G;
G.(k+1) in ].lower_bound(C/.(k+1)),upper_bound(C/.k).[ by A1,A2,A15,A16
,Def3;
then
A17: lower_bound(C/.(k+1)) < G.(k+1) by XXREAL_1:4;
k < len C by A5,A16,XREAL_1:6;
then G.k <= lower_bound(C/.(k+1)) by A1,A2,A15,Th64;
then G.k < G.(k+1) by A17,XXREAL_0:2;
hence thesis by A6,A8,A13,A12,A15,FINSEQ_3:25,XXREAL_0:1,2;
end;
suppose
A18: k = 1;
A19: 1 <= len C by A1,A2,Th51;
A20: m <= 1 by A7,A18,NAT_1:13;
per cases by A19,XXREAL_0:1;
suppose
A21: 1 < len C;
then 1+1 <= len C by NAT_1:13;
then
A22: lower_bound(C/.2) < G.2 by A1,A2,Th63;
G.1 <= lower_bound(C/.(1+1)) by A1,A2,A21,Th64;
then G.1 < G.2 by A22,XXREAL_0:2;
hence thesis by A10,A18,A20,XXREAL_0:1;
end;
suppose
1 = len C;
then G = <*r,s*> by A1,A2,Th61;
then G.1 = r & G.2 = s;
hence thesis by A2,A10,A18,A20,XXREAL_0:1;
end;
end;
suppose
A23: k+1 = len G;
then
A24: G.(k+1) = s by A1,A2,Def3;
per cases by A10,XXREAL_0:1;
suppose
A25: 1 < m;
set z = m-'1;
1-1 <= m-1 by A10,XREAL_1:9;
then
A26: z = m-1 by XREAL_0:def 2;
then
A27: z+1 < len G by A7,A23;
then
A28: z <= len C by A5,XREAL_1:6;
1+1 <= m by A25,NAT_1:13;
then
A29: 1+1-1 <= m-1 by XREAL_1:9;
then
A30: 1 <= z by XREAL_0:def 2;
then
A31: C/.z is non empty by A1,A2,A28,Def2;
A32: rng C c= F by A1,A2,Def2;
A33: z in dom C by A30,A28,FINSEQ_3:25;
then C.z in rng C by FUNCT_1:def 3;
then C.z in F by A32;
then C/.z in F by A33,PARTFUN1:def 6;
then C/.z c= the carrier of Closed-Interval-TSpace(r,s);
then
A34: C/.z c= [.r,s.] by A2,TOPMETR:18;
then C/.z is bounded_above by XXREAL_2:43;
then upper_bound(C/.z) in [.r,s.] by A34,A31,Th2;
then
A35: upper_bound(C/.z) <= s by XXREAL_1:1;
G.m < upper_bound(C/.z) by A1,A2,A26,A29,A27,Th62;
hence thesis by A24,A35,XXREAL_0:2;
end;
suppose
m = 1;
hence thesis by A1,A2,A24,Def3;
end;
end;
end;
A36: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A36,A4);
hence thesis by A3;
end;
theorem
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected & r <=
s & 1 <= n & n < len G implies [.G.n,G.(n+1).] c= C.n
proof
set L = Closed-Interval-TSpace(r,s);
assume that
A1: F is Cover of L & F is open and
A2: F is connected and
A3: r <= s and
A4: 1 <= n and
A5: n < len G;
A6: len G = len C + 1 by A1,A2,A3,Def3;
then
A7: n <= len C by A5,NAT_1:13;
then
A8: C/.n = C.n by A4,FINSEQ_4:15;
n in dom C by A4,A7,FINSEQ_3:25;
then
A9: C.n in rng C by FUNCT_1:def 3;
rng C c= F by A1,A2,A3,Def2;
then C/.n in F by A8,A9;
then C/.n is connected Subset of L by A2;
then
A10: C/.n is interval by Th43;
A11: C/.n is non empty by A1,A2,A3,A4,A7,Def2;
A12: n+1 <= len G by A5,NAT_1:13;
0+1 <= n+1 by XREAL_1:6;
then
A13: n+1 in dom G by A12,FINSEQ_3:25;
A14: n in dom G by A4,A5,FINSEQ_3:25;
A15: n+0 < n+1 by XREAL_1:6;
per cases by A3,XXREAL_0:1;
suppose
r = s;
then C = <*[.r,r.]*> by A1,A2,Th50;
then
A16: len C = 1 by FINSEQ_1:40;
then G = <*r,s*> by A1,A2,A3,Th61;
then
A17: G.1 = r & G.2 = s;
n = 1 & C = <*[.r,s.]*> by A1,A2,A3,A4,A7,A16,Th52,XXREAL_0:1;
hence thesis by A17;
end;
suppose
r < s;
then G is increasing by A1,A2,Th65;
then
A18: G.n < G.(n+1) by A14,A13,A15;
A19: 2 <= len G by A1,A2,A3,Th60;
per cases by A4,A12,A19,XXREAL_0:1;
suppose that
A20: n = 1 and
A21: len G = 2;
G = <*r,s*> by A1,A2,A3,A6,A21,Th61;
then
A22: G.1 = r & G.2 = s;
C = <*[.r,s.]*> by A1,A2,A3,A6,A21,Th52;
hence thesis by A20,A22;
end;
suppose that
A23: n = 1 and
A24: 1+1 < len G;
G.(1+1) in ].lower_bound(C/.(1+1)),upper_bound(C/.1).[ by A1,A2,A3,A24
,Def3;
then
A25: lower_bound(C/.(1+1)) < G.2 by XXREAL_1:4;
1+1 <= len C by A6,A24,NAT_1:13;
then lower_bound(C/.1) <= lower_bound(C/.(1+1)) by A1,A2,A3,Def2;
then
A26: lower_bound(C/.n) < G.(n+1) by A23,A25,XXREAL_0:2;
A27: G.1 = r & r in C/.1 by A1,A2,A3,Def3,Th57;
G.(n+1) < upper_bound(C/.n) by A1,A2,A3,A23,A24,Th62;
then G.(n+1) in C.n by A8,A10,A11,A26,Th30;
hence thesis by A8,A10,A23,A27;
end;
suppose that
A28: 1 < n and
A29: len G = n+1;
1-1 < n-1 by A28,XREAL_1:9;
then
A30: 0+1 <= n-1 & n-1 is Element of NAT by INT_1:3,7;
then G.(n-1+1) in ].lower_bound(C/.(n-1+1)),upper_bound(C/.(n-1)).[ by A1
,A2,A3,A15,A29,Def3;
then
A31: G.n < upper_bound(C/.(n-1)) by XXREAL_1:4;
upper_bound(C/.(n-1)) <= upper_bound(C/.(n-1+1)) by A1,A2,A3,A6,A29,A30
,Def2;
then
A32: G.n < upper_bound(C/.n) by A31,XXREAL_0:2;
G.len G = s by A1,A2,A3,Def3;
then
A33: G.(n+1) in C.n by A1,A2,A3,A6,A8,A29,Th59;
lower_bound(C/.n) < G.n by A1,A2,A3,A6,A28,A29,Th63;
then G.n in C.n by A8,A10,A11,A32,Th30;
hence thesis by A8,A10,A33;
end;
suppose that
A34: 1 < n and
A35: n+1 < len G;
A36: G.(n+1) < upper_bound(C/.n) by A1,A2,A3,A4,A35,Th62;
n <= len C by A5,A6,NAT_1:13;
then
A37: lower_bound(C/.n) < G.n by A1,A2,A3,A34,Th63;
then lower_bound(C/.n) < G.(n+1) by A18,XXREAL_0:2;
then
A38: G.(n+1) in C.n by A8,A10,A11,A36,Th30;
G.n < upper_bound(C/.n) by A18,A36,XXREAL_0:2;
then G.n in C.n by A8,A10,A11,A37,Th30;
hence thesis by A8,A10,A38;
end;
end;
end;