let n be Nat; for S being SetSequence of the carrier of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st P is bounded & ( for i being Nat holds S . i c= P ) holds
Lim_inf S is bounded
let S be SetSequence of the carrier of (TOP-REAL n); for P being Subset of (TOP-REAL n) st P is bounded & ( for i being Nat holds S . i c= P ) holds
Lim_inf S is bounded
let P be Subset of (TOP-REAL n); ( P is bounded & ( for i being Nat holds S . i c= P ) implies Lim_inf S is bounded )
assume that
A1:
P is bounded
and
A2:
for i being Nat holds S . i c= P
; Lim_inf S is bounded
reconsider P9 = P as bounded Subset of (Euclid n) by A1, JORDAN2C:11;
consider t being Real, z being Point of (Euclid n) such that
A3:
0 < t
and
A4:
P9 c= Ball (z,t)
by METRIC_6:def 3;
set r = 1;
set R = (1 + 1) + (3 * t);
assume
not Lim_inf S is bounded
; contradiction
then consider x, y being Point of (Euclid n) such that
A5:
x in Lim_inf S
and
A6:
y in Lim_inf S
and
A7:
dist (x,y) > (1 + 1) + (3 * t)
by A3, Th8;
consider k1 being Nat such that
A8:
for m being Nat st m > k1 holds
S . m meets Ball (x,1)
by A5, Th14;
consider k2 being Nat such that
A9:
for m being Nat st m > k2 holds
S . m meets Ball (y,1)
by A6, Th14;
set k = (max (k1,k2)) + 1;
S . ((max (k1,k2)) + 1) c= P9
by A2;
then A10:
S . ((max (k1,k2)) + 1) c= Ball (z,t)
by A4;
2 * t < 3 * t
by A3, XREAL_1:68;
then A11:
(1 + 1) + (2 * t) < (1 + 1) + (3 * t)
by XREAL_1:8;
max (k1,k2) >= k2
by XXREAL_0:25;
then
(max (k1,k2)) + 1 > k2
by NAT_1:13;
then A12:
Ball (z,t) meets Ball (y,1)
by A9, A10, XBOOLE_1:63;
max (k1,k2) >= k1
by XXREAL_0:25;
then
(max (k1,k2)) + 1 > k1
by NAT_1:13;
then
Ball (z,t) meets Ball (x,1)
by A8, A10, XBOOLE_1:63;
hence
contradiction
by A7, A12, A11, Th10, XXREAL_0:2; verum