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

Commit

3 years ago

feat(topology/locally_finite): add lemmas about `option _` and `sum _ _` (#15923) Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

Author

urkud

Parents