Metamath Proof Explorer


Theorem liminfltlimsupex

Description: An example where the liminf is strictly smaller than the limsup . (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypothesis liminfltlimsupex.1 F=nif2n01
Assertion liminfltlimsupex lim infF<lim supF

Proof

Step Hyp Ref Expression
1 liminfltlimsupex.1 F=nif2n01
2 0lt1 0<1
3 1 liminf10ex lim infF=0
4 1 limsup10ex lim supF=1
5 3 4 breq12i lim infF<lim supF0<1
6 2 5 mpbir lim infF<lim supF