Theorem ContinuousOn.continuousAt_mulIndicator

Modification history

2024-12-09 08:25

Mathlib/Topology/Algebra/Indicator.lean

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

Modified ContinuousOn.continuousAt_mulIndicator View on Github →

2024-12-05 07:37

Mathlib/Topology/ContinuousOn.lean

feat(Analysis/BoxIntegral/UnitPartition): Prove results linking integral point counting and integrals (#12405) …

Added ContinuousOn.continuousAt_mulIndicator View on Github →