Description: The superior limit is greater than or equal to the inferior limit. The second hypothesis is needed (see liminflelimsupcex for a counterexample). The inequality can be strict, see liminfltlimsupex . (Contributed by Glauco Siliprandi, 2-Jan-2022)
Ref | Expression | ||
---|---|---|---|
Hypotheses | liminflelimsup.1 | |
|
liminflelimsup.2 | |
||
Assertion | liminflelimsup | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | liminflelimsup.1 | |
|
2 | liminflelimsup.2 | |
|
3 | oveq1 | |
|
4 | 3 | rexeqdv | |
5 | oveq1 | |
|
6 | 5 | imaeq2d | |
7 | 6 | ineq1d | |
8 | 7 | neeq1d | |
9 | 8 | cbvrexvw | |
10 | 9 | a1i | |
11 | 4 10 | bitrd | |
12 | 11 | cbvralvw | |
13 | 2 12 | sylib | |
14 | 1 13 | liminflelimsuplem | |