Commit 2025-08-30 17:38 c20f6c51

View on Github →

feat(Algebra/Order/Group/Pointwise/Interval): rename Set.mapsTo' to Set.mapsTo_iff_image_subset (#27551)

Estimated changes

Modified Counterexamples/AharoniKorman.lean

Modified Mathlib/Analysis/Analytic/Composition.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Basic.lean

Modified Mathlib/Analysis/Calculus/TangentCone.lean

Modified Mathlib/Analysis/Convex/Basic.lean

Modified Mathlib/Analysis/Convex/Extrema.lean

Modified Mathlib/Analysis/Convex/Segment.lean

Modified Mathlib/Analysis/LocallyConvex/Bounded.lean

Modified Mathlib/CategoryTheory/CofilteredSystem.lean

Modified Mathlib/Data/Set/Finite/Basic.lean

Modified Mathlib/Data/Set/Function.lean

deleted theorem Set.mapsTo'

added theorem Set.mapsTo_iff_image_subset

Modified Mathlib/Dynamics/Flow.lean

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

Modified Mathlib/Order/CompleteSublattice.lean

Modified Mathlib/Topology/CWComplex/Classical/Basic.lean

Modified Mathlib/Topology/CWComplex/Classical/Finite.lean

Modified Mathlib/Topology/CompactOpen.lean

Modified Mathlib/Topology/Connected/Basic.lean

Modified Mathlib/Topology/ContinuousMap/SecondCountableSpace.lean

Modified Mathlib/Topology/Maps/Basic.lean

Modified Mathlib/Topology/PartialHomeomorph.lean

Modified scripts/nolints_prime_decls.txt