Commit 2024-04-15 07:51 5894eb31

View on Github →

refactor(Topology): take continuous argument in LocallyConstant.comap (#12136) Changes the definition of LocallyConstant.comap so that it takes an argument of the form C(X, Y) instead of X → Y. There was no example of a non-continuous argument in mathlib, and this definition generally makes proofs easier.

Estimated changes

modified theorem LocallyConstant.coe_comap
modified theorem LocallyConstant.comap_comap
modified theorem LocallyConstant.comap_comp
modified theorem LocallyConstant.comap_const
modified theorem LocallyConstant.comap_id