Commit 2026-03-20 14:17 53875fe3

View on Github →

chore: replace continuity -> fun_prop in remaining auto-parameters (#35273) Resurrected version of #13994. Let's look at the current fall-out and performance effect.

Estimated changes

Modified Mathlib/Analysis/Convex/PathConnected.lean

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

Modified Mathlib/Analysis/LocallyConvex/WeakSpace.lean

Modified Mathlib/Analysis/Normed/Operator/Basic.lean

Modified Mathlib/Analysis/RCLike/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Arcosh.lean

Modified Mathlib/Topology/Algebra/Algebra.lean

modified def ContinuousAlgHom.toContinuousLinearMap

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

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

Modified Mathlib/Topology/Algebra/Module/Equiv.lean

Modified Mathlib/Topology/Algebra/Module/LinearMap.lean

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

Modified Mathlib/Topology/Category/Profinite/CofilteredLimit.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Products.lean

Modified Mathlib/Topology/Category/TopCat/ULift.lean

Modified Mathlib/Topology/ContinuousMap/Basic.lean

Modified Mathlib/Topology/ContinuousMap/Defs.lean

Modified Mathlib/Topology/FiberPartition.lean