Loogle!

Result

Found 377 declarations mentioning Metric.sphere. Of these, only the first 200 are shown.

• Metric.sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α
• Metric.sphere_isEmpty_of_subsingleton 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} [Subsingleton α] [NeZero ε] : IsEmpty ↑(Metric.sphere x ε)
• Metric.sphere_subset_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.sphere x ε ⊆ Metric.closedBall 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_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_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.nonneg_of_mem_sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} (hy : y ∈ Metric.sphere x ε) : 0 ≤ ε
• Metric.sphere_eq_empty_of_neg 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (hε : ε < 0) : Metric.sphere x ε = ∅
• Metric.sphere_union_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.sphere x ε ∪ Metric.ball x ε = Metric.closedBall x ε
• Metric.mem_sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} : y ∈ Metric.sphere x ε ↔ dist y x = ε
• Metric.mem_sphere' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} : y ∈ Metric.sphere x ε ↔ dist x y = ε
• Metric.sphere_eq_empty_of_subsingleton 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} [Subsingleton α] (hε : ε ≠ 0) : Metric.sphere x ε = ∅
• Metric.mem_sphere_comm 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} : x ∈ Metric.sphere y ε ↔ y ∈ Metric.sphere x ε
• Metric.ne_of_mem_sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} (h : y ∈ Metric.sphere x ε) (hε : ε ≠ 0) : y ≠ x
• Real.sphere_eq_pair 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  (x : ℝ) {r : ℝ} (hr : 0 ≤ r) : Metric.sphere x r = {x - r, x + r}
• Metric.sphere_disjoint_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Disjoint (Metric.sphere x ε) (Metric.ball x ε)
• Metric.subsingleton_sphere 📋 Mathlib.Topology.MetricSpace.Defs
  {γ : Type w} [MetricSpace γ] (x : γ) {r : ℝ} (hr : r ≤ 0) : (Metric.sphere x r).Subsingleton
• Metric.sphere_zero 📋 Mathlib.Topology.MetricSpace.Defs
  {γ : Type w} [MetricSpace γ] {x : γ} : Metric.sphere x 0 = {x}
• 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_sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : ℝ} : IsClosed (Metric.sphere x ε)
• Metric.closure_sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : ℝ} : closure (Metric.sphere x ε) = Metric.sphere x ε
• Metric.frontier_ball_subset_sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : ℝ} : frontier (Metric.ball x ε) ⊆ Metric.sphere x ε
• Metric.frontier_closedBall_subset_sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : ℝ} : frontier (Metric.closedBall x ε) ⊆ Metric.sphere x ε
• 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
• mem_sphere_one_iff_norm 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedGroup E] {a : E} {r : ℝ} : a ∈ Metric.sphere 1 r ↔ ‖a‖ = r
• mem_sphere_zero_iff_norm 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddGroup E] {a : E} {r : ℝ} : a ∈ Metric.sphere 0 r ↔ ‖a‖ = r
• mem_sphere_iff_norm 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : b ∈ Metric.sphere a r ↔ ‖b - a‖ = r
• mem_sphere_iff_norm' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} : b ∈ Metric.sphere a r ↔ ‖b / a‖ = r
• mem_sphere_iff_norm_inv_mul_eq 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedGroup E] {a b : E} {r : ℝ} : b ∈ Metric.sphere a r ↔ ‖b⁻¹ * a‖ = r
• mem_sphere_iff_norm_neg_add_eq 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddGroup E] {a b : E} {r : ℝ} : b ∈ Metric.sphere a r ↔ ‖-b + a‖ = r
• setOf_div_mem_sphere_eq_sphere'' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedCommGroup E] {a : E} {r : ℝ} : {x | x / a ∈ Metric.sphere 1 r} = Metric.sphere a r
• setOf_sub_mem_sphere_eq_sphere 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddCommGroup E] {a : E} {r : ℝ} : {x | x - a ∈ Metric.sphere 0 r} = Metric.sphere a r
• preimage_add_sphere 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddCommGroup E] (a b : E) (r : ℝ) : (fun x => b + x) ⁻¹' Metric.sphere a r = Metric.sphere (a - b) r
• preimage_mul_sphere 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedCommGroup E] (a b : E) (r : ℝ) : (fun x => b * x) ⁻¹' Metric.sphere a r = Metric.sphere (a / b) r
• norm_eq_of_mem_sphere 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddGroup E] {r : ℝ} (x : ↑(Metric.sphere 0 r)) : ‖↑x‖ = r
• norm_eq_of_mem_sphere' 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedGroup E] {r : ℝ} (x : ↑(Metric.sphere 1 r)) : ‖↑x‖ = r
• ne_one_of_mem_sphere 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedGroup E] {r : ℝ} (hr : r ≠ 0) (x : ↑(Metric.sphere 1 r)) : ↑x ≠ 1
• ne_one_of_mem_unit_sphere 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedGroup E] (x : ↑(Metric.sphere 1 1)) : ↑x ≠ 1
• ne_zero_of_mem_sphere 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddGroup E] {r : ℝ} (hr : r ≠ 0) (x : ↑(Metric.sphere 0 r)) : ↑x ≠ 0
• ne_zero_of_mem_unit_sphere 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddGroup E] (x : ↑(Metric.sphere 0 1)) : ↑x ≠ 0
• isCompact_sphere 📋 Mathlib.Topology.MetricSpace.ProperSpace
  {α : Type u_2} [PseudoMetricSpace α] [ProperSpace α] (x : α) (r : ℝ) : IsCompact (Metric.sphere x r)
• Metric.sphere.compactSpace 📋 Mathlib.Topology.MetricSpace.ProperSpace
  {α : Type u_2} [PseudoMetricSpace α] [ProperSpace α] (x : α) (r : ℝ) : CompactSpace ↑(Metric.sphere x r)
• Metric.isBounded_sphere 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} {x : α} {r : ℝ} [PseudoMetricSpace α] : Bornology.IsBounded (Metric.sphere x r)
• Isometry.mapsTo_sphere 📋 Mathlib.Topology.MetricSpace.Isometry
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} (hf : Isometry f) (x : α) (r : ℝ) : Set.MapsTo f (Metric.sphere x r) (Metric.sphere (f x) r)
• Isometry.preimage_sphere 📋 Mathlib.Topology.MetricSpace.Isometry
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} (hf : Isometry f) (x : α) (r : ℝ) : f ⁻¹' Metric.sphere (f x) r = Metric.sphere x r
• IsometryEquiv.image_sphere 📋 Mathlib.Topology.MetricSpace.Isometry
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β) (x : α) (r : ℝ) : ⇑h '' Metric.sphere x r = Metric.sphere (h x) r
• IsometryEquiv.preimage_sphere 📋 Mathlib.Topology.MetricSpace.Isometry
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β) (x : β) (r : ℝ) : ⇑h ⁻¹' Metric.sphere x r = Metric.sphere (h.symm x) r
• Metric.smul_sphere 📋 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.sphere x r = Metric.sphere (c • x) r
• Metric.vadd_sphere 📋 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.sphere x r = Metric.sphere (c +ᵥ x) r
• Metric.preimage_smul_sphere 📋 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.sphere x r = Metric.sphere (c⁻¹ • x) r
• Metric.preimage_vadd_sphere 📋 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.sphere x r = Metric.sphere (-c +ᵥ x) r
• Dilation.mapsTo_sphere 📋 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.sphere x r') (Metric.sphere (f x) (↑(Dilation.ratio f) * r'))
• Metric.smul_image_sphere 📋 Mathlib.Analysis.Normed.MulAction
  {α : Type u_1} {β : Type u_2} [NormedDivisionRing α] [SeminormedAddCommGroup β] [Module α β] [NormSMulClass α β] {s : α} (hs : s ≠ 0) (x : β) (ε : ℝ) : (fun x => s • x) '' Metric.sphere x ε = Metric.sphere (s • x) (‖s‖ * ε)
• Metric.diam_sphere_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.sphere x r) = 2 * r
• Complex.norm_sub_one_sq_eqOn_sphere 📋 Mathlib.Analysis.Complex.Norm
  : Set.EqOn (fun x => ‖x - 1‖ ^ 2) (fun z => 2 * (1 - z.re)) (Metric.sphere 0 1)
• LinearIsometry.preimage_sphere 📋 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.sphere (f x) r = Metric.sphere x r
• LinearIsometryEquiv.image_sphere 📋 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.sphere x r = Metric.sphere (e x) r
• LinearIsometryEquiv.preimage_sphere 📋 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.sphere x r = Metric.sphere (e.symm x) r
• Metric.star_sphere 📋 Mathlib.Analysis.CStarAlgebra.Basic
  {E : Type u_2} [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] (x : E) (r : ℝ) : star (Metric.sphere x r) = Metric.sphere (star x) r
• Complex.subset_slitPlane_iff_of_subset_sphere 📋 Mathlib.Analysis.Complex.Basic
  {r : ℝ} {s : Set ℂ} (hs : s ⊆ Metric.sphere 0 r) : s ⊆ Complex.slitPlane ↔ -↑r ∉ s
• inv_sphere 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : (Metric.sphere x δ)⁻¹ = Metric.sphere x⁻¹ δ
• neg_sphere 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : -Metric.sphere x δ = Metric.sphere (-x) δ
• singleton_div_sphere 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) : {x} / Metric.sphere y δ = Metric.sphere (x / y) δ
• singleton_div_sphere_one 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : {x} / Metric.sphere 1 δ = Metric.sphere x δ
• singleton_sub_sphere 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) : {x} - Metric.sphere y δ = Metric.sphere (x - y) δ
• singleton_sub_sphere_zero 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : {x} - Metric.sphere 0 δ = Metric.sphere x δ
• sphere_div_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) : Metric.sphere x δ / {y} = Metric.sphere (x / y) δ
• sphere_sub_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) : Metric.sphere x δ - {y} = Metric.sphere (x - y) δ
• smul_sphere_one 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : x • Metric.sphere 1 δ = Metric.sphere x δ
• vadd_sphere_zero 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : x +ᵥ Metric.sphere 0 δ = Metric.sphere x δ
• singleton_add_sphere_zero 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : {x} + Metric.sphere 0 δ = Metric.sphere x δ
• singleton_mul_sphere_one 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : {x} * Metric.sphere 1 δ = Metric.sphere x δ
• sphere_one_mul_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : Metric.sphere 1 δ * {x} = Metric.sphere x δ
• sphere_zero_add_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : Metric.sphere 0 δ + {x} = Metric.sphere x δ
• singleton_add_sphere 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) : {x} + Metric.sphere y δ = Metric.sphere (x + y) δ
• singleton_mul_sphere 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) : {x} * Metric.sphere y δ = Metric.sphere (x * y) δ
• sphere_add_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x y : E) : Metric.sphere x δ + {y} = Metric.sphere (x + y) δ
• sphere_mul_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x y : E) : Metric.sphere x δ * {y} = Metric.sphere (x * y) δ
• sphere_one_div_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedCommGroup E] (δ : ℝ) (x : E) : Metric.sphere 1 δ / {x} = Metric.sphere x⁻¹ δ
• sphere_zero_sub_singleton 📋 Mathlib.Analysis.Normed.Group.Pointwise
  {E : Type u_1} [SeminormedAddCommGroup E] (δ : ℝ) (x : E) : Metric.sphere 0 δ - {x} = Metric.sphere (-x) δ
• NormedSpace.sphere_nonempty 📋 Mathlib.Analysis.Normed.Module.RCLike.Real
  {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [NontrivialTopology E] {x : E} {r : ℝ} : (Metric.sphere x r).Nonempty ↔ 0 ≤ r
• interior_sphere' 📋 Mathlib.Analysis.Normed.Module.RCLike.Real
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) (r : ℝ) : interior (Metric.sphere x r) = ∅
• interior_sphere 📋 Mathlib.Analysis.Normed.Module.RCLike.Real
  {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) : interior (Metric.sphere 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
• 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
• frontier_sphere 📋 Mathlib.Analysis.Normed.Module.RCLike.Real
  {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) : frontier (Metric.sphere x r) = Metric.sphere x r
• frontier_closedBall' 📋 Mathlib.Analysis.Normed.Module.RCLike.Real
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) (r : ℝ) : frontier (Metric.closedBall x r) = Metric.sphere x r
• frontier_sphere' 📋 Mathlib.Analysis.Normed.Module.RCLike.Real
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) (r : ℝ) : frontier (Metric.sphere x r) = Metric.sphere x r
• set_smul_sphere_zero 📋 Mathlib.Analysis.Normed.Module.Ball.Pointwise
  {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set 𝕜} (hs : 0 ∉ s) (r : ℝ) : s • Metric.sphere 0 r = (fun x => ‖x‖) ⁻¹' (fun x => ‖x‖ * r) '' s
• Ioo_smul_sphere_zero 📋 Mathlib.Analysis.Normed.Module.Ball.Pointwise
  {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {a b r : ℝ} (ha : 0 ≤ a) (hr : 0 < r) : Set.Ioo a b • Metric.sphere 0 r = Metric.ball 0 (b * r) \ Metric.closedBall 0 (a * r)
• smul_sphere' 📋 Mathlib.Analysis.Normed.Module.Ball.Pointwise
  {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {c : 𝕜} (hc : c ≠ 0) (x : E) (r : ℝ) : c • Metric.sphere x r = Metric.sphere (c • x) (‖c‖ * r)
• smul_sphere 📋 Mathlib.Analysis.Normed.Module.Ball.Pointwise
  {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [Nontrivial E] (c : 𝕜) (x : E) {r : ℝ} (hr : 0 ≤ r) : c • Metric.sphere x r = Metric.sphere (c • x) (‖c‖ * r)
• Complex.range_exp_mul_I 📋 Mathlib.Analysis.SpecialFunctions.Complex.Arg
  : (Set.range fun x => Complex.exp (↑x * Complex.I)) = Metric.sphere 0 1
• Complex.image_exp_Ioc_eq_sphere 📋 Mathlib.Analysis.SpecialFunctions.Complex.Arg
  : (fun θ => Complex.exp (↑θ * Complex.I)) '' Set.Ioc (-Real.pi) Real.pi = Metric.sphere 0 1
• convexHull_sphere_eq_closedBall 📋 Mathlib.Analysis.Normed.Module.Convex
  {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [Nontrivial F] (x : F) {r : ℝ} (hr : 0 ≤ r) : (convexHull ℝ) (Metric.sphere x r) = Metric.closedBall x r
• sphere_subset_range_iff_surjective 📋 Mathlib.Analysis.Normed.Operator.Basic
  {𝕜 : Type u_1} {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] {F' : Type u_9} {𝓕' : Type u_10} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [Nontrivial F'] {τ : 𝕜 →+* ℝ} [FunLike 𝓕' E F'] [SemilinearMapClass 𝓕' τ E F'] [RingHomSurjective τ] {f : 𝓕'} {x : F'} {r : ℝ} (hr : 0 < r) : Metric.sphere x r ⊆ Set.range ⇑f ↔ Function.Surjective ⇑f
• ContinuousLinearMap.sSup_sphere_eq_norm 📋 Mathlib.Analysis.Normed.Operator.NNNorm
  {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [NormedAlgebra ℝ 𝕜] (f : E →SL[σ₁₂] F) : sSup ((fun x => ‖f x‖) '' Metric.sphere 0 1) = ‖f‖
• ContinuousLinearMap.sSup_sphere_eq_nnnorm 📋 Mathlib.Analysis.Normed.Operator.NNNorm
  {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [NormedAlgebra ℝ 𝕜] (f : E →SL[σ₁₂] F) : sSup ((fun x => ‖f x‖₊) '' Metric.sphere 0 1) = ‖f‖₊
• NormedSpace.sphere_nonempty_rclike 📋 Mathlib.Analysis.Normed.Module.RCLike.Basic
  (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [Nontrivial E] {r : ℝ} (hr : 0 ≤ r) : Nonempty ↑(Metric.sphere 0 r)
• LinearMap.bound_of_sphere_bound 📋 Mathlib.Analysis.Normed.Module.RCLike.Basic
  {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] 𝕜) (h : ∀ z ∈ Metric.sphere 0 r, ‖f z‖ ≤ c) (z : E) : ‖f z‖ ≤ c / r * ‖z‖
• EuclideanSpace.sphere_zero_eq 📋 Mathlib.Analysis.InnerProductSpace.PiL2
  {n : Type u_7} [Fintype n] (r : ℝ) (hr : 0 ≤ r) : Metric.sphere 0 r = {x | ∑ i, x.ofLp i ^ 2 = r ^ 2}
• MeasureTheory.Measure.addHaar_sphere 📋 Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] [Nontrivial E] (x : E) (r : ℝ) : μ (Metric.sphere x r) = 0
• MeasureTheory.Measure.addHaar_sphere_of_ne_zero 📋 Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (x : E) {r : ℝ} (hr : r ≠ 0) : μ (Metric.sphere x r) = 0
• circleMap_mem_sphere' 📋 Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
  (c : ℂ) (R θ : ℝ) : circleMap c R θ ∈ Metric.sphere c |R|
• circleMap_mem_sphere 📋 Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
  (c : ℂ) {R : ℝ} (hR : 0 ≤ R) (θ : ℝ) : circleMap c R θ ∈ Metric.sphere c R
• exists_ball_forall_le_norm_circleMap_sub 📋 Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
  {R : ℝ} {c w : ℂ} (hw : w ∉ Metric.sphere c |R|) : ∃ d > 0, ∀ x ∈ Metric.ball w d, ∀ (θ : ℝ), d ≤ ‖circleMap c R θ - x‖
• range_circleMap 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  (c : ℂ) (R : ℝ) : Set.range (circleMap c R) = Metric.sphere c |R|
• circleIntegrable_congr 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {E : Type u_1} [NormedAddCommGroup E] {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → E} (hf : Set.EqOn f₁ f₂ (Metric.sphere c |R|)) : CircleIntegrable f₁ c R ↔ CircleIntegrable f₂ c R
• crcleIntegrable_congr 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {E : Type u_1} [NormedAddCommGroup E] {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → E} (hf : Set.EqOn f₁ f₂ (Metric.sphere c |R|)) : CircleIntegrable f₁ c R ↔ CircleIntegrable f₂ c R
• ContinuousOn.circleIntegrable' 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {c : ℂ} {R : ℝ} (hf : ContinuousOn f (Metric.sphere c |R|)) : CircleIntegrable f c R
• circleIntegrable_sub_inv_iff 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {c w : ℂ} {R : ℝ} : CircleIntegrable (fun z => (z - w)⁻¹) c R ↔ R = 0 ∨ w ∉ Metric.sphere c |R|
• CircleIntegrable.congr_codiscreteWithin 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {E : Type u_1} [NormedAddCommGroup E] {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → E} (hf : f₁ =ᶠ[Filter.codiscreteWithin (Metric.sphere c |R|)] f₂) (hf₁ : CircleIntegrable f₁ c R) : CircleIntegrable f₂ c R
• circleIntegrable_congr_codiscreteWithin 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {E : Type u_1} [NormedAddCommGroup E] {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → E} (hf : f₁ =ᶠ[Filter.codiscreteWithin (Metric.sphere c |R|)] f₂) : CircleIntegrable f₁ c R ↔ CircleIntegrable f₂ c R
• ContinuousOn.circleIntegrable 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (hf : ContinuousOn f (Metric.sphere c R)) : CircleIntegrable f c R
• image_circleMap_Ioc 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  (c : ℂ) (R : ℝ) : circleMap c R '' Set.Ioc 0 (2 * Real.pi) = Metric.sphere c |R|
• circleIntegral.integral_congr 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (h : Set.EqOn f g (Metric.sphere c R)) : ∮ (z : ℂ) in C(c, R), f z = ∮ (z : ℂ) in C(c, R), g z
• circleMap_preimage_codiscrete 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {c : ℂ} {R : ℝ} (hR : R ≠ 0) : Filter.map (circleMap c R) (Filter.codiscrete ℝ) ≤ Filter.codiscreteWithin (Metric.sphere c |R|)
• circleIntegrable_sub_zpow_iff 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {c w : ℂ} {R : ℝ} {n : ℤ} : CircleIntegrable (fun z => (z - w) ^ n) c R ↔ R = 0 ∨ 0 ≤ n ∨ w ∉ Metric.sphere c |R|
• circleIntegral.integral_sub_zpow_of_undef 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {n : ℤ} {c w : ℂ} {R : ℝ} (hn : n < 0) (hw : w ∈ Metric.sphere c |R|) : ∮ (z : ℂ) in C(c, R), (z - w) ^ n = 0
• circleIntegral.circleIntegral_congr_codiscreteWithin 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → ℂ} (hf : f₁ =ᶠ[Filter.codiscreteWithin (Metric.sphere c |R|)] f₂) (hR : R ≠ 0) : ∮ (z : ℂ) in C(c, R), f₁ z = ∮ (z : ℂ) in C(c, R), f₂ z
• CircleIntegrable.fun_continuousOn_mul 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {c : ℂ} {R : ℝ} {𝕜 : Type u_3} [NormedRing 𝕜] {f g : ℂ → 𝕜} (hf : CircleIntegrable f c R) (hg : ContinuousOn g (Metric.sphere c |R|)) : CircleIntegrable (fun i => g i * f i) c R
• CircleIntegrable.fun_mul_continuousOn 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {c : ℂ} {R : ℝ} {𝕜 : Type u_3} [NormedRing 𝕜] {f g : ℂ → 𝕜} (hf : CircleIntegrable f c R) (hg : ContinuousOn g (Metric.sphere c |R|)) : CircleIntegrable (fun i => f i * g i) c R
• CircleIntegrable.fun_mul_of_continuousOn 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {c : ℂ} {R : ℝ} {𝕜 : Type u_3} [NormedRing 𝕜] {f g : ℂ → 𝕜} (hf : CircleIntegrable f c R) (hg : ContinuousOn g (Metric.sphere c |R|)) : CircleIntegrable (fun i => g i * f i) c R
• CircleIntegrable.continuousOn_mul 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {c : ℂ} {R : ℝ} {𝕜 : Type u_3} [NormedRing 𝕜] {f g : ℂ → 𝕜} (hf : CircleIntegrable f c R) (hg : ContinuousOn g (Metric.sphere c |R|)) : CircleIntegrable (g * f) c R
• CircleIntegrable.mul_continuousOn 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {c : ℂ} {R : ℝ} {𝕜 : Type u_3} [NormedRing 𝕜] {f g : ℂ → 𝕜} (hf : CircleIntegrable f c R) (hg : ContinuousOn g (Metric.sphere c |R|)) : CircleIntegrable (f * g) c R
• CircleIntegrable.mul_of_continuousOn 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {c : ℂ} {R : ℝ} {𝕜 : Type u_3} [NormedRing 𝕜] {f g : ℂ → 𝕜} (hf : CircleIntegrable f c R) (hg : ContinuousOn g (Metric.sphere c |R|)) : CircleIntegrable (g * f) c R
• circleIntegral.norm_integral_le_of_norm_le_const' 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R C : ℝ} (hf : ∀ z ∈ Metric.sphere c |R|, ‖f z‖ ≤ C) : ‖∮ (z : ℂ) in C(c, R), f z‖ ≤ 2 * Real.pi * |R| * C
• circleIntegral.norm_integral_le_of_norm_le_const 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R C : ℝ} (hR : 0 ≤ R) (hf : ∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) : ‖∮ (z : ℂ) in C(c, R), f z‖ ≤ 2 * Real.pi * R * C
• TendstoUniformlyOn.tendsto_circleIntegral_of_continuousOn 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {ι : Type u_2} {f : ι → ℂ → E} {g : ℂ → E} {c : ℂ} {R : ℝ} {l : Filter ι} [l.IsCountablyGenerated] (hR : 0 ≤ R) (hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (Metric.sphere c R)) (h : TendstoUniformlyOn f g l (Metric.sphere c R)) : Filter.Tendsto (fun n => ∮ (z : ℂ) in C(c, R), f n z) l (nhds (∮ (z : ℂ) in C(c, R), g z))
• CircleIntegrable.sub_zpow_smul 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c w : ℂ} {R : ℝ} (n : ℤ) (hf : CircleIntegrable f c R) (hw : w ∉ Metric.sphere c |R|) : CircleIntegrable (fun z => (z - w) ^ n • f z) c R
• circleIntegral.integral_eq_zero_of_hasDerivWithinAt' 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f f' : ℂ → E} {c : ℂ} {R : ℝ} (h : ∀ z ∈ Metric.sphere c |R|, HasDerivWithinAt f (f' z) (Metric.sphere c |R|) z) : ∮ (z : ℂ) in C(c, R), f' z = 0
• circleIntegral.integral_eq_zero_of_hasDerivWithinAt 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f f' : ℂ → E} {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (h : ∀ z ∈ Metric.sphere c R, HasDerivWithinAt f (f' z) (Metric.sphere c R) z) : ∮ (z : ℂ) in C(c, R), f' z = 0
• circleIntegral.norm_integral_lt_of_norm_le_const_of_lt 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R C : ℝ} (hR : 0 < R) (hc : ContinuousOn f (Metric.sphere c R)) (hf : ∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) (hlt : ∃ z ∈ Metric.sphere c R, ‖f z‖ < C) : ‖∮ (z : ℂ) in C(c, R), f z‖ < 2 * Real.pi * R * C
• circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R C : ℝ} (hR : 0 ≤ R) (hf : ∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) : ‖(2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), f z‖ ≤ R * C
• CircleIntegrable.fun_continuousOn_smul 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {c : ℂ} {R : ℝ} {𝕜 : Type u_3} {F : Type u_4} [NormedRing 𝕜] [NormedAddCommGroup F] [Module 𝕜 F] [NormSMulClass 𝕜 F] {f : ℂ → F} {g : ℂ → 𝕜} (hf : CircleIntegrable f c R) (hg : ContinuousOn g (Metric.sphere c |R|)) : CircleIntegrable (fun i => g i • f i) c R
• CircleIntegrable.fun_smul_of_continuousOn 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {c : ℂ} {R : ℝ} {𝕜 : Type u_3} {F : Type u_4} [NormedRing 𝕜] [NormedAddCommGroup F] [Module 𝕜 F] [NormSMulClass 𝕜 F] {f : ℂ → F} {g : ℂ → 𝕜} (hf : CircleIntegrable f c R) (hg : ContinuousOn g (Metric.sphere c |R|)) : CircleIntegrable (fun i => g i • f i) c R
• CircleIntegrable.fun_smul_continuousOn 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {c : ℂ} {R : ℝ} {𝕜 : Type u_3} {F : Type u_4} [NormedRing 𝕜] [NormedAddCommGroup F] [Module 𝕜 F] [NormSMulClass 𝕜 F] {f : ℂ → 𝕜} {g : ℂ → F} (hf : CircleIntegrable f c R) (hg : ContinuousOn g (Metric.sphere c |R|)) : CircleIntegrable (fun i => f i • g i) c R
• CircleIntegrable.continuousOn_smul 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {c : ℂ} {R : ℝ} {𝕜 : Type u_3} {F : Type u_4} [NormedRing 𝕜] [NormedAddCommGroup F] [Module 𝕜 F] [NormSMulClass 𝕜 F] {f : ℂ → F} {g : ℂ → 𝕜} (hf : CircleIntegrable f c R) (hg : ContinuousOn g (Metric.sphere c |R|)) : CircleIntegrable (g • f) c R
• CircleIntegrable.smul_of_continuousOn 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {c : ℂ} {R : ℝ} {𝕜 : Type u_3} {F : Type u_4} [NormedRing 𝕜] [NormedAddCommGroup F] [Module 𝕜 F] [NormSMulClass 𝕜 F] {f : ℂ → F} {g : ℂ → 𝕜} (hf : CircleIntegrable f c R) (hg : ContinuousOn g (Metric.sphere c |R|)) : CircleIntegrable (g • f) c R
• CircleIntegrable.smul_continuousOn 📋 Mathlib.MeasureTheory.Integral.CircleIntegral
  {c : ℂ} {R : ℝ} {𝕜 : Type u_3} {F : Type u_4} [NormedRing 𝕜] [NormedAddCommGroup F] [Module 𝕜 F] [NormSMulClass 𝕜 F] {f : ℂ → 𝕜} {g : ℂ → F} (hf : CircleIntegrable f c R) (hg : ContinuousOn g (Metric.sphere c |R|)) : CircleIntegrable (f • g) c R
• Complex.hasDerivAt_circleIntegral_sub_inv_smul 📋 Mathlib.Analysis.Complex.CauchyIntegral
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {R : ℝ} {c w : ℂ} (hf : CircleIntegrable f c R) (hw : w ∉ Metric.sphere c |R|) : HasDerivAt (fun w => ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) (∮ (z : ℂ) in C(c, R), (z - w) ^ (-2) • f z) w
• Complex.hasDerivAt_circleIntegral_sub_zpow_smul 📋 Mathlib.Analysis.Complex.CauchyIntegral
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {R : ℝ} {c w : ℂ} {n : ℤ} (hf : CircleIntegrable f c R) (hw : w ∉ Metric.sphere c |R|) : HasDerivAt (fun w => ∮ (z : ℂ) in C(c, R), (z - w) ^ n • f z) (-↑n • ∮ (z : ℂ) in C(c, R), (z - w) ^ (n - 1) • f z) w
• Complex.norm_deriv_le_of_forall_mem_sphere_norm_le 📋 Mathlib.Analysis.Complex.Liouville
  {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] {c : ℂ} {R C : ℝ} {f : ℂ → F} (hR : 0 < R) (hd : DiffContOnCl ℂ f (Metric.ball c R)) (hC : ∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) : ‖deriv f c‖ ≤ C / R
• Complex.norm_iteratedDeriv_le_of_forall_mem_sphere_norm_le 📋 Mathlib.Analysis.Complex.Liouville
  {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {c : ℂ} {R C : ℝ} {f : ℂ → F} (n : ℕ) (hR : 0 < R) (hf : DiffContOnCl ℂ f (Metric.ball c R)) (hC : ∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) : ‖iteratedDeriv n f c‖ ≤ ↑n.factorial * C / R ^ n
• IsUltrametricDist.isClopen_sphere 📋 Mathlib.Topology.MetricSpace.Ultra.Basic
  {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] (x : X) {r : ℝ} (hr : r ≠ 0) : IsClopen (Metric.sphere x r)
• IsUltrametricDist.isOpen_sphere 📋 Mathlib.Topology.MetricSpace.Ultra.Basic
  {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] (x : X) {r : ℝ} (hr : r ≠ 0) : IsOpen (Metric.sphere x r)
• isPreconnected_sphere 📋 Mathlib.Analysis.Normed.Module.Connected
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : 1 < Module.rank ℝ E) (x : E) (r : ℝ) : IsPreconnected (Metric.sphere x r)
• isConnected_sphere 📋 Mathlib.Analysis.Normed.Module.Connected
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : 1 < Module.rank ℝ E) (x : E) {r : ℝ} (hr : 0 ≤ r) : IsConnected (Metric.sphere x r)
• isPathConnected_sphere 📋 Mathlib.Analysis.Normed.Module.Connected
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : 1 < Module.rank ℝ E) (x : E) {r : ℝ} (hr : 0 ≤ r) : IsPathConnected (Metric.sphere x r)
• spectrum.subset_circle_of_unitary 📋 Mathlib.Analysis.CStarAlgebra.Spectrum
  {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedRing E] [StarRing E] [CStarRing E] [NormedAlgebra 𝕜 E] [CompleteSpace E] {u : E} (h : u ∈ unitary E) : spectrum 𝕜 u ⊆ Metric.sphere 0 1
• Unitary.spectrum_subset_circle 📋 Mathlib.Analysis.CStarAlgebra.Spectrum
  {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedRing E] [StarRing E] [CStarRing E] [NormedAlgebra 𝕜 E] [CompleteSpace E] (u : ↥(unitary E)) : spectrum 𝕜 ↑u ⊆ Metric.sphere 0 1
• instInvolutiveNegElemSphereOfNat 📋 Mathlib.Analysis.Normed.Group.BallSphere
  {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} : InvolutiveNeg ↑(Metric.sphere 0 r)
• instContinuousNegElemSphereOfNat 📋 Mathlib.Analysis.Normed.Group.BallSphere
  {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} : ContinuousNeg ↑(Metric.sphere 0 r)
• coe_neg_sphere 📋 Mathlib.Analysis.Normed.Group.BallSphere
  {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} (v : ↑(Metric.sphere 0 r)) : ↑(-v) = -↑v
• Metric.unitSphere.instDiv 📋 Mathlib.Analysis.Normed.Field.UnitBall
  {𝕜 : Type u_1} [NormedDivisionRing 𝕜] : Div ↑(Metric.sphere 0 1)
• Metric.unitSphere.instGroup 📋 Mathlib.Analysis.Normed.Field.UnitBall
  {𝕜 : Type u_1} [NormedDivisionRing 𝕜] : Group ↑(Metric.sphere 0 1)
• Metric.unitSphere.instInv 📋 Mathlib.Analysis.Normed.Field.UnitBall
  {𝕜 : Type u_1} [NormedDivisionRing 𝕜] : Inv ↑(Metric.sphere 0 1)
• Metric.unitSphere.instZPow 📋 Mathlib.Analysis.Normed.Field.UnitBall
  {𝕜 : Type u_1} [NormedDivisionRing 𝕜] : Pow ↑(Metric.sphere 0 1) ℤ
• Metric.sphere.instCommGroup 📋 Mathlib.Analysis.Normed.Field.UnitBall
  {𝕜 : Type u_1} [NormedField 𝕜] : CommGroup ↑(Metric.sphere 0 1)
• Metric.unitSphere.instMonoid 📋 Mathlib.Analysis.Normed.Field.UnitBall
  {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] : Monoid ↑(Metric.sphere 0 1)
• Metric.unitSphere.instCommMonoid 📋 Mathlib.Analysis.Normed.Field.UnitBall
  {𝕜 : Type u_1} [SeminormedCommRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] : CommMonoid ↑(Metric.sphere 0 1)
• Submonoid.coe_unitSphere 📋 Mathlib.Analysis.Normed.Field.UnitBall
  (𝕜 : Type u_2) [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] : ↑(Submonoid.unitSphere 𝕜) = Metric.sphere 0 1
• Metric.sphere.instIsTopologicalGroup 📋 Mathlib.Analysis.Normed.Field.UnitBall
  {𝕜 : Type u_1} [NormedDivisionRing 𝕜] : IsTopologicalGroup ↑(Metric.sphere 0 1)
• Metric.sphere.instHasDistribNeg 📋 Mathlib.Analysis.Normed.Field.UnitBall
  {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] : HasDistribNeg ↑(Metric.sphere 0 1)
• unitSphereToUnits 📋 Mathlib.Analysis.Normed.Field.UnitBall
  (𝕜 : Type u_2) [NormedDivisionRing 𝕜] : ↑(Metric.sphere 0 1) →* 𝕜ˣ
• Metric.unitSphere.coe_inv 📋 Mathlib.Analysis.Normed.Field.UnitBall
  {𝕜 : Type u_1} [NormedDivisionRing 𝕜] (x : ↑(Metric.sphere 0 1)) : ↑x⁻¹ = (↑x)⁻¹
• Metric.sphere.instContinuousMul 📋 Mathlib.Analysis.Normed.Field.UnitBall
  {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] : ContinuousMul ↑(Metric.sphere 0 1)
• Metric.unitSphere.coe_one 📋 Mathlib.Analysis.Normed.Field.UnitBall
  {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] : ↑1 = 1
• Metric.unitSphere.coe_zpow 📋 Mathlib.Analysis.Normed.Field.UnitBall
  {𝕜 : Type u_1} [NormedDivisionRing 𝕜] (x : ↑(Metric.sphere 0 1)) (n : ℤ) : ↑(x ^ n) = ↑x ^ n
• Metric.unitSphere.coe_pow 📋 Mathlib.Analysis.Normed.Field.UnitBall
  {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] (x : ↑(Metric.sphere 0 1)) (n : ℕ) : ↑(x ^ n) = ↑x ^ n
• Metric.unitSphere.coe_div 📋 Mathlib.Analysis.Normed.Field.UnitBall
  {𝕜 : Type u_1} [NormedDivisionRing 𝕜] (x y : ↑(Metric.sphere 0 1)) : ↑(x / y) = ↑x / ↑y
• Metric.unitSphere.coe_mul 📋 Mathlib.Analysis.Normed.Field.UnitBall
  {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] (x y : ↑(Metric.sphere 0 1)) : ↑(x * y) = ↑x * ↑y
• unitSphereToUnits_injective 📋 Mathlib.Analysis.Normed.Field.UnitBall
  {𝕜 : Type u_1} [NormedDivisionRing 𝕜] : Function.Injective ⇑(unitSphereToUnits 𝕜)
• unitSphereToUnits_apply_coe 📋 Mathlib.Analysis.Normed.Field.UnitBall
  {𝕜 : Type u_1} [NormedDivisionRing 𝕜] (x : ↑(Metric.sphere 0 1)) : ↑((unitSphereToUnits 𝕜) x) = ↑x
• Metric.exists_isLocalMin_mem_ball 📋 Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
  {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [ProperSpace α] [TopologicalSpace β] [ConditionallyCompleteLinearOrder β] [OrderTopology β] {f : α → β} {a z : α} {r : ℝ} (hf : ContinuousOn f (Metric.closedBall a r)) (hz : z ∈ Metric.closedBall a r) (hf1 : ∀ z' ∈ Metric.sphere a r, f z < f z') : ∃ z ∈ Metric.ball a r, IsLocalMin f z
• Complex.norm_cderiv_le 📋 Mathlib.Analysis.Complex.LocallyUniformLimit
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {z : ℂ} {M r : ℝ} {f : ℂ → E} (hr : 0 < r) (hf : ∀ w ∈ Metric.sphere z r, ‖f w‖ ≤ M) : ‖Complex.cderiv r f z‖ ≤ M / r
• Complex.norm_cderiv_lt 📋 Mathlib.Analysis.Complex.LocallyUniformLimit
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {z : ℂ} {M r : ℝ} {f : ℂ → E} (hr : 0 < r) (hfM : ∀ w ∈ Metric.sphere z r, ‖f w‖ < M) (hf : ContinuousOn f (Metric.sphere z r)) : ‖Complex.cderiv r f z‖ < M / r
• Complex.cderiv_sub 📋 Mathlib.Analysis.Complex.LocallyUniformLimit
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {z : ℂ} {r : ℝ} {f g : ℂ → E} (hr : 0 < r) (hf : ContinuousOn f (Metric.sphere z r)) (hg : ContinuousOn g (Metric.sphere z r)) : Complex.cderiv r (f - g) z = Complex.cderiv r f z - Complex.cderiv r g z
• Complex.norm_cderiv_sub_lt 📋 Mathlib.Analysis.Complex.LocallyUniformLimit
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {z : ℂ} {M r : ℝ} {f g : ℂ → E} (hr : 0 < r) (hfg : ∀ w ∈ Metric.sphere z r, ‖f w - g w‖ < M) (hf : ContinuousOn f (Metric.sphere z r)) (hg : ContinuousOn g (Metric.sphere z r)) : ‖Complex.cderiv r f z - Complex.cderiv r g z‖ < M / r
• LipschitzWith.hasFDerivAt_of_hasLineDerivAt_of_closure 📋 Mathlib.Analysis.Calculus.Rademacher
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {C : NNReal} [FiniteDimensional ℝ E] {f : E → F} (hf : LipschitzWith C f) {s : Set E} (hs : Metric.sphere 0 1 ⊆ closure s) {L : E →L[ℝ] F} {x : E} (hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v) : HasFDerivAt f L x
• StrictConvexSpace.of_pairwise_sphere_norm_ne_two 📋 Mathlib.Analysis.Convex.StrictConvexSpace
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : (Metric.sphere 0 1).Pairwise fun x y => ‖x + y‖ ≠ 2) : StrictConvexSpace ℝ E
• instSMulElemSphereOfNatReal 📋 Mathlib.Analysis.Normed.Module.Ball.Action
  {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : SMul ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 r)
• instSMulElemSphereOfNatRealBall 📋 Mathlib.Analysis.Normed.Module.Ball.Action
  {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : SMul ↑(Metric.sphere 0 1) ↑(Metric.ball 0 r)
• instSMulElemSphereOfNatRealClosedBall 📋 Mathlib.Analysis.Normed.Module.Ball.Action
  {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : SMul ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 r)
• mulActionSphereBall 📋 Mathlib.Analysis.Normed.Module.Ball.Action
  {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : MulAction ↑(Metric.sphere 0 1) ↑(Metric.ball 0 r)
• mulActionSphereClosedBall 📋 Mathlib.Analysis.Normed.Module.Ball.Action
  {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : MulAction ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 r)
• mulActionSphereSphere 📋 Mathlib.Analysis.Normed.Module.Ball.Action
  {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : MulAction ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 r)
• ne_neg_of_mem_sphere 📋 Mathlib.Analysis.Normed.Module.Ball.Action
  (𝕜 : Type u_1) {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [CharZero 𝕜] {r : ℝ} (hr : r ≠ 0) (x : ↑(Metric.sphere 0 r)) : x ≠ -x
• ne_neg_of_mem_unit_sphere 📋 Mathlib.Analysis.Normed.Module.Ball.Action
  (𝕜 : Type u_1) {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [CharZero 𝕜] (x : ↑(Metric.sphere 0 1)) : x ≠ -x
• continuousSMul_sphere_ball 📋 Mathlib.Analysis.Normed.Module.Ball.Action
  {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : ContinuousSMul ↑(Metric.sphere 0 1) ↑(Metric.ball 0 r)
• continuousSMul_sphere_closedBall 📋 Mathlib.Analysis.Normed.Module.Ball.Action
  {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : ContinuousSMul ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 r)
• continuousSMul_sphere_sphere 📋 Mathlib.Analysis.Normed.Module.Ball.Action
  {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : ContinuousSMul ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 r)
• instSMulCommClass_sphere_ball_ball 📋 Mathlib.Analysis.Normed.Module.Ball.Action
  {𝕜 : Type u_1} {𝕜' : Type u_2} [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] : SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.ball 0 1) ↑(Metric.ball 0 1)
• instSMulCommClass_sphere_closedBall_ball 📋 Mathlib.Analysis.Normed.Module.Ball.Action
  {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [SMulCommClass 𝕜 𝕜' E] : SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)
• instSMulCommClass_sphere_closedBall_closedBall 📋 Mathlib.Analysis.Normed.Module.Ball.Action
  {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [SMulCommClass 𝕜 𝕜' E] : SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)
• instSMulCommClass_sphere_sphere_ball 📋 Mathlib.Analysis.Normed.Module.Ball.Action
  {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [SMulCommClass 𝕜 𝕜' E] : SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 1) ↑(Metric.ball 0 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