Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_map.nnnorm_lt_iff_of_nonempty

Modification history

2022-09-30 06:01
src/topology/continuous_function/compact.lean
feat(topology/continuous_function/{basic, compact}): add a few missing lemmas (#16714)
Added continuous_map.nnnorm_lt_iff_of_nonemptyView on Github →