Loogle!

Result

Found 558 declarations mentioning Metric.ball. Of these, only the first 200 are shown.

• Metric.ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α
• Metric.isOpen_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : IsOpen (Metric.ball x ε)
• Metric.ball_subset_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.ball x ε ⊆ Metric.closedBall x ε
• Metric.iUnion_ball_nat 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) : ⋃ n, Metric.ball x ↑n = Set.univ
• Metric.ball_zero 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} : Metric.ball x 0 = ∅
• Real.ball_zero_eq_Ioo 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  (r : ℝ) : Metric.ball 0 r = Set.Ioo (-r) r
• Metric.nonempty_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : (Metric.ball x ε).Nonempty ↔ 0 < ε
• Metric.ball_subset_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε₁ ε₂ : ℝ} (h : ε₁ ≤ ε₂) : Metric.ball x ε₁ ⊆ Metric.ball x ε₂
• Metric.closedBall_subset_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε₁ ε₂ : ℝ} (h : ε₁ < ε₂) : Metric.closedBall x ε₁ ⊆ Metric.ball x ε₂
• Metric.sphere_subset_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {r R : ℝ} (h : r < R) : Metric.sphere x r ⊆ Metric.ball x R
• Metric.ball_subset_interior_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.ball x ε ⊆ interior (Metric.closedBall x ε)
• Metric.mem_ball_self 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (h : 0 < ε) : x ∈ Metric.ball 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_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.pos_of_mem_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} (hy : y ∈ Metric.ball 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.ball_eq_empty 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.ball x ε = ∅ ↔ ε ≤ 0
• Metric.forall_of_forall_mem_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (p : α → Prop) (x : α) (H : ∃ᶠ (R : ℝ) in Filter.atTop, ∀ y ∈ Metric.ball x R, p y) (y : α) : p y
• Metric.mem_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} : y ∈ Metric.ball x ε ↔ dist y x < ε
• Metric.mem_ball' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} : y ∈ Metric.ball x ε ↔ dist x y < ε
• Metric.nhds_basis_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} : (nhds x).HasBasis (fun x => 0 < x) (Metric.ball x)
• Metric.mem_ball_comm 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} : x ∈ Metric.ball y ε ↔ y ∈ Metric.ball x ε
• Real.ball_eq_Ioo 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  (x r : ℝ) : Metric.ball x r = Set.Ioo (x - r) (x + r)
• Metric.ball_eq_singleton_of_subsingleton 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} [Subsingleton α] (h : 0 < ε) : Metric.ball x ε = {x}
• Metric.eball_ofReal 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.eball x (ENNReal.ofReal ε) = Metric.ball x ε
• Metric.eball_coe 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : NNReal} : Metric.eball x ↑ε = Metric.ball x ↑ε
• Metric.closedBall_eq_bInter_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.closedBall x ε = ⋂ δ, ⋂ (_ : δ > ε), Metric.ball x δ
• Metric.iUnion_ball_nat_succ 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) : ⋃ n, Metric.ball x (↑n + 1) = Set.univ
• Metric.ball_mem_nhds 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) {ε : ℝ} (ε0 : 0 < ε) : Metric.ball 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.dense_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {s : Set α} : Dense s ↔ ∀ (x : α), ∀ r > 0, (Metric.ball x r ∩ s).Nonempty
• Metric.exists_lt_mem_ball_of_mem_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} (h : x ∈ Metric.ball y ε) : ∃ ε' < ε, x ∈ Metric.ball y ε'
• Metric.ball_eq_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (ε : ℝ) (x : α) : UniformSpace.ball x {p | dist p.2 p.1 < ε} = Metric.ball x ε
• Metric.ball_eq_ball' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (ε : ℝ) (x : α) : UniformSpace.ball x {p | dist p.1 p.2 < ε} = Metric.ball x ε
• Metric.ball_subset 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : dist x y ≤ ε₂ - ε₁) : Metric.ball x ε₁ ⊆ Metric.ball y ε₂
• Metric.ball_subset_ball' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : ε₁ + dist x y ≤ ε₂) : Metric.ball x ε₁ ⊆ Metric.ball y ε₂
• 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.nhdsWithin_basis_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {s : Set α} : (nhdsWithin x s).HasBasis (fun ε => 0 < ε) fun ε => Metric.ball x ε ∩ s
• Metric.dist_lt_add_of_nonempty_ball_inter_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : (Metric.ball x ε₁ ∩ Metric.ball 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.exists_ball_subset_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} (h : y ∈ Metric.ball x ε) : ∃ ε' > 0, Metric.ball y ε' ⊆ Metric.ball x ε
• Metric.isOpen_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {s : Set α} : IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s
• Metric.mem_nhds_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {s : Set α} : s ∈ nhds x ↔ ∃ ε > 0, Metric.ball x ε ⊆ s
• Metric.eventually_nhds_iff_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {p : α → Prop} : (∀ᶠ (y : α) in nhds x, p y) ↔ ∃ ε > 0, ∀ y ∈ Metric.ball x ε, p y
• Metric.nhds_basis_ball_inv_nat_pos 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} : (nhds x).HasBasis (fun n => 0 < n) fun n => Metric.ball x (1 / ↑n)
• Metric.nhds_basis_ball_inv_nat_succ 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} : (nhds x).HasBasis (fun x => True) fun n => Metric.ball x (1 / (↑n + 1))
• Metric.sphere_disjoint_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Disjoint (Metric.sphere x ε) (Metric.ball x ε)
• Metric.dense_iff_iUnion_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (s : Set α) : Dense s ↔ ∀ r > 0, ⋃ c ∈ s, Metric.ball c r = Set.univ
• Metric.mem_nhdsWithin_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {s t : Set α} : s ∈ nhdsWithin x t ↔ ∃ ε > 0, Metric.ball x ε ∩ t ⊆ s
• Metric.nhds_basis_ball_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.ball x (r ^ n)
• Metric.ball_disjoint_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {δ ε : ℝ} (h : δ + ε ≤ dist x y) : Disjoint (Metric.ball x δ) (Metric.ball y ε)
• 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 ε)
• Real.Ioo_eq_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  (x y : ℝ) : Set.Ioo x y = Metric.ball ((x + y) / 2) ((y - x) / 2)
• Metric.ball_half_subset 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (y : α) (h : y ∈ Metric.ball x (ε / 2)) : Metric.ball y (ε / 2) ⊆ Metric.ball x ε
• Metric.exists_ball_inter_eq_singleton_of_mem_discrete 📋 Mathlib.Topology.MetricSpace.Pseudo.Basic
  {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : IsDiscrete s) {x : α} (hx : x ∈ s) : ∃ ε > 0, Metric.ball x ε ∩ s = {x}
• Metric.totallyBounded_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Basic
  {α : Type u} [PseudoMetricSpace α] {s : Set α} : TotallyBounded s ↔ ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, Metric.ball y ε
• Metric.finite_approx_of_totallyBounded 📋 Mathlib.Topology.MetricSpace.Pseudo.Basic
  {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : TotallyBounded s) (ε : ℝ) : ε > 0 → ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, Metric.ball y ε
• finite_cover_balls_of_compact 📋 Mathlib.Topology.MetricSpace.Pseudo.Basic
  {X : Type u_2} [PseudoMetricSpace X] {s : Set X} (hs : IsCompact s) {e : ℝ} (he : 0 < e) : ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, Metric.ball x e
• IsCompact.finite_cover_balls 📋 Mathlib.Topology.MetricSpace.Pseudo.Basic
  {X : Type u_2} [PseudoMetricSpace X] {s : Set X} (hs : IsCompact s) {e : ℝ} (he : 0 < e) : ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, Metric.ball x e
• exists_finite_cover_balls_of_isCompact_closure 📋 Mathlib.Topology.MetricSpace.Pseudo.Basic
  {X : Type u_2} [PseudoMetricSpace X] {s : Set X} {ε : ℝ} (hs : IsCompact (closure s)) (hε : 0 < ε) : ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, Metric.ball x ε
• NNReal.ball_zero_eq_Ico 📋 Mathlib.Topology.MetricSpace.Pseudo.Constructions
  (c : ℝ) : Metric.ball 0 c = Set.Ico 0 c.toNNReal
• NNReal.ball_zero_eq_Ico' 📋 Mathlib.Topology.MetricSpace.Pseudo.Constructions
  (c : NNReal) : Metric.ball 0 ↑c = Set.Ico 0 c
• ball_prod_same 📋 Mathlib.Topology.MetricSpace.Pseudo.Constructions
  {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] (x : α) (y : β) (r : ℝ) : Metric.ball x r ×ˢ Metric.ball y r = Metric.ball (x, y) r
• Subtype.preimage_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Constructions
  {α : Type u_1} [PseudoMetricSpace α] {p : α → Prop} (a : { a // p a }) (r : ℝ) : Subtype.val ⁻¹' Metric.ball (↑a) r = Metric.ball a r
• Subtype.image_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Constructions
  {α : Type u_1} [PseudoMetricSpace α] {p : α → Prop} (a : { a // p a }) (r : ℝ) : Subtype.val '' Metric.ball a r = Metric.ball (↑a) r ∩ {a | p a}
• Metric.closure_ball_subset_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : ℝ} : closure (Metric.ball x ε) ⊆ Metric.closedBall x ε
• Metric.frontier_ball_subset_sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : ℝ} : frontier (Metric.ball x ε) ⊆ Metric.sphere 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.biUnion_lt_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] (x : α) (r : ℝ) : ⋃ r', ⋃ (_ : r' < r), Metric.ball x r' = Metric.ball 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
• eventually_ball_subset 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] {x : α} {u : Set α} (hu : u ∈ nhds x) : ∀ᶠ (r : ℝ) in nhds 0, Metric.ball x r ⊆ u
• lebesgue_number_lemma_of_metric 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] {s : Set α} {ι : Sort u_3} {c : ι → Set α} (hs : IsCompact s) (hc₁ : ∀ (i : ι), IsOpen (c i)) (hc₂ : s ⊆ ⋃ i, c i) : ∃ δ > 0, ∀ x ∈ s, ∃ i, Metric.ball x δ ⊆ c i
• lebesgue_number_lemma_of_metric_sUnion 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] {s : Set α} {c : Set (Set α)} (hs : IsCompact s) (hc₁ : ∀ t ∈ c, IsOpen t) (hc₂ : s ⊆ ⋃₀ c) : ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, Metric.ball x δ ⊆ t
• ball_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.ball x r = Set.univ.pi fun b => Metric.ball (x b) r
• ball_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.ball x r = Set.univ.pi fun b => Metric.ball (x b) r
• ball_one_eq 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedGroup E] (r : ℝ) : Metric.ball 1 r = {x | ‖x‖ < r}
• ball_zero_eq 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddGroup E] (r : ℝ) : Metric.ball 0 r = {x | ‖x‖ < r}
• norm_lt_of_mem_ball 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddGroup E] {a b : E} {r : ℝ} (h : b ∈ Metric.ball a r) : ‖b‖ < ‖a‖ + r
• norm_lt_of_mem_ball' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedGroup E] {a b : E} {r : ℝ} (h : b ∈ Metric.ball a r) : ‖b‖ < ‖a‖ + r
• ball_eq 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddCommGroup E] (y : E) (ε : ℝ) : Metric.ball y ε = {x | ‖x - y‖ < ε}
• ball_eq' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedCommGroup E] (y : E) (ε : ℝ) : Metric.ball y ε = {x | ‖x / y‖ < ε}
• mem_ball_one_iff 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedGroup E] {a : E} {r : ℝ} : a ∈ Metric.ball 1 r ↔ ‖a‖ < r
• mem_ball_zero_iff 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddGroup E] {a : E} {r : ℝ} : a ∈ Metric.ball 0 r ↔ ‖a‖ < r
• mem_ball_iff_norm 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : b ∈ Metric.ball a r ↔ ‖b - a‖ < r
• mem_ball_iff_norm' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : b ∈ Metric.ball a r ↔ ‖a - b‖ < r
• mem_ball_iff_norm'' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} : b ∈ Metric.ball a r ↔ ‖b / a‖ < r
• mem_ball_iff_norm''' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} : b ∈ Metric.ball a r ↔ ‖a / b‖ < r
• add_mem_ball_iff_norm 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : a + b ∈ Metric.ball a r ↔ ‖b‖ < r
• mul_mem_ball_iff_norm 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} : a * b ∈ Metric.ball a r ↔ ‖b‖ < r
• ball_eq_norm_inv_mul_lt 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedGroup E] (y : E) (ε : ℝ) : Metric.ball y ε = {x | ‖x⁻¹ * y‖ < ε}
• ball_eq_norm_neg_add_lt 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddGroup E] (y : E) (ε : ℝ) : Metric.ball y ε = {x | ‖-x + y‖ < ε}
• mem_ball_iff_norm_inv_mul_lt 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedGroup E] {a b : E} {r : ℝ} : b ∈ Metric.ball a r ↔ ‖b⁻¹ * a‖ < r
• mem_ball_iff_norm_inv_mul_lt' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedGroup E] {a b : E} {r : ℝ} : b ∈ Metric.ball a r ↔ ‖a⁻¹ * b‖ < r
• mem_ball_iff_norm_neg_add_lt 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddGroup E] {a b : E} {r : ℝ} : b ∈ Metric.ball a r ↔ ‖-b + a‖ < r
• mem_ball_iff_norm_neg_add_lt' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddGroup E] {a b : E} {r : ℝ} : b ∈ Metric.ball a r ↔ ‖-a + b‖ < r
• setOf_div_mem_ball_eq_ball'' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedCommGroup E] {a : E} {r : ℝ} : {x | x / a ∈ Metric.ball 1 r} = Metric.ball a r
• setOf_sub_mem_ball_eq_ball 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddCommGroup E] {a : E} {r : ℝ} : {x | x - a ∈ Metric.ball 0 r} = Metric.ball a r
• preimage_add_ball 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddCommGroup E] (a b : E) (r : ℝ) : (fun x => b + x) ⁻¹' Metric.ball a r = Metric.ball (a - b) r
• preimage_mul_ball 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedCommGroup E] (a b : E) (r : ℝ) : (fun x => b * x) ⁻¹' Metric.ball a r = Metric.ball (a / b) r
• smul_ball'' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} : a • Metric.ball b r = Metric.ball (a • b) r
• vadd_ball'' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : a +ᵥ Metric.ball b r = Metric.ball (a +ᵥ b) r
• add_mem_ball_add_iff 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} {c : E} : a + c ∈ Metric.ball (b + c) r ↔ a ∈ Metric.ball b r
• mul_mem_ball_mul_iff 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} {c : E} : a * c ∈ Metric.ball (b * c) r ↔ a ∈ Metric.ball b r
• nsmul_mem_ball 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} {n : ℕ} (hn : 0 < n) (h : a ∈ Metric.ball b r) : n • a ∈ Metric.ball (n • b) (n • r)
• pow_mem_ball 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} {n : ℕ} (hn : 0 < n) (h : a ∈ Metric.ball b r) : a ^ n ∈ Metric.ball (b ^ n) (n • r)
• Metric.isBounded_ball 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} {x : α} {r : ℝ} [PseudoMetricSpace α] : Bornology.IsBounded (Metric.ball x r)
• Metric.hasAntitoneBasis_cobounded_compl_ball 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} [PseudoMetricSpace α] (c : α) : (Bornology.cobounded α).HasAntitoneBasis fun r => (Metric.ball c r)ᶜ
• Metric.hasBasis_cobounded_compl_ball 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} [PseudoMetricSpace α] (c : α) : (Bornology.cobounded α).HasBasis (fun x => True) fun r => (Metric.ball c r)ᶜ
• Bornology.IsBounded.subset_ball 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} {s : Set α} [PseudoMetricSpace α] (h : Bornology.IsBounded s) (c : α) : ∃ r, s ⊆ Metric.ball c r
• Metric.isBounded_iff_subset_ball 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} {s : Set α} [PseudoMetricSpace α] (c : α) : Bornology.IsBounded s ↔ ∃ r, s ⊆ Metric.ball c r
• Bornology.IsBounded.subset_ball_lt 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} {s : Set α} [PseudoMetricSpace α] (h : Bornology.IsBounded s) (a : ℝ) (c : α) : ∃ r, a < r ∧ s ⊆ Metric.ball c r
• Metric.diam_ball 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} {x : α} [PseudoMetricSpace α] {r : ℝ} (h : 0 ≤ r) : Metric.diam (Metric.ball x r) ≤ 2 * r
• Int.preimage_ball 📋 Mathlib.Topology.Instances.Int
  (x : ℤ) (r : ℝ) : Int.cast ⁻¹' Metric.ball (↑x) r = Metric.ball x r
• Int.ball_eq_Ioo 📋 Mathlib.Topology.Instances.Int
  (x : ℤ) (r : ℝ) : Metric.ball x r = Set.Ioo ⌊↑x - r⌋ ⌈↑x + r⌉
• Nat.preimage_ball 📋 Mathlib.Topology.Instances.Nat
  (x : ℕ) (r : ℝ) : Nat.cast ⁻¹' Metric.ball (↑x) r = Metric.ball x r
• Isometry.mapsTo_ball 📋 Mathlib.Topology.MetricSpace.Isometry
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} (hf : Isometry f) (x : α) (r : ℝ) : Set.MapsTo f (Metric.ball x r) (Metric.ball (f x) r)
• Isometry.preimage_ball 📋 Mathlib.Topology.MetricSpace.Isometry
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} (hf : Isometry f) (x : α) (r : ℝ) : f ⁻¹' Metric.ball (f x) r = Metric.ball x r
• IsometryEquiv.image_ball 📋 Mathlib.Topology.MetricSpace.Isometry
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β) (x : α) (r : ℝ) : ⇑h '' Metric.ball x r = Metric.ball (h x) r
• IsometryEquiv.preimage_ball 📋 Mathlib.Topology.MetricSpace.Isometry
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β) (x : β) (r : ℝ) : ⇑h ⁻¹' Metric.ball x r = Metric.ball (h.symm x) r
• LipschitzWith.mapsTo_ball 📋 Mathlib.Topology.MetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) (hK : K ≠ 0) (x : α) (r : ℝ) : Set.MapsTo f (Metric.ball x r) (Metric.ball (f x) (↑K * r))
• Metric.preimage_add_left_ball 📋 Mathlib.Topology.MetricSpace.IsometricSMul
  {G : Type v} [AddGroup G] [PseudoMetricSpace G] [IsIsometricVAdd G G] (a b : G) (r : ℝ) : (fun x => a + x) ⁻¹' Metric.ball b r = Metric.ball (-a + b) r
• Metric.preimage_mul_left_ball 📋 Mathlib.Topology.MetricSpace.IsometricSMul
  {G : Type v} [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G] (a b : G) (r : ℝ) : (fun x => a * x) ⁻¹' Metric.ball b r = Metric.ball (a⁻¹ * b) r
• Metric.preimage_add_right_ball 📋 Mathlib.Topology.MetricSpace.IsometricSMul
  {G : Type v} [AddGroup G] [PseudoMetricSpace G] [IsIsometricVAdd Gᵃᵒᵖ G] (a b : G) (r : ℝ) : (fun x => x + a) ⁻¹' Metric.ball b r = Metric.ball (b - a) r
• Metric.preimage_mul_right_ball 📋 Mathlib.Topology.MetricSpace.IsometricSMul
  {G : Type v} [Group G] [PseudoMetricSpace G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ) : (fun x => x * a) ⁻¹' Metric.ball b r = Metric.ball (b / a) r
• Metric.smul_ball 📋 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.ball x r = Metric.ball (c • x) r
• Metric.vadd_ball 📋 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.ball x r = Metric.ball (c +ᵥ x) r
• Metric.preimage_smul_ball 📋 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.ball x r = Metric.ball (c⁻¹ • x) r
• Metric.preimage_vadd_ball 📋 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.ball x r = Metric.ball (-c +ᵥ x) r
• LatticeOrderedAddCommGroup.isSolid_ball 📋 Mathlib.Analysis.Normed.Order.Lattice
  {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] (r : ℝ) : LatticeOrderedAddCommGroup.IsSolid (Metric.ball 0 r)
• Dilation.mapsTo_ball 📋 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.ball x r') (Metric.ball (f x) (↑(Dilation.ratio f) * r'))
• Metric.smul_image_ball 📋 Mathlib.Analysis.Normed.MulAction
  {α : Type u_1} {β : Type u_2} [NormedDivisionRing α] [SeminormedAddCommGroup β] [Module α β] [NormSMulClass α β] {s : α} (hs : s ≠ 0) (x : β) (ε : ℝ) : (fun x => s • x) '' Metric.ball x ε = Metric.ball (s • x) (‖s‖ * ε)
• Metric.diam_ball_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.ball x r) = 2 * r
• MeasureTheory.measure_ball_ne_top 📋 Mathlib.MeasureTheory.Measure.Typeclasses.Finite
  {α : Type u_1} {m0 : MeasurableSpace α} [PseudoMetricSpace α] [ProperSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {x : α} {r : ℝ} : μ (Metric.ball x r) ≠ ⊤
• MeasureTheory.measure_ball_lt_top 📋 Mathlib.MeasureTheory.Measure.Typeclasses.Finite
  {α : Type u_1} {m0 : MeasurableSpace α} [PseudoMetricSpace α] [ProperSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {x : α} {r : ℝ} : μ (Metric.ball x r) < ⊤
• MeasureTheory.exists_pos_ball 📋 Mathlib.MeasureTheory.Measure.Typeclasses.Finite
  {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PseudoMetricSpace α] (x : α) (hμ : μ ≠ 0) : ∃ n, 0 < μ (Metric.ball x ↑n)
• MeasureTheory.exists_pos_preimage_ball 📋 Mathlib.MeasureTheory.Measure.Typeclasses.Finite
  {α : Type u_1} {δ : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PseudoMetricSpace δ] (f : α → δ) (x : δ) (hμ : μ ≠ 0) : ∃ n, 0 < μ (f ⁻¹' Metric.ball x ↑n)
• Metric.ball_infDist_compl_subset 📋 Mathlib.Topology.MetricSpace.HausdorffDistance
  {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} : Metric.ball x (Metric.infDist x sᶜ) ⊆ s
• Metric.ball_infDist_subset_compl 📋 Mathlib.Topology.MetricSpace.HausdorffDistance
  {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} : Metric.ball x (Metric.infDist x s) ⊆ sᶜ
• Metric.disjoint_ball_infDist 📋 Mathlib.Topology.MetricSpace.HausdorffDistance
  {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} : Disjoint (Metric.ball x (Metric.infDist x s)) s
• Metric.thickening_singleton 📋 Mathlib.Topology.MetricSpace.Thickening
  {X : Type u} [PseudoMetricSpace X] (δ : ℝ) (x : X) : Metric.thickening δ {x} = Metric.ball x δ
• Metric.ball_subset_thickening 📋 Mathlib.Topology.MetricSpace.Thickening
  {X : Type u} [PseudoMetricSpace X] {x : X} {E : Set X} (hx : x ∈ E) (δ : ℝ) : Metric.ball x δ ⊆ Metric.thickening δ E
• Metric.thickening_ball 📋 Mathlib.Topology.MetricSpace.Thickening
  {α : Type u_2} [PseudoMetricSpace α] (x : α) (ε δ : ℝ) : Metric.thickening ε (Metric.ball x δ) ⊆ Metric.ball x (ε + δ)
• Metric.thickening_eq_biUnion_ball 📋 Mathlib.Topology.MetricSpace.Thickening
  {X : Type u} [PseudoMetricSpace X] {δ : ℝ} {E : Set X} : Metric.thickening δ E = ⋃ x ∈ E, Metric.ball x δ
• measurableSet_ball 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
  {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {x : α} {ε : ℝ} : MeasurableSet (Metric.ball x ε)
• Real.totallyBounded_ball 📋 Mathlib.Topology.Instances.Real.Lemmas
  (x ε : ℝ) : TotallyBounded (Metric.ball x ε)
• Metric.measure_ball_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.ball x r)
• LinearIsometry.preimage_ball 📋 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.ball (f x) r = Metric.ball x r
• LinearIsometryEquiv.image_ball 📋 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.ball x r = Metric.ball (e x) r
• LinearIsometryEquiv.preimage_ball 📋 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.ball x r = Metric.ball (e.symm x) r
• Metric.star_ball 📋 Mathlib.Analysis.CStarAlgebra.Basic
  {E : Type u_2} [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] (x : E) (r : ℝ) : star (Metric.ball x r) = Metric.ball (star x) r
• Complex.ball_one_subset_slitPlane 📋 Mathlib.Analysis.Complex.Basic
  : Metric.ball 1 1 ⊆ Complex.slitPlane
• inv_ball 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : (Metric.ball x δ)⁻¹ = Metric.ball x⁻¹ δ
• neg_ball 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : -Metric.ball x δ = Metric.ball (-x) δ
• div_ball_one 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) : s / Metric.ball 1 δ = Metric.thickening δ s
• sub_ball_zero 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) : s - Metric.ball 0 δ = Metric.thickening δ s
• ball_div_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) : Metric.ball x δ / {y} = Metric.ball (x / y) δ
• ball_sub_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) : Metric.ball x δ - {y} = Metric.ball (x - y) δ
• singleton_div_ball 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) : {x} / Metric.ball y δ = Metric.ball (x / y) δ
• singleton_div_ball_one 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : {x} / Metric.ball 1 δ = Metric.ball x δ
• singleton_sub_ball 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) : {x} - Metric.ball y δ = Metric.ball (x - y) δ
• singleton_sub_ball_zero 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : {x} - Metric.ball 0 δ = Metric.ball x δ
• add_ball_zero 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) : s + Metric.ball 0 δ = Metric.thickening δ s
• ball_add_zero 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) : Metric.ball 0 δ + s = Metric.thickening δ s
• ball_mul_one 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) : Metric.ball 1 δ * s = Metric.thickening δ s
• mul_ball_one 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) : s * Metric.ball 1 δ = Metric.thickening δ s
• smul_ball_one 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : x • Metric.ball 1 δ = Metric.ball x δ
• vadd_ball_zero 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : x +ᵥ Metric.ball 0 δ = Metric.ball x δ
• ball_one_mul_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : Metric.ball 1 δ * {x} = Metric.ball x δ
• ball_zero_add_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : Metric.ball 0 δ + {x} = Metric.ball x δ
• singleton_add_ball_zero 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : {x} + Metric.ball 0 δ = Metric.ball x δ
• singleton_mul_ball_one 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : {x} * Metric.ball 1 δ = Metric.ball x δ
• ball_add_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) : Metric.ball x δ + {y} = Metric.ball (x + y) δ
• ball_mul_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) : Metric.ball x δ * {y} = Metric.ball (x * y) δ
• singleton_add_ball 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) : {x} + Metric.ball y δ = Metric.ball (x + y) δ
• singleton_mul_ball 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) : {x} * Metric.ball y δ = Metric.ball (x * y) δ
• ball_div_one 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) : Metric.ball 1 δ / s = Metric.thickening δ s⁻¹
• ball_one_div_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : Metric.ball 1 δ / {x} = Metric.ball x⁻¹ δ
• ball_sub_zero 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) : Metric.ball 0 δ - s = Metric.thickening δ (-s)
• ball_zero_sub_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : Metric.ball 0 δ - {x} = Metric.ball (-x) δ
• add_ball 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) (x : E) : s + Metric.ball x δ = x +ᵥ Metric.thickening δ s
• ball_add 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) (x : E) : Metric.ball x δ + s = x +ᵥ Metric.thickening δ s
• ball_mul 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) (x : E) : Metric.ball x δ * s = x • Metric.thickening δ s
• mul_ball 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) (x : E) : s * Metric.ball x δ = x • Metric.thickening δ s
• div_ball 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) (x : E) : s / Metric.ball x δ = x⁻¹ • Metric.thickening δ s
• sub_ball 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) (x : E) : s - Metric.ball x δ = -x +ᵥ Metric.thickening δ s
• ball_div 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (s : Set E) (x : E) : Metric.ball x δ / s = x • Metric.thickening δ s⁻¹
• ball_sub 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) (x : E) : Metric.ball x δ - s = x +ᵥ Metric.thickening δ (-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_ball 📋 Mathlib.Analysis.Normed.Module.RCLike.Real
  {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) : frontier (Metric.ball 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
• interior_closedBall' 📋 Mathlib.Analysis.Normed.Module.RCLike.Real
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) (r : ℝ) : interior (Metric.closedBall x r) = Metric.ball x r
• cthickening_ball 📋 Mathlib.Analysis.Normed.Module.Ball.Pointwise
  {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ} (hε : 0 ≤ ε) (hδ : 0 < δ) (x : E) : Metric.cthickening ε (Metric.ball x δ) = Metric.closedBall x (ε + δ)
• thickening_ball 📋 Mathlib.Analysis.Normed.Module.Ball.Pointwise
  {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ} (hε : 0 < ε) (hδ : 0 < δ) (x : E) : Metric.thickening ε (Metric.ball x δ) = Metric.ball x (ε + δ)
• thickening_closedBall 📋 Mathlib.Analysis.Normed.Module.Ball.Pointwise
  {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ} (hε : 0 < ε) (hδ : 0 ≤ δ) (x : E) : Metric.thickening ε (Metric.closedBall x δ) = Metric.ball x (ε + δ)
• ball_sub_ball 📋 Mathlib.Analysis.Normed.Module.Ball.Pointwise
  {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ} (hε : 0 < ε) (hδ : 0 < δ) (a b : E) : Metric.ball a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)

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