Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-22 18:31 c2719adf

View on Github →

feat(topology/basic): sum.elim of locally finite set families is locally finite (#14826)

Estimated changes

Modified src/order/filter/small_sets.lean

added theorem filter.frequently_small_sets

added theorem filter.frequently_small_sets_mem

Modified src/topology/basic.lean

added theorem locally_finite.eventually_finite

added theorem locally_finite.preimage_continuous

added theorem locally_finite.sum_elim