Commit 2024-01-30 06:20 42e69f03

feat(Group/Measure): reformulate exists_nhds_measure_smul_diff_lt (#10093)

• Formulate the lemma as ∀ᶠ g in 𝓝 1, _ instead of ∃ V ∈ 𝓝 1, ∀ g ∈ V, _.
• Add a version in terms of Filter.Tendsto.
• Golf Steinhaus Theorem.