Theorem liminflelimsupcex

Description: A counterexample for liminflelimsup , showing that the second hypothesis is needed. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Assertion	liminflelimsupcex	⊢ ( lim sup ‘ ∅ ) < ( lim inf ‘ ∅ )

Proof

Step	Hyp	Ref	Expression
1		mnfltpnf	⊢ -∞ < +∞
2		limsup0	⊢ ( lim sup ‘ ∅ ) = -∞
3		liminf0	⊢ ( lim inf ‘ ∅ ) = +∞
4	2 3	breq12i	⊢ ( ( lim sup ‘ ∅ ) < ( lim inf ‘ ∅ ) ↔ -∞ < +∞ )
5	1 4	mpbir	⊢ ( lim sup ‘ ∅ ) < ( lim inf ‘ ∅ )