Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.frequently_small_sets

Modification history

2022-06-22 18:31

src/order/filter/small_sets.lean

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

Added filter.frequently_small_sets View on Github →