Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-12-09 10:21
b20b0dd8
View on Github →
feat: Continuity of an indicator function (
#8918
) From PFR
Estimated changes
Modified
Mathlib/Topology/ContinuousOn.lean
added
theorem
continuous_mulIndicator