Mathlib v3 is deprecated. Go to Mathlib v4

Theorem locally_finite.finite_nonempty_of_compact

Modification history

2021-02-22 14:12
src/topology/subset_properties.lean
feat(topology/subset_properties): locally finite family on a compact space is finite (#6352)
Added locally_finite.finite_nonempty_of_compactView on Github →