Theorem continuous_mulIndicator

Modification history

2024-12-09 08:25

Mathlib/Topology/Algebra/Indicator.lean

chore: don't import `Set.indicator` in `Topology.ContinuousOn` (#19653) …

Modified continuous_mulIndicator View on Github →

2023-12-09 10:21

Mathlib/Topology/ContinuousOn.lean

feat: Continuity of an indicator function (#8918) …

Added continuous_mulIndicator View on Github →