From c5cae68a5c4cf8b31ba5d9c90ac74a27aaed4d9b Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Sat, 12 Sep 2026 01:48:07 +0000 Subject: [PATCH 1/2] feat(Analysis/Normed/Group/Basic): add mem_closedBall_iff_nnnorm --- Mathlib/Analysis/Normed/Group/Basic.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Analysis/Normed/Group/Basic.lean b/Mathlib/Analysis/Normed/Group/Basic.lean index e931315afe809c..fd9fc901d99ee8 100644 --- a/Mathlib/Analysis/Normed/Group/Basic.lean +++ b/Mathlib/Analysis/Normed/Group/Basic.lean @@ -869,6 +869,10 @@ theorem mem_closedBall_iff_norm'' : b ∈ closedBall a r ↔ ‖b / a‖ ≤ r : theorem mem_closedBall_iff_norm''' : b ∈ closedBall a r ↔ ‖a / b‖ ≤ r := by rw [mem_closedBall', dist_eq_norm_div] +@[to_additive mem_closedBall_iff_nnnorm] +theorem mem_closedBall_iff_nnnorm'' {r : ℝ≥0} : b ∈ closedBall a r ↔ ‖b / a‖₊ ≤ r := + mem_closedBall_iff_norm'' + /-- A scaled closed ball is a closed ball. -/ @[to_additive setOf_sub_mem_closedBall_eq_closedBall /-- A translated closed ball is a closed ball. -/] From 91f1dac19903185f59029451788824f8b47af6e3 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Sat, 12 Sep 2026 03:57:57 +0000 Subject: [PATCH 2/2] add mem_closedBall_iff_nnnorm' variant --- Mathlib/Analysis/Normed/Group/Basic.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Analysis/Normed/Group/Basic.lean b/Mathlib/Analysis/Normed/Group/Basic.lean index fd9fc901d99ee8..01b75c51d93158 100644 --- a/Mathlib/Analysis/Normed/Group/Basic.lean +++ b/Mathlib/Analysis/Normed/Group/Basic.lean @@ -873,6 +873,10 @@ theorem mem_closedBall_iff_norm''' : b ∈ closedBall a r ↔ ‖a / b‖ ≤ r theorem mem_closedBall_iff_nnnorm'' {r : ℝ≥0} : b ∈ closedBall a r ↔ ‖b / a‖₊ ≤ r := mem_closedBall_iff_norm'' +@[to_additive mem_closedBall_iff_nnnorm'] +theorem mem_closedBall_iff_nnnorm''' {r : ℝ≥0} : b ∈ closedBall a r ↔ ‖a / b‖₊ ≤ r := + mem_closedBall_iff_norm''' + /-- A scaled closed ball is a closed ball. -/ @[to_additive setOf_sub_mem_closedBall_eq_closedBall /-- A translated closed ball is a closed ball. -/]