Commit 2026-09-02 10:15 ed25ae5a

View on Github →

chore(Topology/LocallyClosed): fix names (#43310) When adapting my PR adding IsLocallyClosedAt to Yaël's refactor for eventual equality of sets, I forgot to follow the new naming convention. This PR was automatically created from PR #42501 by @ADedecker via a review comment by @ADedecker.

Estimated changes

Modified Mathlib/Topology/LocallyClosed.lean

deleted theorem isLocallyClosedAt_iff_closure_eventuallyLE

added theorem isLocallyClosedAt_iff_closure_eventuallySubset

added theorem isLocallyClosedAt_iff_eventuallyEqSet_closure

deleted theorem isLocallyClosedAt_iff_eventuallyEq_closure

deleted theorem isLocallyClosedAt_iff_exists_isClosed_eventuallyEq

added theorem isLocallyClosedAt_iff_exists_isClosed_eventuallyEqSet