Commit 2024-10-18 10:35 cbaeaf5e

View on Github →

chore(Topology): deprecate Homeomorph.toContinuousMap (#17714) Use _root_.toContinuousMap instead.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Content.lean

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

Modified Mathlib/Topology/ContinuousMap/Algebra.lean

Modified Mathlib/Topology/ContinuousMap/Basic.lean

deleted def Homeomorph.toContinuousMap

Modified Mathlib/Topology/ContinuousMap/Compact.lean

Modified Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean

Modified Mathlib/Topology/ContinuousMap/Defs.lean

Modified Mathlib/Topology/ContinuousMap/Polynomial.lean

Modified Mathlib/Topology/ContinuousMap/Weierstrass.lean

Modified Mathlib/Topology/Homotopy/HomotopyGroup.lean

Modified Mathlib/Topology/Sets/Opens.lean