Commit 2026-03-25 10:28 6ecc71f5

View on Github →

feat(Analysis/Topology): Generalize Riesz' theorem to locally compact… (#36447) … T2 topological vector spaces

Estimated changes

Modified Mathlib/Analysis/Normed/Module/FiniteDimension.lean

modified theorem FiniteDimensional.of_isCompact_closedBall

modified theorem FiniteDimensional.of_isCompact_closedBall₀

deleted theorem FiniteDimensional.of_locallyCompactSpace

deleted theorem HasCompactMulSupport.eq_one_or_finiteDimensional

deleted theorem HasCompactSupport.eq_zero_or_finiteDimensional

modified theorem ProperSpace.of_locallyCompactSpace

modified theorem ProperSpace.of_locallyCompact_module

Modified Mathlib/GroupTheory/GroupAction/SubMulAction.lean

added theorem SetLike.smul_subset_self

added theorem SetLike.units_smul

Modified Mathlib/Topology/Algebra/Module/FiniteDimension.lean

added theorem FiniteDimensional.of_exists_totallyBounded_nhds

added theorem FiniteDimensional.of_locallyCompactSpace

added theorem FiniteDimensional.of_totallyBounded_nhds

added theorem FiniteDimensional.of_totallyBounded_nhds_zero

added theorem HasCompactMulSupport.eq_one_or_finiteDimensional

added theorem HasCompactSupport.eq_zero_or_finiteDimensional