Commit 2024-12-09 08:25 bde99e32

View on Github →

chore: don't import Set.indicator in Topology.ContinuousOn (#19653) This is a first step towards not depending on algebra in basic topology

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Indicator.lean

added theorem ContinuousOn.continuousAt_mulIndicator

added theorem continuous_mulIndicator

Modified Mathlib/Topology/ContinuousMap/Bounded/Basic.lean

Modified Mathlib/Topology/ContinuousOn.lean

deleted theorem ContinuousOn.continuousAt_mulIndicator

deleted theorem continuous_mulIndicator

Modified Mathlib/Topology/IndicatorConstPointwise.lean

Modified Mathlib/Topology/Order/LeftRight.lean

Modified Mathlib/Topology/Separation/Basic.lean