Mathlib v3 is deprecated. Go to Mathlib v4

Theorem locally_finite_sum

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_sum View on Github →