Commit 2024-01-18 12:30 b105bcd5

View on Github →

feat(Topology/Support): add locallyFinite_mulSupport_iff (#9779) From sphere-eversion; I'm just upstreaming it.

Estimated changes

Modified Mathlib/Topology/Support.lean

modified theorem LocallyFinite.exists_finset_nhd_mulSupport_subset

added theorem locallyFinite_mulSupport_iff