Description: The supremum of the empty set is strictly smaller than the infimum of the empty set. (Contributed by Glauco Siliprandi, 2-Jan-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | supxrltinfxr | |- sup ( (/) , RR* , < ) < inf ( (/) , RR* , < ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mnfltpnf | |- -oo < +oo |
|
2 | xrsup0 | |- sup ( (/) , RR* , < ) = -oo |
|
3 | xrinf0 | |- inf ( (/) , RR* , < ) = +oo |
|
4 | 1 2 3 | 3brtr4i | |- sup ( (/) , RR* , < ) < inf ( (/) , RR* , < ) |