Mathlib v3 is deprecated. Go to Mathlib v4

Theorem locally_finite.option_elim

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