Description: The closed-below, open-above interval function's value is empty outside of its domain. (Contributed by Glauco Siliprandi, 2-Jan-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | ndmico | |- ( -. ( A e. RR* /\ B e. RR* ) -> ( A [,) B ) = (/) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmico | |- dom [,) = ( RR* X. RR* ) |
|
2 | 1 | ndmov | |- ( -. ( A e. RR* /\ B e. RR* ) -> ( A [,) B ) = (/) ) |