let n be Element of 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 Element of 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 Element of 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 Element of NAT holds S . i c= P ) implies Lim_inf S is Bounded )
assume that
A1: P is Bounded and
A2: for i being Element of NAT holds S . i c= P ; :: thesis: Lim_inf S is Bounded
assume A3: not Lim_inf S is Bounded ; :: thesis: contradiction
reconsider P' = P as bounded Subset of (Euclid n) by A1, JORDAN2C:def 2;
consider t being Real, z being Point of (Euclid n) such that
A4: ( 0 < t & P' c= Ball z,t ) by METRIC_6:def 10;
set r = 1;
set R = (1 + 1) + (3 * t);
consider x, y being Point of (Euclid n) such that
A5: ( x in Lim_inf S & y in Lim_inf S & dist x,y > (1 + 1) + (3 * t) ) by A3, Th38, A4;
consider k1 being Element of NAT such that
A6: for m being Element of NAT st m > k1 holds
S . m meets Ball x,1 by A5, Th50;
consider k2 being Element of NAT such that
A7: for m being Element of NAT st m > k2 holds
S . m meets Ball y,1 by A5, Th50;
set k = (max k1,k2) + 1;
S . ((max k1,k2) + 1) c= P' by A2;
then A8: S . ((max k1,k2) + 1) c= Ball z,t by A4, XBOOLE_1:1;
max k1,k2 >= k1 by XXREAL_0:25;
then (max k1,k2) + 1 > k1 by NAT_1:13;
then A9: Ball z,t meets Ball x,1 by A6, A8, XBOOLE_1:63;
max k1,k2 >= k2 by XXREAL_0:25;
then (max k1,k2) + 1 > k2 by NAT_1:13;
then A10: Ball z,t meets Ball y,1 by A7, A8, XBOOLE_1:63;
2 * t < 3 * t by A4, XREAL_1:70;
then (1 + 1) + (2 * t) < (1 + 1) + (3 * t) by XREAL_1:10;
hence contradiction by A5, A9, A10, Th40, XXREAL_0:2; :: thesis: verum