Commit 2023-08-25 09:58 2c3112d5

View on Github →

chore: golf some proofs, add helper lemmas (#6769)

Estimated changes

Modified Mathlib/MeasureTheory/Group/Measure.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem Set.Infinite.meas_eq_top

Modified Mathlib/Topology/Algebra/Group/Basic.lean

added theorem exists_isCompact_isClosed_nhds_one

added theorem exists_isCompact_isClosed_subset_isCompact_nhds_one

Modified Mathlib/Topology/CompactOpen.lean

Modified Mathlib/Topology/Paracompact.lean