Theorem MonoidHom.exists_nhds_isBounded

Modification history

2025-01-05 13:11
Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean
feat: if `f` is a measurable group hom, then every point has a neighborhood `s` such that `f '' s` is bounded (#20304) …
Added MonoidHom.exists_nhds_isBoundedView on Github →