Commit 2024-01-24 14:31 d1054e16

View on Github →

chore(Topology): remove autoImplicit from most remaining files (#9865)

Estimated changes

Modified Mathlib/Topology/Algebra/Order/Compact.lean

Modified Mathlib/Topology/Algebra/Order/Rolle.lean

Modified Mathlib/Topology/Algebra/Star.lean

Modified Mathlib/Topology/ContinuousOn.lean

modified theorem continuousWithinAt_congr_nhds

Modified Mathlib/Topology/CountableSeparatingOn.lean

Modified Mathlib/Topology/ExtremallyDisconnected.lean

Modified Mathlib/Topology/Homotopy/Basic.lean

Modified Mathlib/Topology/LocallyConstant/Algebra.lean

Modified Mathlib/Topology/Order.lean

modified theorem denseRange_discrete

Modified Mathlib/Topology/ProperMap.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean