let n be Nat; :: thesis: 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); :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum