Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_empty_function

Modification history

2022-05-29 17:50
src/topology/order.lean
feat(topology/vector_bundle): the pullback of a vector bundle is a vector bundle (#8545) …
Added continuous_empty_functionView on Github →