Commit 2025-03-20 14:16 aec06ab8

View on Github →

chore(Topology): continuity -> fun_prop (#23136)

Estimated changes

Modified Mathlib/Dynamics/Flow.lean

Modified Mathlib/Topology/Algebra/Monoid.lean

Modified Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean

Modified Mathlib/Topology/ExtremallyDisconnected.lean

Modified Mathlib/Topology/Homotopy/Basic.lean

Modified Mathlib/Topology/Homotopy/HomotopyGroup.lean

Modified Mathlib/Topology/MetricSpace/Perfect.lean