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	$$⊢\mathrm{lim\; sup}\left(\varnothing \right)<\mathrm{lim\; inf}\left(\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		mnfltpnf	$$⊢\mathrm{-\infty }<\mathrm{+\infty }$$
2		limsup0	$$⊢\mathrm{lim\; sup}\left(\varnothing \right)=\mathrm{-\infty }$$
3		liminf0	$$⊢\mathrm{lim\; inf}\left(\varnothing \right)=\mathrm{+\infty }$$
4	2 3	breq12i	$$⊢\mathrm{lim\; sup}\left(\varnothing \right)<\mathrm{lim\; inf}\left(\varnothing \right)\leftrightarrow \mathrm{-\infty }<\mathrm{+\infty }$$
5	1 4	mpbir	$$⊢\mathrm{lim\; sup}\left(\varnothing \right)<\mathrm{lim\; inf}\left(\varnothing \right)$$