Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-05 21:07 7952bc6d

View on Github →

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

Estimated changes

Modified src/data/set/basic.lean

added theorem set.image_preimage_inl_union_image_preimage_inr

Modified src/data/set/finite.lean

added theorem set.finite_preimage_inl_and_inr

Modified src/topology/locally_finite.lean

added theorem equiv.locally_finite_comp_iff

modified theorem locally_finite.comp_injective

deleted theorem locally_finite.eventually_finite

added theorem locally_finite.option_elim

modified theorem locally_finite.sum_elim

added theorem locally_finite_iff_small_sets

added theorem locally_finite_option

added theorem locally_finite_sum