Changing imports in `LocallyConstant.Basic`

Stream: mathlib4

[Dagur Asgeirsson]

Is it acceptable to change the imports of Topology/LocallyConstant/Basic.lean so that it imports Topology/Sets/Closeds.lean? I'm afraid of changing the import structure in basic files like this one. See #10390

[Matthew Ballard]

Please be sure to benchmark this

[Dagur Asgeirsson]

I'm not sure what that means

[Dagur Asgeirsson]

I guess you mean comparing the speed of mathlib before and after this import change? But how do I do that?

[Kevin Buzzard]

Type !bench as a message on GitHub

[Yury G. Kudryashov]

IMHO, the right way is to move all definitions from Topology/Sets/* to a new file without heavy dependencies, then import that file if all you need is the definition + a SetLike instance. But this can wait until another PR.

[Yury G. Kudryashov]

(it's on my TODO list)

[Dagur Asgeirsson]

!bench gave no significant changes, so I guess the cleanest solution is to change the imports in LocallyConstant/Basic, and in the future we can change it to the more basic file in Topology/Sets which Yury is suggesting