Commit 2023-01-27 14:08 8b474487

View on Github →

feat: port Topology.LocallyFinite (#1877)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/LocallyFinite.lean

added theorem Equiv.locallyFinite_comp_iff

added theorem LocallyFinite.closure_unionᵢ

added theorem LocallyFinite.comp_injOn

added theorem LocallyFinite.comp_injective

added theorem LocallyFinite.exists_forall_eventually_atTop_eventuallyEq

added theorem LocallyFinite.exists_forall_eventually_atTop_eventually_eq'

added theorem LocallyFinite.exists_forall_eventually_eq_prod

added theorem LocallyFinite.exists_mem_basis

added theorem LocallyFinite.interᵢ_compl_mem_nhds

added theorem LocallyFinite.isClosed_unionᵢ

added theorem LocallyFinite.option_elim'

added theorem LocallyFinite.point_finite

added theorem LocallyFinite.preimage_continuous

added theorem LocallyFinite.sum_elim

added def LocallyFinite

added theorem locallyFinite_iff_smallSets

added theorem locallyFinite_of_finite

added theorem locallyFinite_option

added theorem locallyFinite_sum