Commit 2025-05-22 19:35 ebe90d28

View on Github →

chore: replace nhd with nhds (#25108)

Estimated changes

Modified Mathlib/Analysis/Meromorphic/Basic.lean

Modified Mathlib/Analysis/Meromorphic/FactorizedRational.lean

Modified Mathlib/Analysis/Meromorphic/NormalForm.lean

deleted theorem MeromorphicAt.eq_nhdNE_toMeromorphicNFAt

added theorem MeromorphicAt.eq_nhdsNE_toMeromorphicNFAt

deleted theorem MeromorphicNFAt.eventuallyEq_nhdNE_iff_eventuallyEq_nhd

added theorem MeromorphicNFAt.eventuallyEq_nhdsNE_iff_eventuallyEq_nhds

deleted theorem MeromorphicOn.toMeromorphicNFOn_eq_self_on_nhdNE

added theorem MeromorphicOn.toMeromorphicNFOn_eq_self_on_nhdsNE

deleted theorem toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhd

added theorem toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhds

Modified Mathlib/Analysis/Meromorphic/Order.lean

Modified Mathlib/Analysis/Normed/Group/Quotient.lean

deleted theorem quotient_nhd_basis

added theorem quotient_nhds_basis

Modified Mathlib/Analysis/Normed/Module/Dual.lean

modified theorem NormedSpace.isBounded_polar_of_mem_nhds_zero

Modified Mathlib/Analysis/Normed/Module/WeakDual.lean

modified theorem WeakDual.isClosed_image_polar_of_mem_nhds

modified theorem WeakDual.isCompact_polar

Modified Mathlib/Analysis/Oscillation.lean

deleted theorem oscillationWithin_nhd_eq_oscillation

added theorem oscillationWithin_nhds_eq_oscillation

Modified Mathlib/FieldTheory/Galois/Infinite.lean

Modified Mathlib/FieldTheory/KrullTopology.lean

Modified Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean

deleted theorem PartialHomeomorph.extend_image_nhd_mem_nhds_of_boundaryless

deleted theorem PartialHomeomorph.extend_image_nhd_mem_nhds_of_mem_interior_range

added theorem PartialHomeomorph.extend_image_nhds_mem_nhds_of_boundaryless

added theorem PartialHomeomorph.extend_image_nhds_mem_nhds_of_mem_interior_range

deleted theorem extChartAt_image_nhd_mem_nhds_of_boundaryless

deleted theorem extChartAt_image_nhd_mem_nhds_of_mem_interior_range

added theorem extChartAt_image_nhds_mem_nhds_of_boundaryless

added theorem extChartAt_image_nhds_mem_nhds_of_mem_interior_range

Modified Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

Modified Mathlib/MeasureTheory/Measure/DiracProba.lean

Modified Mathlib/MeasureTheory/Measure/Portmanteau.lean

Modified Mathlib/Topology/Algebra/Category/ProfiniteGrp/Limits.lean

Modified Mathlib/Topology/Algebra/ClopenNhdofOne.lean

deleted theorem IsTopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhd_of_one

added theorem IsTopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhds_of_one

deleted theorem ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhd_of_one

added theorem ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one

Modified Mathlib/Topology/Algebra/InfiniteSum/UniformOn.lean

deleted theorem hasProdLocallyUniformlyOn_of_of_forall_exists_nhd

added theorem hasProdLocallyUniformlyOn_of_of_forall_exists_nhds

deleted theorem multipliableLocallyUniformlyOn_of_of_forall_exists_nhd

added theorem multipliableLocallyUniformlyOn_of_of_forall_exists_nhds

Modified Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean

Modified Mathlib/Topology/Algebra/IsUniformGroup/Defs.lean

Modified Mathlib/Topology/Algebra/OpenSubgroup.lean

deleted theorem IsTopologicalGroup.exist_mul_closure_nhd

added theorem IsTopologicalGroup.exist_mul_closure_nhds

deleted theorem IsTopologicalGroup.exist_openSubgroup_sub_clopen_nhd_of_one

added theorem IsTopologicalGroup.exist_openSubgroup_sub_clopen_nhds_of_one

Modified Mathlib/Topology/Algebra/Support.lean

deleted theorem LocallyFinite.exists_finset_nhd_mulSupport_subset

added theorem LocallyFinite.exists_finset_nhds_mulSupport_subset

Modified Mathlib/Topology/Compactness/Compact.lean

Modified Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean

Modified Mathlib/Topology/DiscreteSubset.lean

deleted theorem nhdNE_of_nhdNE_sdiff_finite

added theorem nhdsNE_of_nhdsNE_sdiff_finite

Modified Mathlib/Topology/IndicatorConstPointwise.lean

Modified Mathlib/Topology/PartitionOfUnity.lean

deleted theorem PartitionOfUnity.exists_finset_nhd'

deleted theorem PartitionOfUnity.exists_finset_nhd

deleted theorem PartitionOfUnity.exists_finset_nhd_support_subset

added theorem PartitionOfUnity.exists_finset_nhds'

added theorem PartitionOfUnity.exists_finset_nhds

added theorem PartitionOfUnity.exists_finset_nhds_support_subset

Modified Mathlib/Topology/Separation/Hausdorff.lean

deleted theorem ContinuousAt.eventuallyEq_nhd_iff_eventuallyEq_nhdNE

added theorem ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE

Modified Mathlib/Topology/Separation/Profinite.lean

Modified Mathlib/Topology/Separation/Regular.lean

Modified Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean

deleted theorem tendstoLocallyUniformlyOn_of_forall_exists_nhd

added theorem tendstoLocallyUniformlyOn_of_forall_exists_nhds

deleted theorem tendstoLocallyUniformly_of_forall_exists_nhd

added theorem tendstoLocallyUniformly_of_forall_exists_nhds

Modified scripts/nolints_prime_decls.txt