Description: The infimum regarding an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | inf00 | ⊢ inf ( 𝐵 , ∅ , 𝑅 ) = ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-inf | ⊢ inf ( 𝐵 , ∅ , 𝑅 ) = sup ( 𝐵 , ∅ , ◡ 𝑅 ) | |
2 | sup00 | ⊢ sup ( 𝐵 , ∅ , ◡ 𝑅 ) = ∅ | |
3 | 1 2 | eqtri | ⊢ inf ( 𝐵 , ∅ , 𝑅 ) = ∅ |