Mathlib v3 is deprecated. Go to Mathlib v4

Def partition_of_unity.is_subordinate

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) …
Modified partition_of_unity.is_subordinateView on Github →
2021-08-06 09:28
src/topology/partition_of_unity.lean
feat(topology,geometry/manifold): continuous and smooth partition of unity (#8281) …
Added partition_of_unity.is_subordinateView on Github →