:: Properties of Connected Subsets of the Real Line
:: by Artur Korni{\l}owicz
::
:: Received February 22, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, SUBSET_1, 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;
begin :: Preliminaries
registration
let X be non empty set;
cluster [#]X -> non empty;
end;
registration
cluster -> real-membered for SubSpace of RealSpace;
end;
theorem :: RCOMP_3:1
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;
theorem :: RCOMP_3:2
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;
theorem :: RCOMP_3:3
for X, Y being Subset of REAL holds Cl(X \/ Y) = Cl X \/ Cl Y;
begin :: Intervals
reserve a, b, r, s for Real;
registration
let r be Real, s be ExtReal;
cluster [.r,s.[ -> bounded_below;
cluster ].s,r.] -> bounded_above;
end;
registration
let r, s;
cluster [.r,s.[ -> real-bounded;
cluster ].r,s.] -> real-bounded;
cluster ].r,s.[ -> real-bounded;
end;
registration
cluster open real-bounded interval non empty for Subset of REAL;
end;
theorem :: RCOMP_3:4
r < s implies lower_bound [.r,s.[ = r;
theorem :: RCOMP_3:5
r < s implies upper_bound [.r,s.[ = s;
theorem :: RCOMP_3:6
r < s implies lower_bound ].r,s.] = r;
theorem :: RCOMP_3:7
r < s implies upper_bound ].r,s.] = s;
begin :: Halflines
theorem :: RCOMP_3:8
a <= b implies [.a,b.] /\ (left_closed_halfline(a) \/
right_closed_halfline(b)) = {a,b};
registration
let a;
cluster left_closed_halfline(a) -> non bounded_below bounded_above interval;
cluster left_open_halfline(a) -> non bounded_below bounded_above interval;
cluster right_closed_halfline(a) -> bounded_below non bounded_above interval;
cluster right_open_halfline(a) -> bounded_below non bounded_above interval;
end;
theorem :: RCOMP_3:9
upper_bound left_closed_halfline(a) = a;
theorem :: RCOMP_3:10
upper_bound left_open_halfline(a) = a;
theorem :: RCOMP_3:11
lower_bound right_closed_halfline(a) = a;
theorem :: RCOMP_3:12
lower_bound right_open_halfline(a) = a;
begin :: Connectedness
registration
cluster [#]REAL -> interval non bounded_below non bounded_above;
end;
theorem :: RCOMP_3:13
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.];
theorem :: RCOMP_3:14
for X being real-bounded Subset of REAL st not lower_bound X in X
holds X c= ].lower_bound X,upper_bound X.];
theorem :: RCOMP_3:15
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.];
theorem :: RCOMP_3:16
for X being real-bounded Subset of REAL st not upper_bound X in X
holds X c= [.lower_bound X,upper_bound X.[;
theorem :: RCOMP_3:17
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.[;
theorem :: RCOMP_3:18
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.[;
theorem :: RCOMP_3:19
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.[;
theorem :: RCOMP_3:20
for X being Subset of REAL st X is bounded_above holds X c=
left_closed_halfline(upper_bound X);
theorem :: RCOMP_3:21
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);
theorem :: RCOMP_3:22
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);
theorem :: RCOMP_3:23
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);
theorem :: RCOMP_3:24
for X being Subset of REAL st X is bounded_below holds X c=
right_closed_halfline(lower_bound X);
theorem :: RCOMP_3:25
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);
theorem :: RCOMP_3:26
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);
theorem :: RCOMP_3:27
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);
theorem :: RCOMP_3:28
for X being interval Subset of REAL st X is not bounded_above &
X is not bounded_below holds X = REAL;
theorem :: RCOMP_3:29
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.[;
theorem :: RCOMP_3:30
for X being non empty interval Subset of REAL st not r in X
holds r <= lower_bound X or upper_bound X <= r;
theorem :: RCOMP_3:31
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;
registration
cluster open closed interval non empty non real-bounded for Subset of REAL;
end;
begin :: R^1
theorem :: RCOMP_3:32
for X being Subset of R^1 st a <= b & X = [.a,b.] holds Fr X = { a,b};
theorem :: RCOMP_3:33
for X being Subset of R^1 st a < b & X = ].a,b.[ holds Fr X = {a,b};
theorem :: RCOMP_3:34
for X being Subset of R^1 st a < b & X = [.a,b.[ holds Fr X = {a ,b};
theorem :: RCOMP_3:35
for X being Subset of R^1 st a < b & X = ].a,b.] holds Fr X = {a ,b};
theorem :: RCOMP_3:36
for X being Subset of R^1 st X = [.a,b.] holds Int X = ].a,b.[;
theorem :: RCOMP_3:37
for X being Subset of R^1 st X = ].a,b.[ holds Int X = ].a,b.[;
theorem :: RCOMP_3:38
for X being Subset of R^1 st X = [.a,b.[ holds Int X = ].a,b.[;
theorem :: RCOMP_3:39
for X being Subset of R^1 st X = ].a,b.] holds Int X = ].a,b.[;
registration let T be real-membered TopStruct, X be interval Subset of T;
cluster T|X -> interval;
end;
registration
let A be interval Subset of REAL;
cluster R^1(A) -> interval;
end;
registration
cluster connected -> interval for Subset of R^1;
cluster interval -> connected for Subset of R^1;
end;
begin :: Closed Interval TSpace
registration
let r;
cluster Closed-Interval-TSpace(r,r) -> 1-element;
end;
theorem :: RCOMP_3:40
r <= s implies for A being Subset of Closed-Interval-TSpace(r,s) holds
A is real-bounded Subset of REAL;
theorem :: RCOMP_3:41
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.[;
theorem :: RCOMP_3:42
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.[;
theorem :: RCOMP_3:43
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;
registration
let T be TopSpace;
cluster open closed connected for Subset of T;
end;
registration
let T be non empty connected TopSpace;
cluster non empty open closed connected for Subset of T;
end;
theorem :: RCOMP_3:44
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.[;
begin
theorem :: RCOMP_3:45
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;
theorem :: RCOMP_3:46
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;
definition
let T be TopStruct, F be Subset-Family of T;
attr F is connected means
:: RCOMP_3:def 1
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;
end;
reserve n, m for Nat,
F for Subset-Family of Closed-Interval-TSpace (r,s);
theorem :: RCOMP_3:47
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;
theorem :: RCOMP_3:48
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;
registration let X be Subset-Family of REAL;
cluster -> real-membered for Element of X;
end;
definition
let r, s be Real;
let F be Subset-Family of Closed-Interval-TSpace(r,s) such that
F is Cover of Closed-Interval-TSpace(r,s) and
F is open and
F is connected and
r <= s;
mode IntervalCover of F -> FinSequence of bool REAL means
:: RCOMP_3:def 2
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.[ );
end;
theorem :: RCOMP_3:49
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;
reserve C for IntervalCover of F;
theorem :: RCOMP_3:50
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.]*>;
theorem :: RCOMP_3:51
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
& r <= s implies 1 <= len C;
theorem :: RCOMP_3:52
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
& r <= s & len C = 1 implies C = <*[.r,s.]*>;
theorem :: RCOMP_3:53
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);
theorem :: RCOMP_3:54
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);
theorem :: RCOMP_3:55
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;
theorem :: RCOMP_3:56
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected & r <=
s implies lower_bound(C/.1) = r;
theorem :: RCOMP_3:57
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
& r <= s implies r in C/.1;
theorem :: RCOMP_3:58
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected & r <=
s implies upper_bound(C/.len C) = s;
theorem :: RCOMP_3:59
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
& r <= s implies s in C/.len C;
definition
let r, s be Real;
let F be Subset-Family of Closed-Interval-TSpace(r,s), C be IntervalCover of
F such that
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
:: RCOMP_3:def 3
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).[;
end;
reserve G for IntervalCoverPts of C;
theorem :: RCOMP_3:60
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
& r <= s implies 2 <= len G;
theorem :: RCOMP_3:61
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
& r <= s & len C = 1 implies G = <*r,s*>;
theorem :: RCOMP_3:62
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);
theorem :: RCOMP_3:63
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;
theorem :: RCOMP_3:64
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));
theorem :: RCOMP_3:65
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected
& r < s implies G is increasing;
theorem :: RCOMP_3:66
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;