[Merged by Bors] - chore(Topology/DiscreteSubset): fix typo eventualy -> eventually in lemma name

[kim-em]

This PR renames Disjoint.eventualy_nhdsWithin_specializes to Disjoint.eventually_nhdsWithin_specializes, fixing the misspelling "eventualy", and update its single (internal) use site. The lemma was merged three days ago and has not been in any release, so no deprecated alias is added.

---

Follow-up to #39353 (feat(Topology): Show existence of a neighbourhood around p which avoids all points in the support of a locally finsupp function except those which specialize to p).

🤖 Prepared with Claude Code

[github-actions]

PR summary 01737d1046

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ Disjoint.eventually_nhdsWithin_specializes
- Disjoint.eventualy_nhdsWithin_specializes

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 01737d1).

• +1 new declarations
• −1 removed declarations

+Disjoint.eventually_nhdsWithin_specializes
-Disjoint.eventualy_nhdsWithin_specializes

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 01737d1046
Reference commit a33a5ccd63

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[themathqueen]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by themathqueen.

[j-loreaux]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Test and lint
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job