Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-22 14:12 590442ad

View on Github →

feat(topology/subset_properties): locally finite family on a compact space is finite (#6352)

Estimated changes

Modified src/data/set/finite.lean

deleted def set.fintype_of_univ_finite

Modified src/topology/basic.lean

deleted theorem locally_finite_of_finite

added theorem locally_finite_of_fintype

Modified src/topology/subset_properties.lean

added theorem finite_cover_nhds

added theorem finite_cover_nhds_interior

added theorem locally_finite.finite_nonempty_of_compact

added theorem locally_finite.finite_of_compact