Mathlib v3 is deprecated. Go to Mathlib v4

Theorem partition_of_unity.exists_finset_nhd_support_subset

Modification history

2022-04-01 22:20
src/topology/partition_of_unity.lean
feat(topology/support): add lemma `locally_finite.exists_finset_nhd_mul_support_subset` (#13006) …
Added partition_of_unity.exists_finset_nhd_support_subsetView on Github →