Loogle!

Result

Found 605 declarations mentioning Metric.closedBall. Of these, only the first 200 are shown.

• Metric.closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α
• Metric.ball_subset_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.ball x ε ⊆ Metric.closedBall x ε
• Metric.sphere_subset_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.sphere x ε ⊆ Metric.closedBall x ε
• Metric.iUnion_closedBall_nat 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) : ⋃ n, Metric.closedBall x ↑n = Set.univ
• Real.closedBall_zero_eq_Icc 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  (r : ℝ) : Metric.closedBall 0 r = Set.Icc (-r) r
• Metric.nonempty_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : (Metric.closedBall x ε).Nonempty ↔ 0 ≤ ε
• Metric.closedBall_subset_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε₁ ε₂ : ℝ} (h : ε₁ < ε₂) : Metric.closedBall x ε₁ ⊆ Metric.ball x ε₂
• Metric.closedBall_subset_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε₁ ε₂ : ℝ} (h : ε₁ ≤ ε₂) : Metric.closedBall x ε₁ ⊆ Metric.closedBall x ε₂
• Metric.ball_subset_interior_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.ball x ε ⊆ interior (Metric.closedBall x ε)
• Metric.mem_closedBall_self 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (h : 0 ≤ ε) : x ∈ Metric.closedBall x ε
• Metric.ball_union_sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.ball x ε ∪ Metric.sphere x ε = Metric.closedBall x ε
• Metric.closedBall_diff_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.closedBall x ε \ Metric.ball x ε = Metric.sphere x ε
• Metric.closedBall_diff_sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.closedBall x ε \ Metric.sphere x ε = Metric.ball x ε
• Metric.closedBall_eq_sphere_of_nonpos 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (hε : ε ≤ 0) : Metric.closedBall x ε = Metric.sphere x ε
• Metric.closedBall_of_neg 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : ε < 0 → Metric.closedBall x ε = ∅
• Metric.closedBall_sdiff_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.closedBall x ε \ Metric.ball x ε = Metric.sphere x ε
• Metric.closedBall_sdiff_sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.closedBall x ε \ Metric.sphere x ε = Metric.ball x ε
• Metric.iUnion_inter_closedBall_nat 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (s : Set α) (x : α) : ⋃ n, s ∩ Metric.closedBall x ↑n = s
• Metric.nonneg_of_mem_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} (hy : y ∈ Metric.closedBall x ε) : 0 ≤ ε
• Metric.sphere_union_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.sphere x ε ∪ Metric.ball x ε = Metric.closedBall x ε
• Metric.closedBall_eq_empty 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.closedBall x ε = ∅ ↔ ε < 0
• Metric.forall_of_forall_mem_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (p : α → Prop) (x : α) (H : ∃ᶠ (R : ℝ) in Filter.atTop, ∀ y ∈ Metric.closedBall x R, p y) (y : α) : p y
• Metric.mem_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} : y ∈ Metric.closedBall x ε ↔ dist y x ≤ ε
• Metric.mem_closedBall' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} : y ∈ Metric.closedBall x ε ↔ dist x y ≤ ε
• Metric.nhds_basis_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} : (nhds x).HasBasis (fun ε => 0 < ε) (Metric.closedBall x)
• Metric.mem_closedBall_comm 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} : x ∈ Metric.closedBall y ε ↔ y ∈ Metric.closedBall x ε
• Real.closedBall_eq_Icc 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {x r : ℝ} : Metric.closedBall x r = Set.Icc (x - r) (x + r)
• Metric.closedBall_eq_singleton_of_subsingleton 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} [Subsingleton α] (h : 0 ≤ ε) : Metric.closedBall x ε = {x}
• Metric.closedEBall_coe 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : NNReal} : Metric.closedEBall x ↑ε = Metric.closedBall x ↑ε
• Metric.closedBall_eq_bInter_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.closedBall x ε = ⋂ δ, ⋂ (_ : δ > ε), Metric.ball x δ
• Metric.closedBall_mem_nhds 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) {ε : ℝ} (ε0 : 0 < ε) : Metric.closedBall x ε ∈ nhds x
• Metric.closedBall_mem_nhds_of_mem 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x c : α} {ε : ℝ} (h : x ∈ Metric.ball c ε) : Metric.closedBall c ε ∈ nhds x
• Metric.closedBall_subset_ball' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : ε₁ + dist x y < ε₂) : Metric.closedBall x ε₁ ⊆ Metric.ball y ε₂
• Metric.closedBall_subset_closedBall' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : ε₁ + dist x y ≤ ε₂) : Metric.closedBall x ε₁ ⊆ Metric.closedBall y ε₂
• Metric.closedEBall_ofReal 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (h : 0 ≤ ε) : Metric.closedEBall x (ENNReal.ofReal ε) = Metric.closedBall x ε
• Metric.dist_le_add_of_nonempty_closedBall_inter_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : (Metric.closedBall x ε₁ ∩ Metric.closedBall y ε₂).Nonempty) : dist x y ≤ ε₁ + ε₂
• Metric.dist_lt_add_of_nonempty_ball_inter_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : (Metric.ball x ε₁ ∩ Metric.closedBall y ε₂).Nonempty) : dist x y < ε₁ + ε₂
• Metric.dist_lt_add_of_nonempty_closedBall_inter_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : (Metric.closedBall x ε₁ ∩ Metric.ball y ε₂).Nonempty) : dist x y < ε₁ + ε₂
• Metric.nhds_basis_closedBall_inv_nat_pos 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} : (nhds x).HasBasis (fun n => 0 < n) fun n => Metric.closedBall x (1 / ↑n)
• Metric.nhds_basis_closedBall_inv_nat_succ 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} : (nhds x).HasBasis (fun x => True) fun n => Metric.closedBall x (1 / (↑n + 1))
• Metric.nhds_basis_closedBall_pow 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {r : ℝ} (h0 : 0 < r) (h1 : r < 1) : (nhds x).HasBasis (fun x => True) fun n => Metric.closedBall x (r ^ n)
• Metric.ball_disjoint_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {δ ε : ℝ} (h : δ + ε ≤ dist x y) : Disjoint (Metric.ball x δ) (Metric.closedBall y ε)
• Metric.closedBall_disjoint_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {δ ε : ℝ} (h : δ + ε ≤ dist x y) : Disjoint (Metric.closedBall x δ) (Metric.ball y ε)
• Metric.closedBall_disjoint_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {δ ε : ℝ} (h : δ + ε < dist x y) : Disjoint (Metric.closedBall x δ) (Metric.closedBall y ε)
• Real.Icc_eq_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  (x y : ℝ) : Set.Icc x y = Metric.closedBall ((x + y) / 2) ((y - x) / 2)
• Metric.subsingleton_closedBall 📋 Mathlib.Topology.MetricSpace.Defs
  {γ : Type w} [MetricSpace γ] (x : γ) {r : ℝ} (hr : r ≤ 0) : (Metric.closedBall x r).Subsingleton
• Metric.closedBall_zero 📋 Mathlib.Topology.MetricSpace.Defs
  {γ : Type w} [MetricSpace γ] {x : γ} : Metric.closedBall x 0 = {x}
• Metric.exists_closedBall_inter_eq_singleton_of_discrete 📋 Mathlib.Topology.MetricSpace.Pseudo.Basic
  {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : IsDiscrete s) {x : α} (hx : x ∈ s) : ∃ ε > 0, Metric.closedBall x ε ∩ s = {x}
• NNReal.closedBall_zero_eq_Icc' 📋 Mathlib.Topology.MetricSpace.Pseudo.Constructions
  (c : NNReal) : Metric.closedBall 0 ↑c = Set.Icc 0 c
• NNReal.closedBall_zero_eq_Icc 📋 Mathlib.Topology.MetricSpace.Pseudo.Constructions
  {c : ℝ} (c_nn : 0 ≤ c) : Metric.closedBall 0 c = Set.Icc 0 c.toNNReal
• closedBall_prod_same 📋 Mathlib.Topology.MetricSpace.Pseudo.Constructions
  {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] (x : α) (y : β) (r : ℝ) : Metric.closedBall x r ×ˢ Metric.closedBall y r = Metric.closedBall (x, y) r
• Subtype.preimage_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Constructions
  {α : Type u_1} [PseudoMetricSpace α] {p : α → Prop} (a : { a // p a }) (r : ℝ) : Subtype.val ⁻¹' Metric.closedBall (↑a) r = Metric.closedBall a r
• Subtype.image_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Constructions
  {α : Type u_1} [PseudoMetricSpace α] {p : α → Prop} (a : { a // p a }) (r : ℝ) : Subtype.val '' Metric.closedBall a r = Metric.closedBall (↑a) r ∩ {a | p a}
• sphere_prod 📋 Mathlib.Topology.MetricSpace.Pseudo.Constructions
  {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] (x : α × β) (r : ℝ) : Metric.sphere x r = Metric.sphere x.1 r ×ˢ Metric.closedBall x.2 r ∪ Metric.closedBall x.1 r ×ˢ Metric.sphere x.2 r
• Metric.isClosed_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : ℝ} : IsClosed (Metric.closedBall x ε)
• Metric.closure_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : ℝ} : closure (Metric.closedBall x ε) = Metric.closedBall x ε
• Metric.closure_ball_subset_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : ℝ} : closure (Metric.ball x ε) ⊆ Metric.closedBall x ε
• Metric.frontier_closedBall_subset_sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : ℝ} : frontier (Metric.closedBall x ε) ⊆ Metric.sphere x ε
• Metric.closedBall_zero' 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] (x : α) : Metric.closedBall x 0 = closure {x}
• Metric.biInter_gt_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] (x : α) (r : ℝ) : ⋂ r', ⋂ (_ : r' > r), Metric.ball x r' = Metric.closedBall x r
• Metric.biInter_gt_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] (x : α) (r : ℝ) : ⋂ r', ⋂ (_ : r' > r), Metric.closedBall x r' = Metric.closedBall x r
• Metric.biUnion_lt_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] (x : α) (r : ℝ) : ⋃ r', ⋃ (_ : r' < r), Metric.closedBall x r' = Metric.ball x r
• tendsto_closedBall_smallSets 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] (x : α) : Filter.Tendsto (Metric.closedBall x) (nhds 0) (nhds x).smallSets
• Metric.exists_isCompact_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] [WeaklyLocallyCompactSpace α] (x : α) : ∃ r, 0 < r ∧ IsCompact (Metric.closedBall x r)
• Metric.eventually_isCompact_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] [WeaklyLocallyCompactSpace α] (x : α) : ∀ᶠ (r : ℝ) in nhds 0, IsCompact (Metric.closedBall x r)
• eventually_closedBall_subset 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] {x : α} {u : Set α} (hu : u ∈ nhds x) : ∀ᶠ (r : ℝ) in nhds 0, Metric.closedBall x r ⊆ u
• closedBall_pi' 📋 Mathlib.Topology.MetricSpace.Pseudo.Pi
  {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (X b)] [Nonempty β] (x : (b : β) → X b) (r : ℝ) : Metric.closedBall x r = Set.univ.pi fun b => Metric.closedBall (x b) r
• closedBall_pi 📋 Mathlib.Topology.MetricSpace.Pseudo.Pi
  {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (X b)] (x : (b : β) → X b) {r : ℝ} (hr : 0 ≤ r) : Metric.closedBall x r = Set.univ.pi fun b => Metric.closedBall (x b) r
• sphere_pi 📋 Mathlib.Topology.MetricSpace.Pseudo.Pi
  {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (X b)] (x : (b : β) → X b) {r : ℝ} (h : 0 < r ∨ Nonempty β) : Metric.sphere x r = (⋃ i, Function.eval i ⁻¹' Metric.sphere (x i) r) ∩ Metric.closedBall x r
• norm_le_of_mem_closedBall 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddGroup E] {a b : E} {r : ℝ} (h : b ∈ Metric.closedBall a r) : ‖b‖ ≤ ‖a‖ + r
• norm_le_of_mem_closedBall' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedGroup E] {a b : E} {r : ℝ} (h : b ∈ Metric.closedBall a r) : ‖b‖ ≤ ‖a‖ + r
• mem_closedBall_one_iff 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedGroup E] {a : E} {r : ℝ} : a ∈ Metric.closedBall 1 r ↔ ‖a‖ ≤ r
• mem_closedBall_zero_iff 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddGroup E] {a : E} {r : ℝ} : a ∈ Metric.closedBall 0 r ↔ ‖a‖ ≤ r
• mem_closedBall_iff_norm 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : b ∈ Metric.closedBall a r ↔ ‖b - a‖ ≤ r
• mem_closedBall_iff_norm' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : b ∈ Metric.closedBall a r ↔ ‖a - b‖ ≤ r
• mem_closedBall_iff_norm'' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} : b ∈ Metric.closedBall a r ↔ ‖b / a‖ ≤ r
• mem_closedBall_iff_norm''' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} : b ∈ Metric.closedBall a r ↔ ‖a / b‖ ≤ r
• add_mem_closedBall_iff_norm 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : a + b ∈ Metric.closedBall a r ↔ ‖b‖ ≤ r
• mul_mem_closedBall_iff_norm 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} : a * b ∈ Metric.closedBall a r ↔ ‖b‖ ≤ r
• mem_closedBall_iff_norm_inv_mul_le 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedGroup E] {a b : E} {r : ℝ} : b ∈ Metric.closedBall a r ↔ ‖b⁻¹ * a‖ ≤ r
• mem_closedBall_iff_norm_inv_mul_le' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedGroup E] {a b : E} {r : ℝ} : b ∈ Metric.closedBall a r ↔ ‖a⁻¹ * b‖ ≤ r
• mem_closedBall_iff_norm_neg_add_le 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddGroup E] {a b : E} {r : ℝ} : b ∈ Metric.closedBall a r ↔ ‖-b + a‖ ≤ r
• mem_closedBall_iff_norm_neg_add_le' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddGroup E] {a b : E} {r : ℝ} : b ∈ Metric.closedBall a r ↔ ‖-a + b‖ ≤ r
• setOf_div_mem_closedBall_eq_closedBall'' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedCommGroup E] {a : E} {r : ℝ} : {x | x / a ∈ Metric.closedBall 1 r} = Metric.closedBall a r
• setOf_sub_mem_closedBall_eq_closedBall 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddCommGroup E] {a : E} {r : ℝ} : {x | x - a ∈ Metric.closedBall 0 r} = Metric.closedBall a r
• preimage_add_closedBall 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddCommGroup E] (a b : E) (r : ℝ) : (fun x => b + x) ⁻¹' Metric.closedBall a r = Metric.closedBall (a - b) r
• preimage_mul_closedBall 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedCommGroup E] (a b : E) (r : ℝ) : (fun x => b * x) ⁻¹' Metric.closedBall a r = Metric.closedBall (a / b) r
• smul_closedBall'' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} : a • Metric.closedBall b r = Metric.closedBall (a • b) r
• vadd_closedBall'' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : a +ᵥ Metric.closedBall b r = Metric.closedBall (a +ᵥ b) r
• add_mem_closedBall_add_iff 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} {c : E} : a + c ∈ Metric.closedBall (b + c) r ↔ a ∈ Metric.closedBall b r
• mul_mem_closedBall_mul_iff 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} {c : E} : a * c ∈ Metric.closedBall (b * c) r ↔ a ∈ Metric.closedBall b r
• nsmul_mem_closedBall 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} {n : ℕ} (h : a ∈ Metric.closedBall b r) : n • a ∈ Metric.closedBall (n • b) (n • r)
• pow_mem_closedBall 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} {n : ℕ} (h : a ∈ Metric.closedBall b r) : a ^ n ∈ Metric.closedBall (b ^ n) (n • r)
• ProperSpace.isCompact_closedBall 📋 Mathlib.Topology.MetricSpace.ProperSpace
  {α : Type u} {inst✝ : PseudoMetricSpace α} [self : ProperSpace α] (x : α) (r : ℝ) : IsCompact (Metric.closedBall x r)
• ProperSpace.mk 📋 Mathlib.Topology.MetricSpace.ProperSpace
  {α : Type u} [PseudoMetricSpace α] (isCompact_closedBall : ∀ (x : α) (r : ℝ), IsCompact (Metric.closedBall x r)) : ProperSpace α
• ProperSpace.of_isCompact_closedBall_of_le 📋 Mathlib.Topology.MetricSpace.ProperSpace
  {α : Type u} [PseudoMetricSpace α] (R : ℝ) (h : ∀ (x : α) (r : ℝ), R ≤ r → IsCompact (Metric.closedBall x r)) : ProperSpace α
• instCompactSpaceElemClosedBallOfProperSpace 📋 Mathlib.Topology.MetricSpace.ProperSpace
  {α : Type u_2} [PseudoMetricSpace α] [ProperSpace α] (x : α) (r : ℝ) : CompactSpace ↑(Metric.closedBall x r)
• ProperSpace.of_seq_closedBall 📋 Mathlib.Topology.MetricSpace.ProperSpace
  {α : Type u} [PseudoMetricSpace α] {β : Type u_2} {l : Filter β} [l.NeBot] {x : α} {r : β → ℝ} (hr : Filter.Tendsto r l Filter.atTop) (hc : ∀ᶠ (i : β) in l, IsCompact (Metric.closedBall x (r i))) : ProperSpace α
• Metric.isBounded_closedBall 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} {x : α} {r : ℝ} [PseudoMetricSpace α] : Bornology.IsBounded (Metric.closedBall x r)
• Metric.hasAntitoneBasis_cobounded_compl_closedBall 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} [PseudoMetricSpace α] (c : α) : (Bornology.cobounded α).HasAntitoneBasis fun r => (Metric.closedBall c r)ᶜ
• Metric.hasBasis_cobounded_compl_closedBall 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} [PseudoMetricSpace α] (c : α) : (Bornology.cobounded α).HasBasis (fun x => True) fun r => (Metric.closedBall c r)ᶜ
• Bornology.IsBounded.subset_closedBall 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} {s : Set α} [PseudoMetricSpace α] (h : Bornology.IsBounded s) (c : α) : ∃ r, s ⊆ Metric.closedBall c r
• Metric.isBounded_iff_subset_closedBall 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} {s : Set α} [PseudoMetricSpace α] (c : α) : Bornology.IsBounded s ↔ ∃ r, s ⊆ Metric.closedBall c r
• Bornology.IsCobounded.closedBall_compl_subset 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : Bornology.IsCobounded s) (c : α) : ∃ r, (Metric.closedBall c r)ᶜ ⊆ s
• Metric.isCobounded_iff_closedBall_compl_subset 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} [PseudoMetricSpace α] {s : Set α} (c : α) : Bornology.IsCobounded s ↔ ∃ r, (Metric.closedBall c r)ᶜ ⊆ s
• Bornology.IsBounded.subset_closedBall_lt 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} {s : Set α} [PseudoMetricSpace α] (h : Bornology.IsBounded s) (a : ℝ) (c : α) : ∃ r, a < r ∧ s ⊆ Metric.closedBall c r
• Metric.closedBall_compl_subset_of_mem_cocompact 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : s ∈ Filter.cocompact α) (c : α) : ∃ r, (Metric.closedBall c r)ᶜ ⊆ s
• IsOrderBornology.of_isCompactIcc 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (x : α) (bddBelow_ball : ∀ (r : ℝ), BddBelow (Metric.closedBall x r)) (bddAbove_ball : ∀ (r : ℝ), BddAbove (Metric.closedBall x r)) : IsOrderBornology α
• Metric.mem_cocompact_of_closedBall_compl_subset 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} {s : Set α} [PseudoMetricSpace α] [ProperSpace α] (c : α) (h : ∃ r, (Metric.closedBall c r)ᶜ ⊆ s) : s ∈ Filter.cocompact α
• Metric.mem_cocompact_iff_closedBall_compl_subset 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} {s : Set α} [PseudoMetricSpace α] [ProperSpace α] (c : α) : s ∈ Filter.cocompact α ↔ ∃ r, (Metric.closedBall c r)ᶜ ⊆ s
• Metric.diam_closedBall 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} {x : α} [PseudoMetricSpace α] {r : ℝ} (h : 0 ≤ r) : Metric.diam (Metric.closedBall x r) ≤ 2 * r
• Metric.diam_le_of_subset_closedBall 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} {s : Set α} {x : α} [PseudoMetricSpace α] {r : ℝ} (hr : 0 ≤ r) (h : s ⊆ Metric.closedBall x r) : Metric.diam s ≤ 2 * r
• Int.preimage_closedBall 📋 Mathlib.Topology.Instances.Int
  (x : ℤ) (r : ℝ) : Int.cast ⁻¹' Metric.closedBall (↑x) r = Metric.closedBall x r
• Int.closedBall_eq_Icc 📋 Mathlib.Topology.Instances.Int
  (x : ℤ) (r : ℝ) : Metric.closedBall x r = Set.Icc ⌈↑x - r⌉ ⌊↑x + r⌋
• Nat.preimage_closedBall 📋 Mathlib.Topology.Instances.Nat
  (x : ℕ) (r : ℝ) : Nat.cast ⁻¹' Metric.closedBall (↑x) r = Metric.closedBall x r
• Nat.closedBall_eq_Icc 📋 Mathlib.Topology.Instances.Nat
  (x : ℕ) (r : ℝ) : Metric.closedBall x r = Set.Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊
• Isometry.mapsTo_closedBall 📋 Mathlib.Topology.MetricSpace.Isometry
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} (hf : Isometry f) (x : α) (r : ℝ) : Set.MapsTo f (Metric.closedBall x r) (Metric.closedBall (f x) r)
• Isometry.preimage_closedBall 📋 Mathlib.Topology.MetricSpace.Isometry
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} (hf : Isometry f) (x : α) (r : ℝ) : f ⁻¹' Metric.closedBall (f x) r = Metric.closedBall x r
• IsometryEquiv.image_closedBall 📋 Mathlib.Topology.MetricSpace.Isometry
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β) (x : α) (r : ℝ) : ⇑h '' Metric.closedBall x r = Metric.closedBall (h x) r
• IsometryEquiv.preimage_closedBall 📋 Mathlib.Topology.MetricSpace.Isometry
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β) (x : β) (r : ℝ) : ⇑h ⁻¹' Metric.closedBall x r = Metric.closedBall (h.symm x) r
• LipschitzWith.mapsTo_closedBall 📋 Mathlib.Topology.MetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) (x : α) (r : ℝ) : Set.MapsTo f (Metric.closedBall x r) (Metric.closedBall (f x) (↑K * r))
• Metric.preimage_add_left_closedBall 📋 Mathlib.Topology.MetricSpace.IsometricSMul
  {G : Type v} [AddGroup G] [PseudoMetricSpace G] [IsIsometricVAdd G G] (a b : G) (r : ℝ) : (fun x => a + x) ⁻¹' Metric.closedBall b r = Metric.closedBall (-a + b) r
• Metric.preimage_mul_left_closedBall 📋 Mathlib.Topology.MetricSpace.IsometricSMul
  {G : Type v} [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G] (a b : G) (r : ℝ) : (fun x => a * x) ⁻¹' Metric.closedBall b r = Metric.closedBall (a⁻¹ * b) r
• Metric.preimage_add_right_closedBall 📋 Mathlib.Topology.MetricSpace.IsometricSMul
  {G : Type v} [AddGroup G] [PseudoMetricSpace G] [IsIsometricVAdd Gᵃᵒᵖ G] (a b : G) (r : ℝ) : (fun x => x + a) ⁻¹' Metric.closedBall b r = Metric.closedBall (b - a) r
• Metric.preimage_mul_right_closedBall 📋 Mathlib.Topology.MetricSpace.IsometricSMul
  {G : Type v} [Group G] [PseudoMetricSpace G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ) : (fun x => x * a) ⁻¹' Metric.closedBall b r = Metric.closedBall (b / a) r
• Metric.smul_closedBall 📋 Mathlib.Topology.MetricSpace.IsometricSMul
  {G : Type v} {X : Type w} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] (c : G) (x : X) (r : ℝ) : c • Metric.closedBall x r = Metric.closedBall (c • x) r
• Metric.vadd_closedBall 📋 Mathlib.Topology.MetricSpace.IsometricSMul
  {G : Type v} {X : Type w} [PseudoMetricSpace X] [AddGroup G] [AddAction G X] [IsIsometricVAdd G X] (c : G) (x : X) (r : ℝ) : c +ᵥ Metric.closedBall x r = Metric.closedBall (c +ᵥ x) r
• Metric.preimage_smul_closedBall 📋 Mathlib.Topology.MetricSpace.IsometricSMul
  {G : Type v} {X : Type w} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] (c : G) (x : X) (r : ℝ) : (fun x => c • x) ⁻¹' Metric.closedBall x r = Metric.closedBall (c⁻¹ • x) r
• Metric.preimage_vadd_closedBall 📋 Mathlib.Topology.MetricSpace.IsometricSMul
  {G : Type v} {X : Type w} [PseudoMetricSpace X] [AddGroup G] [AddAction G X] [IsIsometricVAdd G X] (c : G) (x : X) (r : ℝ) : (fun x => c +ᵥ x) ⁻¹' Metric.closedBall x r = Metric.closedBall (-c +ᵥ x) r
• NormedDivisionRing.unitClosedBall_eq_univ_of_discrete 📋 Mathlib.Analysis.Normed.Field.Basic
  {𝕜 : Type u_3} [NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] : Metric.closedBall 0 1 = Set.univ
• Dilation.mapsTo_closedBall 📋 Mathlib.Topology.MetricSpace.Dilation
  {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) (x : α) (r' : ℝ) : Set.MapsTo (⇑f) (Metric.closedBall x r') (Metric.closedBall (f x) (↑(Dilation.ratio f) * r'))
• Metric.smul_image_closedBall 📋 Mathlib.Analysis.Normed.MulAction
  {α : Type u_1} {β : Type u_2} [NormedDivisionRing α] [SeminormedAddCommGroup β] [Module α β] [NormSMulClass α β] {s : α} (hs : s ≠ 0) (x : β) (ε : ℝ) : (fun x => s • x) '' Metric.closedBall x ε = Metric.closedBall (s • x) (‖s‖ * ε)
• NormedField.completeSpace_iff_isComplete_closedBall 📋 Mathlib.Analysis.Normed.Field.Lemmas
  {K : Type u_4} [NormedField K] : CompleteSpace K ↔ IsComplete (Metric.closedBall 0 1)
• Metric.diam_closedBall_eq 📋 Mathlib.Analysis.Normed.Module.Basic
  {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) {r : ℝ} (hr : 0 ≤ r) : Metric.diam (Metric.closedBall x r) = 2 * r
• MeasureTheory.measure_closedBall_lt_top 📋 Mathlib.MeasureTheory.Measure.Typeclasses.Finite
  {α : Type u_1} {m0 : MeasurableSpace α} [PseudoMetricSpace α] [ProperSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {x : α} {r : ℝ} : μ (Metric.closedBall x r) < ⊤
• Metric.infDist_inter_closedBall_of_mem 📋 Mathlib.Topology.MetricSpace.HausdorffDistance
  {α : Type u} [PseudoMetricSpace α] {s : Set α} {x y : α} (h : y ∈ s) : Metric.infDist x (s ∩ Metric.closedBall x (dist y x)) = Metric.infDist x s
• Metric.disjoint_closedBall_of_lt_infDist 📋 Mathlib.Topology.MetricSpace.HausdorffDistance
  {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {r : ℝ} (h : r < Metric.infDist x s) : Disjoint (Metric.closedBall x r) s
• Metric.closedBall_subset_cthickening_singleton 📋 Mathlib.Topology.MetricSpace.Thickening
  {α : Type u_2} [PseudoMetricSpace α] (x : α) (δ : ℝ) : Metric.closedBall x δ ⊆ Metric.cthickening δ {x}
• Metric.closedBall_subset_cthickening 📋 Mathlib.Topology.MetricSpace.Thickening
  {α : Type u_2} [PseudoMetricSpace α] {x : α} {E : Set α} (hx : x ∈ E) (δ : ℝ) : Metric.closedBall x δ ⊆ Metric.cthickening δ E
• Metric.cthickening_singleton 📋 Mathlib.Topology.MetricSpace.Thickening
  {α : Type u_2} [PseudoMetricSpace α] (x : α) {δ : ℝ} (hδ : 0 ≤ δ) : Metric.cthickening δ {x} = Metric.closedBall x δ
• IsCompact.cthickening_eq_biUnion_closedBall 📋 Mathlib.Topology.MetricSpace.Thickening
  {α : Type u_2} [PseudoMetricSpace α] {δ : ℝ} {E : Set α} (hE : IsCompact E) (hδ : 0 ≤ δ) : Metric.cthickening δ E = ⋃ x ∈ E, Metric.closedBall x δ
• Metric.cthickening_subset_iUnion_closedBall_of_lt 📋 Mathlib.Topology.MetricSpace.Thickening
  {α : Type u_2} [PseudoMetricSpace α] (E : Set α) {δ δ' : ℝ} (hδ₀ : 0 < δ') (hδδ' : δ < δ') : Metric.cthickening δ E ⊆ ⋃ x ∈ E, Metric.closedBall x δ'
• IsClosed.cthickening_eq_biUnion_closedBall 📋 Mathlib.Topology.MetricSpace.Thickening
  {δ : ℝ} {α : Type u_2} [PseudoMetricSpace α] [ProperSpace α] {E : Set α} (hE : IsClosed E) (hδ : 0 ≤ δ) : Metric.cthickening δ E = ⋃ x ∈ E, Metric.closedBall x δ
• Metric.cthickening_eq_biUnion_closedBall 📋 Mathlib.Topology.MetricSpace.Thickening
  {δ : ℝ} {α : Type u_2} [PseudoMetricSpace α] [ProperSpace α] (E : Set α) (hδ : 0 ≤ δ) : Metric.cthickening δ E = ⋃ x ∈ closure E, Metric.closedBall x δ
• measurableSet_closedBall 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
  {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {x : α} {ε : ℝ} : MeasurableSet (Metric.closedBall x ε)
• unitInterval.eq_closedBall 📋 Mathlib.Topology.UnitInterval
  : unitInterval = Metric.closedBall 2⁻¹ 2⁻¹
• Metric.measure_closedBall_pos 📋 Mathlib.MeasureTheory.Measure.OpenPos
  {X : Type u_1} [PseudoMetricSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] (x : X) {r : ℝ} (hr : 0 < r) : 0 < μ (Metric.closedBall x r)
• Metric.measure_closedBall_pos_iff 📋 Mathlib.MeasureTheory.Measure.OpenPos
  {X : Type u_2} [MetricSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] [MeasureTheory.NullSingletonClass μ] {x : X} {r : ℝ} : 0 < μ (Metric.closedBall x r) ↔ 0 < r
• IsUnifLocDoublingMeasure.eventually_measure_le_scaling_constant_mul 📋 Mathlib.MeasureTheory.Measure.Doubling
  {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] (K : ℝ) : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (x : α), μ (Metric.closedBall x (K * r)) ≤ ↑(IsUnifLocDoublingMeasure.scalingConstantOf μ K) * μ (Metric.closedBall x r)
• IsUnifLocDoublingMeasure.exists_eventually_forall_measure_closedBall_le_mul 📋 Mathlib.MeasureTheory.Measure.Doubling
  {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] (K : ℝ) : ∃ C, ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (x : α), ∀ t ≤ K, μ (Metric.closedBall x (t * ε)) ≤ ↑C * μ (Metric.closedBall x ε)
• IsUnifLocDoublingMeasure.measure_mul_le_scalingConstantOf_mul 📋 Mathlib.MeasureTheory.Measure.Doubling
  {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] {K : ℝ} {x : α} {t r : ℝ} (ht : t ∈ Set.Ioc 0 K) (hr : r ≤ IsUnifLocDoublingMeasure.scalingScaleOf μ K) : μ (Metric.closedBall x (t * r)) ≤ ↑(IsUnifLocDoublingMeasure.scalingConstantOf μ K) * μ (Metric.closedBall x r)
• IsUnifLocDoublingMeasure.eventually_measure_le_scaling_constant_mul' 📋 Mathlib.MeasureTheory.Measure.Doubling
  {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] (K : ℝ) (hK : 0 < K) : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (x : α), μ (Metric.closedBall x r) ≤ ↑(IsUnifLocDoublingMeasure.scalingConstantOf μ K⁻¹) * μ (Metric.closedBall x (K * r))
• IsUnifLocDoublingMeasure.eventually_measure_mul_le_scalingConstantOf_mul 📋 Mathlib.MeasureTheory.Measure.Doubling
  {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] (K : ℝ) : ∃ R, 0 < R ∧ ∀ (x : α) (t r : ℝ), t ∈ Set.Ioc 0 K → r ≤ R → μ (Metric.closedBall x (t * r)) ≤ ↑(IsUnifLocDoublingMeasure.scalingConstantOf μ K) * μ (Metric.closedBall x r)
• IsUnifLocDoublingMeasure.exists_measure_closedBall_le_mul 📋 Mathlib.MeasureTheory.Measure.Doubling
  {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] : ∃ C, ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (x : α), μ (Metric.closedBall x (2 * ε)) ≤ ↑C * μ (Metric.closedBall x ε)
• IsUnifLocDoublingMeasure.exists_measure_closedBall_le_mul'' 📋 Mathlib.MeasureTheory.Measure.Doubling
  {α : Type u_1} {inst✝ : PseudoMetricSpace α} {inst✝¹ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : IsUnifLocDoublingMeasure μ] : ∃ C, ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (x : α), μ (Metric.closedBall x (2 * ε)) ≤ ↑C * μ (Metric.closedBall x ε)
• IsUnifLocDoublingMeasure.mk 📋 Mathlib.MeasureTheory.Measure.Doubling
  {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} (exists_measure_closedBall_le_mul'' : ∃ C, ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (x : α), μ (Metric.closedBall x (2 * ε)) ≤ ↑C * μ (Metric.closedBall x ε)) : IsUnifLocDoublingMeasure μ
• IsUnifLocDoublingMeasure.eventually_measure_le_doublingConstant_mul 📋 Mathlib.MeasureTheory.Measure.Doubling
  {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (x : α), μ (Metric.closedBall x (2 * ε)) ≤ ↑(IsUnifLocDoublingMeasure.doublingConstant μ) * μ (Metric.closedBall x ε)
• LinearIsometry.preimage_closedBall 📋 Mathlib.Analysis.Normed.Operator.LinearIsometry
  {R : Type u_1} {R₂ : Type u_2} {E : Type u_4} {E₂ : Type u_5} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) (r : ℝ) : ⇑f ⁻¹' Metric.closedBall (f x) r = Metric.closedBall x r
• LinearIsometryEquiv.image_closedBall 📋 Mathlib.Analysis.Normed.Operator.LinearIsometry
  {R : Type u_1} {R₂ : Type u_2} {E : Type u_4} {E₂ : Type u_5} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) (r : ℝ) : ⇑e '' Metric.closedBall x r = Metric.closedBall (e x) r
• LinearIsometryEquiv.preimage_closedBall 📋 Mathlib.Analysis.Normed.Operator.LinearIsometry
  {R : Type u_1} {R₂ : Type u_2} {E : Type u_4} {E₂ : Type u_5} [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E₂) (r : ℝ) : ⇑e ⁻¹' Metric.closedBall x r = Metric.closedBall (e.symm x) r
• Metric.star_closedBall 📋 Mathlib.Analysis.CStarAlgebra.Basic
  {E : Type u_2} [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] (x : E) (r : ℝ) : star (Metric.closedBall x r) = Metric.closedBall (star x) r
• inv_closedBall 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : (Metric.closedBall x δ)⁻¹ = Metric.closedBall x⁻¹ δ
• neg_closedBall 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : -Metric.closedBall x δ = Metric.closedBall (-x) δ
• closedBall_div_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) : Metric.closedBall x δ / {y} = Metric.closedBall (x / y) δ
• closedBall_sub_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) : Metric.closedBall x δ - {y} = Metric.closedBall (x - y) δ
• singleton_div_closedBall 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) : {x} / Metric.closedBall y δ = Metric.closedBall (x / y) δ
• singleton_div_closedBall_one 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : {x} / Metric.closedBall 1 δ = Metric.closedBall x δ
• singleton_sub_closedBall 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) : {x} - Metric.closedBall y δ = Metric.closedBall (x - y) δ
• singleton_sub_closedBall_zero 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : {x} - Metric.closedBall 0 δ = Metric.closedBall x δ
• smul_closedBall_one 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : x • Metric.closedBall 1 δ = Metric.closedBall x δ
• vadd_closedBall_zero 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : x +ᵥ Metric.closedBall 0 δ = Metric.closedBall x δ
• closedBall_one_mul_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : Metric.closedBall 1 δ * {x} = Metric.closedBall x δ
• closedBall_zero_add_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : Metric.closedBall 0 δ + {x} = Metric.closedBall x δ
• singleton_add_closedBall_zero 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : {x} + Metric.closedBall 0 δ = Metric.closedBall x δ
• singleton_mul_closedBall_one 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : {x} * Metric.closedBall 1 δ = Metric.closedBall x δ
• closedBall_add_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) : Metric.closedBall x δ + {y} = Metric.closedBall (x + y) δ
• closedBall_mul_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) : Metric.closedBall x δ * {y} = Metric.closedBall (x * y) δ
• singleton_add_closedBall 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) : {x} + Metric.closedBall y δ = Metric.closedBall (x + y) δ
• singleton_mul_closedBall 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) : {x} * Metric.closedBall y δ = Metric.closedBall (x * y) δ
• closedBall_one_div_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : Metric.closedBall 1 δ / {x} = Metric.closedBall x⁻¹ δ
• closedBall_zero_sub_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : Metric.closedBall 0 δ - {x} = Metric.closedBall (-x) δ
• IsCompact.div_closedBall_one 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) : s / Metric.closedBall 1 δ = Metric.cthickening δ s
• IsCompact.sub_closedBall_zero 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) : s - Metric.closedBall 0 δ = Metric.cthickening δ s
• IsCompact.add_closedBall_zero 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) : s + Metric.closedBall 0 δ = Metric.cthickening δ s
• IsCompact.closedBall_one_mul 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) : Metric.closedBall 1 δ * s = Metric.cthickening δ s
• IsCompact.closedBall_zero_add 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) : Metric.closedBall 0 δ + s = Metric.cthickening δ s
• IsCompact.mul_closedBall_one 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) : s * Metric.closedBall 1 δ = Metric.cthickening δ s
• IsCompact.closedBall_one_div 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) : Metric.closedBall 1 δ / s = Metric.cthickening δ s⁻¹
• IsCompact.closedBall_zero_sub 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) : Metric.closedBall 0 δ - s = Metric.cthickening δ (-s)
• IsCompact.add_closedBall 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) : s + Metric.closedBall x δ = x +ᵥ Metric.cthickening δ s
• IsCompact.closedBall_add 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) : Metric.closedBall x δ + s = x +ᵥ Metric.cthickening δ s
• IsCompact.closedBall_div 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) : Metric.closedBall x δ * s = x • Metric.cthickening δ s
• IsCompact.closedBall_mul 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) : Metric.closedBall x δ * s = x • Metric.cthickening δ s
• IsCompact.closedBall_sub 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) : Metric.closedBall x δ + s = x +ᵥ Metric.cthickening δ s
• IsCompact.mul_closedBall 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) : s * Metric.closedBall x δ = x • Metric.cthickening δ s
• IsCompact.div_closedBall 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) : s / Metric.closedBall x δ = x⁻¹ • Metric.cthickening δ s
• IsCompact.sub_closedBall 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] {δ : ℝ} {s : Set E} (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) : s - Metric.closedBall x δ = -x +ᵥ Metric.cthickening δ s
• closure_ball 📋 Mathlib.Analysis.Normed.Module.RCLike.Real
  {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) : closure (Metric.ball x r) = Metric.closedBall x r
• frontier_closedBall 📋 Mathlib.Analysis.Normed.Module.RCLike.Real
  {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) : frontier (Metric.closedBall x r) = Metric.sphere x r
• interior_closedBall 📋 Mathlib.Analysis.Normed.Module.RCLike.Real
  {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) : interior (Metric.closedBall x r) = Metric.ball x r

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59