Commit 2024-06-30 22:15 c64a8cc6

View on Github →

chore(Topology): remove all but one use of autoImplicit (#14298) And remove superfluous open's in Order/ExtendFrom.

Estimated changes

Modified Mathlib/Topology/Algebra/ConstMulAction.lean

modified theorem isClosed_setOf_map_smul

Modified Mathlib/Topology/Category/Stonean/Limits.lean

Modified Mathlib/Topology/Order/ExtendFrom.lean

Modified Mathlib/Topology/Sheaves/Presheaf.lean

modified theorem TopCat.Presheaf.comp_app

modified theorem TopCat.Presheaf.ext