Commit 2022-07-11 14:26 627bd0c2

View on Github →

chore(topology/basic): use finite in locally_finite_of_finite (#15181) Rename locally_finite_of_fintype to locally_finite_of_finite, use [finite] instead of [fintype].

Estimated changes

Modified src/topology/basic.lean

added theorem locally_finite_of_finite

deleted theorem locally_finite_of_fintype

Modified src/topology/paracompact.lean