Commit 2022-07-26 11:31 b08c7ace

View on Github →

chore(topology/locally_finite): move from topology.basic (#15640) Create a new file about locally_finite, move the definition and some lemmas from topology.basic.

Estimated changes

Modified src/topology/basic.lean

deleted theorem locally_finite.Inter_compl_mem_nhds

deleted theorem locally_finite.closure

deleted theorem locally_finite.closure_Union

deleted theorem locally_finite.comp_inj_on

deleted theorem locally_finite.comp_injective

deleted theorem locally_finite.eventually_finite

deleted theorem locally_finite.exists_forall_eventually_at_top_eventually_eq'

deleted theorem locally_finite.exists_forall_eventually_at_top_eventually_eq

deleted theorem locally_finite.exists_forall_eventually_eq_prod

deleted theorem locally_finite.exists_mem_basis

deleted theorem locally_finite.is_closed_Union

deleted theorem locally_finite.point_finite

deleted theorem locally_finite.preimage_continuous

deleted theorem locally_finite.subset

deleted theorem locally_finite.sum_elim

deleted def locally_finite

deleted theorem locally_finite_of_finite

Modified src/topology/constructions.lean

Created src/topology/locally_finite.lean

added theorem locally_finite.Inter_compl_mem_nhds

added theorem locally_finite.closure_Union

added theorem locally_finite.comp_inj_on

added theorem locally_finite.comp_injective

added theorem locally_finite.eventually_finite

added theorem locally_finite.exists_forall_eventually_at_top_eventually_eq'

added theorem locally_finite.exists_forall_eventually_at_top_eventually_eq

added theorem locally_finite.exists_forall_eventually_eq_prod

added theorem locally_finite.exists_mem_basis

added theorem locally_finite.is_closed_Union

added theorem locally_finite.point_finite

added theorem locally_finite.preimage_continuous

added theorem locally_finite.sum_elim

added def locally_finite

added theorem locally_finite_of_finite