Mathlib v3 is deprecated. Go to Mathlib v4

Theorem locally_finite_iff_small_sets

Modification history

2022-10-05 21:07

src/topology/locally_finite.lean

feat(topology/locally_finite): add lemmas about `option _` and `sum _ _` (#15923)

Added locally_finite_iff_small_sets View on Github →