Commit 2024-09-03 07:25 d7a22491

View on Github →

feat(LocallyIntegrable): generalize locallyIntegrableOn_iff (#16324) Drop a T2Space assumption and assume IsLocallyClosed instead of IsClosed s ∨ IsOpen s.

Estimated changes

Modified Mathlib/Analysis/MellinTransform.lean

Modified Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

modified theorem MeasureTheory.locallyIntegrableOn_iff

Modified Mathlib/Topology/Basic.lean

added theorem IsClosed.isLocallyClosed

added theorem IsOpen.isLocallyClosed

Modified Mathlib/Topology/LocallyClosed.lean

deleted theorem IsClosed.isLocallyClosed

deleted theorem IsOpen.isLocallyClosed