Loogle!

Result

Found 1401 declarations mentioning PseudoEMetricSpace. Of these, only the first 200 are shown.

• PseudoEMetricSpace 📋 Mathlib.Topology.EMetricSpace.Defs
  (α : Type u) : Type u
• EMetricSpace.toPseudoEMetricSpace 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [self : EMetricSpace α] : PseudoEMetricSpace α
• PseudoEMetricSpace.toEDist 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [self : PseudoEMetricSpace α] : EDist α
• PseudoEMetricSpace.toUniformSpace 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [self : PseudoEMetricSpace α] : UniformSpace α
• instPseudoEMetricSpaceAdditive 📋 Mathlib.Topology.EMetricSpace.Defs
  {X : Type u_1} [PseudoEMetricSpace X] : PseudoEMetricSpace (Additive X)
• instPseudoEMetricSpaceMultiplicative 📋 Mathlib.Topology.EMetricSpace.Defs
  {X : Type u_1} [PseudoEMetricSpace X] : PseudoEMetricSpace (Multiplicative X)
• instPseudoEMetricSpaceOrderDual 📋 Mathlib.Topology.EMetricSpace.Defs
  {X : Type u_1} [PseudoEMetricSpace X] : PseudoEMetricSpace Xᵒᵈ
• instPseudoEMetricSpaceULift 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} [PseudoEMetricSpace α] : PseudoEMetricSpace (ULift.{u_3, u_2} α)
• PseudoEMetricSpace.induced 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} {β : Type u_3} (f : α → β) (m : PseudoEMetricSpace β) : PseudoEMetricSpace α
• instPseudoEMetricSpaceSubtype 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} {p : α → Prop} [PseudoEMetricSpace α] : PseudoEMetricSpace (Subtype p)
• Prod.pseudoEMetricSpaceMax 📋 Mathlib.Topology.EMetricSpace.Defs
  {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] : PseudoEMetricSpace (α × β)
• PseudoEMetricSpace.toWeakPseudoEMetricSpace 📋 Mathlib.Topology.EMetricSpace.Defs
  (α : Type u) [inst : PseudoEMetricSpace α] : WeakPseudoEMetricSpace α
• EMetric.instIsCountablyGeneratedUniformity 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [PseudoEMetricSpace α] : (uniformity α).IsCountablyGenerated
• Metric.isOpen_eball 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {x : α} [PseudoEMetricSpace α] {r : ENNReal} : IsOpen (Metric.eball x r)
• PseudoEMetricSpace.edist_self 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [self : PseudoEMetricSpace α] (x : α) : edist x x = 0
• PseudoEMetricSpace.ext 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} {m m' : PseudoEMetricSpace α} (h : m.toEDist = m'.toEDist) : m = m'
• PseudoEMetricSpace.ext_iff 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} {m m' : PseudoEMetricSpace α} : m = m' ↔ m.toEDist = m'.toEDist
• PseudoEMetricSpace.replaceUniformity 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} [U : UniformSpace α] (m : PseudoEMetricSpace α) (H : uniformity α = uniformity α) : PseudoEMetricSpace α
• PseudoEMetricSpace.edist_comm 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [self : PseudoEMetricSpace α] (x y : α) : edist x y = edist y x
• uniformSpace_edist 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [PseudoEMetricSpace α] : PseudoEMetricSpace.toUniformSpace = uniformSpaceOfEDist edist ⋯ ⋯ ⋯
• EMetricSpace.mk 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [toPseudoEMetricSpace : PseudoEMetricSpace α] (eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y) : EMetricSpace α
• Metric.isClosed_eball_top 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} [PseudoEMetricSpace α] {x : α} : IsClosed (Metric.eball x ⊤)
• Metric.nhds_basis_eball 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {x : α} [PseudoEMetricSpace α] : (nhds x).HasBasis (fun ε => 0 < ε) (Metric.eball x)
• PseudoEMetricSpace.edist_triangle 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [self : PseudoEMetricSpace α] (x y z : α) : edist x z ≤ edist x y + edist y z
• Metric.nhds_basis_closedEBall 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_4} [PseudoEMetricSpace α] {x : α} : (nhds x).HasBasis (fun ε => 0 < ε) (Metric.closedEBall x)
• Metric.nhdsWithin_basis_eball 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {x : α} {s : Set α} [PseudoEMetricSpace α] : (nhdsWithin x s).HasBasis (fun ε => 0 < ε) fun ε => Metric.eball x ε ∩ s
• Metric.closedEBall_mem_nhds 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} [PseudoEMetricSpace α] (x : α) {ε : ENNReal} (ε0 : 0 < ε) : Metric.closedEBall x ε ∈ nhds x
• Metric.eball_mem_nhds 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} [PseudoEMetricSpace α] (x : α) {ε : ENNReal} (ε0 : 0 < ε) : Metric.eball x ε ∈ nhds x
• ULift.edist_up_up 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} [PseudoEMetricSpace α] (x y : α) : edist { down := x } { down := y } = edist x y
• PseudoEMetricSpace.ofEDist 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} (edist : α → α → ENNReal) (edist_self : ∀ (x : α), edist x x = 0) (edist_comm : ∀ (x y : α), edist x y = edist y x) (edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z) : PseudoEMetricSpace α
• ULift.edist_eq 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} [PseudoEMetricSpace α] (x y : ULift.{u_3, u_2} α) : edist x y = edist x.down y.down
• EMetric.dense_iff 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} [PseudoEMetricSpace α] {s : Set α} : Dense s ↔ ∀ (x : α), ∀ r > 0, (Metric.eball x r ∩ s).Nonempty
• EMetric.isOpen_iff 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {s : Set α} [PseudoEMetricSpace α] : IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, Metric.eball x ε ⊆ s
• EMetric.mem_nhds_iff 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {x : α} {s : Set α} [PseudoEMetricSpace α] : s ∈ nhds x ↔ ∃ ε > 0, Metric.eball x ε ⊆ s
• Metric.nhdsWithin_basis_closedEBall 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_4} [PseudoEMetricSpace α] {s : Set α} {x : α} : (nhdsWithin x s).HasBasis (fun ε => 0 < ε) fun ε => Metric.closedEBall x ε ∩ s
• uniformity_basis_edist 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [PseudoEMetricSpace α] : (uniformity α).HasBasis (fun ε => 0 < ε) fun ε => {p | edist p.1 p.2 < ε}
• uniformity_basis_edist_le 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [PseudoEMetricSpace α] : (uniformity α).HasBasis (fun ε => 0 < ε) fun ε => {p | edist p.1 p.2 ≤ ε}
• uniformity_basis_edist_inv_nat 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [PseudoEMetricSpace α] : (uniformity α).HasBasis (fun x => True) fun n => {p | edist p.1 p.2 < (↑n)⁻¹}
• uniformity_basis_edist_nnreal_le 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [PseudoEMetricSpace α] : (uniformity α).HasBasis (fun ε => 0 < ε) fun ε => {p | edist p.1 p.2 ≤ ↑ε}
• EMetric.mem_nhdsWithin_iff 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {x : α} {s t : Set α} [PseudoEMetricSpace α] : s ∈ nhdsWithin x t ↔ ∃ ε > 0, Metric.eball x ε ∩ t ⊆ s
• EMetric.nhds_eq 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {x : α} [PseudoEMetricSpace α] : nhds x = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal (Metric.eball x ε)
• uniformity_basis_edist_nnreal 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [PseudoEMetricSpace α] : (uniformity α).HasBasis (fun ε => 0 < ε) fun ε => {p | edist p.1 p.2 < ↑ε}
• EMetric.tendsto_nhds 📋 Mathlib.Topology.EMetricSpace.Defs
  {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] {f : Filter β} {u : β → α} {a : α} : Filter.Tendsto u f (nhds a) ↔ ∀ ε > 0, ∀ᶠ (x : β) in f, edist (u x) a < ε
• EMetric.continuous_iff' 📋 Mathlib.Topology.EMetricSpace.Defs
  {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [TopologicalSpace β] {f : β → α} : Continuous f ↔ ∀ (a : β), ∀ ε > 0, ∀ᶠ (x : β) in nhds a, edist (f x) (f a) < ε
• EMetric.continuousAt_iff' 📋 Mathlib.Topology.EMetricSpace.Defs
  {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [TopologicalSpace β] {f : β → α} {b : β} : ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in nhds b, edist (f x) (f b) < ε
• edist_mem_uniformity 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [PseudoEMetricSpace α] {ε : ENNReal} (ε0 : 0 < ε) : {p | edist p.1 p.2 < ε} ∈ uniformity α
• EMetric.continuousWithinAt_iff' 📋 Mathlib.Topology.EMetricSpace.Defs
  {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [TopologicalSpace β] {f : β → α} {b : β} {s : Set β} : ContinuousWithinAt f s b ↔ ∀ ε > 0, ∀ᶠ (x : β) in nhdsWithin b s, edist (f x) (f b) < ε
• EMetric.mem_closure_iff 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} [PseudoEMetricSpace α] {x : α} {s : Set α} : x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, edist x y < ε
• EMetric.continuousOn_iff' 📋 Mathlib.Topology.EMetricSpace.Defs
  {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [TopologicalSpace β] {f : β → α} {s : Set β} : ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∀ᶠ (x : β) in nhdsWithin b s, edist (f x) (f b) < ε
• mem_uniformity_edist 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [PseudoEMetricSpace α] {s : Set (α × α)} : s ∈ uniformity α ↔ ∃ ε > 0, ∀ {a b : α}, edist a b < ε → (a, b) ∈ s
• uniformity_basis_edist_le' 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [PseudoEMetricSpace α] (ε' : ENNReal) (hε' : 0 < ε') : (uniformity α).HasBasis (fun ε => ε ∈ Set.Ioo 0 ε') fun ε => {p | edist p.1 p.2 ≤ ε}
• uniformity_basis_edist' 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [PseudoEMetricSpace α] (ε' : ENNReal) (hε' : 0 < ε') : (uniformity α).HasBasis (fun ε => ε ∈ Set.Ioo 0 ε') fun ε => {p | edist p.1 p.2 < ε}
• EMetric.tendsto_atTop 📋 Mathlib.Topology.EMetricSpace.Defs
  {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : β → α} {a : α} : Filter.Tendsto u Filter.atTop (nhds a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (u n) a < ε
• Prod.edist_eq 📋 Mathlib.Topology.EMetricSpace.Defs
  {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (x y : α × β) : edist x y = max (edist x.1 y.1) (edist x.2 y.2)
• Metric.closedEBall_prod_same 📋 Mathlib.Topology.EMetricSpace.Defs
  {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (x : α) (y : β) (r : ENNReal) : Metric.closedEBall x r ×ˢ Metric.closedEBall y r = Metric.closedEBall (x, y) r
• Metric.eball_prod_same 📋 Mathlib.Topology.EMetricSpace.Defs
  {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (x : α) (y : β) (r : ENNReal) : Metric.eball x r ×ˢ Metric.eball y r = Metric.eball (x, y) r
• PseudoEMetricSpace.ofEDistOfTopology 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} [TopologicalSpace α] (d : α → α → ENNReal) (h_self : ∀ (x : α), d x x = 0) (h_comm : ∀ (x y : α), d x y = d y x) (h_triangle : ∀ (x y z : α), d x z ≤ d x y + d y z) (h_basis : ∀ (x : α), (nhds x).HasBasis (fun c => 0 < c) fun c => {y | d x y < c}) : PseudoEMetricSpace α
• EMetric.uniformContinuous_iff_le 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} : UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃a b : α⦄, edist a b ≤ δ → edist (f a) (f b) ≤ ε
• uniformity_basis_edist_inv_two_pow 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [PseudoEMetricSpace α] : (uniformity α).HasBasis (fun x => True) fun n => {p | edist p.1 p.2 < 2⁻¹ ^ n}
• uniformity_pseudoedist 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [PseudoEMetricSpace α] : uniformity α = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | edist p.1 p.2 < ε}
• PseudoEMetricSpace.uniformity_edist 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [self : PseudoEMetricSpace α] : uniformity α = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | edist p.1 p.2 < ε}
• EMetric.mk_uniformity_basis_le 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [PseudoEMetricSpace α] {β : Type u_2} {p : β → Prop} {f : β → ENNReal} (hf₀ : ∀ (x : β), p x → 0 < f x) (hf : ∀ (ε : ENNReal), 0 < ε → ∃ x, p x ∧ f x ≤ ε) : (uniformity α).HasBasis p fun x => {p | edist p.1 p.2 ≤ f x}
• EMetric.uniformContinuous_iff 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} : UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε
• EMetric.mk_uniformity_basis 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [PseudoEMetricSpace α] {β : Type u_2} {p : β → Prop} {f : β → ENNReal} (hf₀ : ∀ (x : β), p x → 0 < f x) (hf : ∀ (ε : ENNReal), 0 < ε → ∃ x, p x ∧ f x ≤ ε) : (uniformity α).HasBasis p fun x => {p | edist p.1 p.2 < f x}
• EMetric.continuous_iff 📋 Mathlib.Topology.EMetricSpace.Defs
  {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} : Continuous f ↔ ∀ (b : α), ∀ ε > 0, ∃ δ > 0, ∀ (a : α), edist a b < δ → edist (f a) (f b) < ε
• EMetric.continuousAt_iff 📋 Mathlib.Topology.EMetricSpace.Defs
  {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {a : α} : ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε
• EMetric.tendsto_nhds_nhds 📋 Mathlib.Topology.EMetricSpace.Defs
  {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {a : α} {b : β} : Filter.Tendsto f (nhds a) (nhds b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) b < ε
• EMetric.uniformContinuousOn_iff_le 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {s : Set α} : UniformContinuousOn f s ↔ ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, ∀ b ∈ s, edist a b ≤ δ → edist (f a) (f b) ≤ ε
• EMetric.continuousWithinAt_iff 📋 Mathlib.Topology.EMetricSpace.Defs
  {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {a : α} {s : Set α} : ContinuousWithinAt f s a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → edist (f x) (f a) < ε
• EMetric.uniformContinuousOn_iff 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {s : Set α} : UniformContinuousOn f s ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a : α}, a ∈ s → ∀ {b : α}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
• EMetric.tendsto_nhdsWithin_nhds 📋 Mathlib.Topology.EMetricSpace.Defs
  {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] {s : Set α} [PseudoEMetricSpace β] {f : α → β} {a : α} {b : β} : Filter.Tendsto f (nhdsWithin a s) (nhds b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε
• EMetric.continuousOn_iff 📋 Mathlib.Topology.EMetricSpace.Defs
  {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {s : Set α} : ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, edist a b < δ → edist (f a) (f b) < ε
• EMetric.tendsto_nhdsWithin_nhdsWithin 📋 Mathlib.Topology.EMetricSpace.Defs
  {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] {s : Set α} [PseudoEMetricSpace β] {f : α → β} {t : Set β} {a : α} {b : β} : Filter.Tendsto f (nhdsWithin a s) (nhdsWithin b t) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
• PseudoEMetricSpace.mk 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [toEDist : EDist α] (edist_self : ∀ (x : α), edist x x = 0) (edist_comm : ∀ (x y : α), edist x y = edist y x) (edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z) (toUniformSpace : UniformSpace α) (uniformity_edist : uniformity α = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | edist p.1 p.2 < ε} := by rfl) : PseudoEMetricSpace α
• PseudoMetricSpace.toPseudoEMetricSpace 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : PseudoEMetricSpace α
• PseudoEMetricSpace.toPseudoMetricSpace 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoEMetricSpace α] (h : ∀ (x y : α), edist x y ≠ ⊤) : PseudoMetricSpace α
• PseudoEMetricSpace.toPseudoMetricSpaceOfDist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {X : Type u_3} [e : PseudoEMetricSpace X] (dist : X → X → ℝ) (dist_nonneg : ∀ (x y : X), 0 ≤ dist x y) (h : ∀ (x y : X), edist x y = ENNReal.ofReal (dist x y)) : PseudoMetricSpace X
• instEDistSeparationQuotient 📋 Mathlib.Topology.EMetricSpace.Basic
  {X : Type u_1} [PseudoEMetricSpace X] : EDist (SeparationQuotient X)
• instEMetricSpaceSeparationQuotient 📋 Mathlib.Topology.EMetricSpace.Basic
  {X : Type u_1} [PseudoEMetricSpace X] : EMetricSpace (SeparationQuotient X)
• EMetricSpace.ofT0PseudoEMetricSpace 📋 Mathlib.Topology.EMetricSpace.Basic
  (α : Type u_2) [PseudoEMetricSpace α] [T0Space α] : EMetricSpace α
• EMetric.secondCountable_of_sigmaCompact 📋 Mathlib.Topology.EMetricSpace.Basic
  (γ : Type u) [PseudoEMetricSpace γ] [SigmaCompactSpace γ] : SecondCountableTopology γ
• EMetric.complete_of_cauchySeq_tendsto 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} [PseudoEMetricSpace γ] : (∀ (u : ℕ → γ), CauchySeq u → ∃ a, Filter.Tendsto u Filter.atTop (nhds a)) → CompleteSpace γ
• Inseparable.edist_eq_zero 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} [PseudoEMetricSpace γ] {x y : γ} : Inseparable x y → edist x y = 0
• EMetric.inseparable_iff 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} [PseudoEMetricSpace γ] {x y : γ} : Inseparable x y ↔ edist x y = 0
• EMetric.subset_countable_closure_of_compact 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} [PseudoEMetricSpace γ] {s : Set γ} (hs : IsCompact s) : ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t
• SeparationQuotient.edist_mk 📋 Mathlib.Topology.EMetricSpace.Basic
  {X : Type u_1} [PseudoEMetricSpace X] (x y : X) : edist (SeparationQuotient.mk x) (SeparationQuotient.mk y) = edist x y
• EMetric.tendstoUniformly_iff 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} {β : Type v} [PseudoEMetricSpace γ] {ι : Type u_2} {F : ι → β → γ} {f : β → γ} {p : Filter ι} : TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), edist (f x) (F n x) < ε
• EMetric.secondCountable_of_almost_dense_set 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} [PseudoEMetricSpace γ] (hs : ∀ ε > 0, ∃ t, t.Countable ∧ ⋃ x ∈ t, Metric.closedEBall x ε = Set.univ) : SecondCountableTopology γ
• EMetric.cauchySeq_iff' 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} {β : Type v} [PseudoEMetricSpace γ] [Nonempty β] [SemilatticeSup β] {u : β → γ} : CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (u n) (u N) < ε
• EMetric.cauchySeq_iff_NNReal 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} {β : Type v} [PseudoEMetricSpace γ] [Nonempty β] [SemilatticeSup β] {u : β → γ} : CauchySeq u ↔ ∀ (ε : NNReal), 0 < ε → ∃ N, ∀ (n : β), N ≤ n → edist (u n) (u N) < ↑ε
• EMetric.totallyBounded_iff 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} [PseudoEMetricSpace γ] {s : Set γ} : TotallyBounded s ↔ ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, Metric.eball y ε
• EMetric.tendstoUniformlyOn_iff 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} {β : Type v} [PseudoEMetricSpace γ] {ι : Type u_2} {F : ι → β → γ} {f : β → γ} {p : Filter ι} {s : Set β} : TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε
• EMetric.complete_of_convergent_controlled_sequences 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} [PseudoEMetricSpace γ] (B : ℕ → ENNReal) (hB : ∀ (n : ℕ), 0 < B n) (H : ∀ (u : ℕ → γ), (∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (u n) (u m) < B N) → ∃ x, Filter.Tendsto u Filter.atTop (nhds x)) : CompleteSpace γ
• EMetric.totallyBounded_iff' 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} [PseudoEMetricSpace γ] {s : Set γ} : TotallyBounded s ↔ ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, Metric.eball y ε
• EMetric.cauchySeq_iff 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} {β : Type v} [PseudoEMetricSpace γ] [Nonempty β] [SemilatticeSup β] {u : β → γ} : CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (u m) (u n) < ε
• EMetric.cauchy_iff 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} [PseudoEMetricSpace γ] {f : Filter γ} : Cauchy f ↔ f ≠ ⊥ ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε
• EMetric.tendstoLocallyUniformly_iff 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} {β : Type v} [PseudoEMetricSpace γ] {ι : Type u_2} [TopologicalSpace β] {F : ι → β → γ} {f : β → γ} {p : Filter ι} : TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ (x : β), ∃ t ∈ nhds x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
• EMetric.tendstoLocallyUniformlyOn_iff 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} {β : Type v} [PseudoEMetricSpace γ] {ι : Type u_2} [TopologicalSpace β] {F : ι → β → γ} {f : β → γ} {p : Filter ι} {s : Set β} : TendstoLocallyUniformlyOn F f p s ↔ ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
• EMetric.isUniformInducing_iff 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} {β : Type v} [PseudoEMetricSpace γ] [PseudoEMetricSpace β] {f : γ → β} : IsUniformInducing f ↔ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ
• EMetric.isUniformEmbedding_iff 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} {β : Type v} [PseudoEMetricSpace γ] [PseudoEMetricSpace β] {f : γ → β} : IsUniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ
• EMetric.controlled_of_isUniformEmbedding 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} {β : Type v} [PseudoEMetricSpace γ] [PseudoEMetricSpace β] {f : γ → β} (h : IsUniformEmbedding f) : (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ
• EMetric.controlled_of_isUniformInducing 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} {β : Type v} [PseudoEMetricSpace γ] [PseudoEMetricSpace β] {f : γ → β} (h : IsUniformInducing f) : (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ
• EMetric.isUniformEmbedding_iff' 📋 Mathlib.Topology.EMetricSpace.Basic
  {β : Type v} {γ : Type w} [EMetricSpace γ] [PseudoEMetricSpace β] {f : γ → β} : IsUniformEmbedding f ↔ (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ
• pseudoEMetricSpacePi 📋 Mathlib.Topology.EMetricSpace.Pi
  {β : Type v} {X : β → Type u_2} [Fintype β] [(b : β) → PseudoEMetricSpace (X b)] : PseudoEMetricSpace ((b : β) → X b)
• PseudoEMetricSpace.replaceEDist 📋 Mathlib.Topology.MetricSpace.Basic
  {X : Type u_2} (m : PseudoEMetricSpace X) (d : X → X → ENNReal) (hd : d = edist) : PseudoEMetricSpace X
• PseudoEMetricSpace.replaceEDist_eq 📋 Mathlib.Topology.MetricSpace.Basic
  {X : Type u_2} (m : PseudoEMetricSpace X) (d : X → X → ENNReal) (hd : d = edist) : m.replaceEDist d hd = m
• Metric.ediam_pi_le_of_le 📋 Mathlib.Topology.EMetricSpace.Diam
  {ι : Type u_3} {X : ι → Type u_4} [Fintype ι] [(i : ι) → PseudoEMetricSpace (X i)] {s : (i : ι) → Set (X i)} {c : ENNReal} (h : ∀ (b : ι), Metric.ediam (s b) ≤ c) : Metric.ediam (Set.univ.pi s) ≤ c
• LocallyLipschitz 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α → β) : Prop
• LipschitzWith 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : NNReal) (f : α → β) : Prop
• LocallyLipschitz.id 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} [PseudoEMetricSpace α] : LocallyLipschitz id
• LocallyLipschitzOn 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (s : Set α) (f : α → β) : Prop
• LipschitzOnWith 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : NNReal) (f : α → β) (s : Set α) : Prop
• LocallyLipschitz.const 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (b : β) : LocallyLipschitz fun x => b
• LipschitzWith.const' 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (b : β) {K : NNReal} : LipschitzWith K fun x => b
• LipschitzWith.id 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} [PseudoEMetricSpace α] : LipschitzWith 1 id
• locallyLipschitzOn_empty 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α → β) : LocallyLipschitzOn ∅ f
• LipschitzWith.const 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (b : β) : LipschitzWith 0 fun x => b
• lipschitzOnWith_empty 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : NNReal) (f : α → β) : LipschitzOnWith K f ∅
• LocallyLipschitz.iterate 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} [PseudoEMetricSpace α] {f : α → α} (hf : LocallyLipschitz f) (n : ℕ) : LocallyLipschitz f^[n]
• LipschitzWith.locallyLipschitz 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {K : NNReal} (hf : LipschitzWith K f) : LocallyLipschitz f
• LocallyLipschitz.prodMk_left 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (a : α) : LocallyLipschitz (Prod.mk a)
• locallyLipschitzOn_univ 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} : LocallyLipschitzOn Set.univ f ↔ LocallyLipschitz f
• LocallyLipschitz.locallyLipschitzOn 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {s : Set α} {f : α → β} (h : LocallyLipschitz f) : LocallyLipschitzOn s f
• LocallyLipschitz.prodMk_right 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (b : β) : LocallyLipschitz fun a => (a, b)
• lipschitzOnWith_univ 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} : LipschitzOnWith K f Set.univ ↔ LipschitzWith K f
• LipschitzWith.lipschitzOnWith 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} {s : Set α} (h : LipschitzWith K f) : LipschitzOnWith K f s
• LipschitzWith.prod_fst 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] : LipschitzWith 1 Prod.fst
• LipschitzWith.prod_snd 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] : LipschitzWith 1 Prod.snd
• LipschitzWith.uniformContinuous 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) : UniformContinuous f
• LipschitzWith.prodMk_left 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (a : α) : LipschitzWith 1 (Prod.mk a)
• LocallyLipschitz.continuous 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (hf : LocallyLipschitz f) : Continuous f
• LipschitzOnWith.uniformContinuousOn 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} (hf : LipschitzOnWith K f s) : UniformContinuousOn f s
• LipschitzWith.continuous 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) : Continuous f
• LipschitzWith.prodMk_right 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (b : β) : LipschitzWith 1 fun a => (a, b)
• LipschitzWith.zero_iff 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} [PseudoEMetricSpace α] {β : Type u_1} [EMetricSpace β] (f : α → β) : LipschitzWith 0 f ↔ ∀ (x y : α), f x = f y
• LocallyLipschitzOn.continuousOn 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {s : Set α} (hf : LocallyLipschitzOn s f) : ContinuousOn f s
• LipschitzWith.eval 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {ι : Type x} {α : ι → Type u} [(i : ι) → PseudoEMetricSpace (α i)] [Fintype ι] (i : ι) : LipschitzWith 1 (Function.eval i)
• LipschitzWith.weaken 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) {K' : NNReal} (h : K ≤ K') : LipschitzWith K' f
• LocallyLipschitzOn.mono 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {s t : Set α} {f : α → β} (hf : LocallyLipschitzOn t f) (h : s ⊆ t) : LocallyLipschitzOn s f
• LipschitzOnWith.continuousOn 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} (hf : LipschitzOnWith K f s) : ContinuousOn f s
• LipschitzOnWith.mono 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s t : Set α} {f : α → β} (hf : LipschitzOnWith K f t) (h : s ⊆ t) : LipschitzOnWith K f s
• LocallyLipschitz.comp 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {f : β → γ} {g : α → β} (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) : LocallyLipschitz (f ∘ g)
• LipschitzOnWith.weaken 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} (hf : LipschitzOnWith K f s) {K' : NNReal} (h : K ≤ K') : LipschitzOnWith K' f s
• LocallyLipschitz.pow_end 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} [PseudoEMetricSpace α] {f : Function.End α} (h : LocallyLipschitz f) (n : ℕ) : LocallyLipschitz (f ^ n)
• LipschitzWith.iterate 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} [PseudoEMetricSpace α] {K : NNReal} {f : α → α} (hf : LipschitzWith K f) (n : ℕ) : LipschitzWith (K ^ n) f^[n]
• LocallyLipschitzOn.restrict 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {s : Set α} {f : α → β} : LocallyLipschitzOn s f → LocallyLipschitz (s.domRestrict f)
• locallyLipschitzOn_iff_restrict 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {s : Set α} {f : α → β} : LocallyLipschitzOn s f ↔ LocallyLipschitz (s.domRestrict f)
• LipschitzWith.restrict 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) (s : Set α) : LipschitzWith K (s.domRestrict f)
• LipschitzOnWith.to_restrict 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} : LipschitzOnWith K f s → LipschitzWith K (s.domRestrict f)
• LocallyLipschitz.prodMk 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {f : α → β} (hf : LocallyLipschitz f) {g : α → γ} (hg : LocallyLipschitz g) : LocallyLipschitz fun x => (f x, g x)
• lipschitzOnWith_iff_restrict 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} : LipschitzOnWith K f s ↔ LipschitzWith K (s.domRestrict f)
• LipschitzWith.subtype_mk 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) {p : β → Prop} (hp : ∀ (x : α), p (f x)) : LipschitzWith K fun x => ⟨f x, ⋯⟩
• LocallyLipschitz.mul_end 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} [PseudoEMetricSpace α] {f g : Function.End α} (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) : LocallyLipschitz (f * g)
• LipschitzWith.subtype_val 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} [PseudoEMetricSpace α] (s : Set α) : LipschitzWith 1 Subtype.val
• LipschitzOnWith.zero_iff 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} [PseudoEMetricSpace α] {s : Set α} {β : Type u_1} [EMetricSpace β] (f : α → β) : LipschitzOnWith 0 f s ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y
• LipschitzWith.comp 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {Kf Kg : NNReal} {f : β → γ} {g : α → β} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (Kf * Kg) (f ∘ g)
• LipschitzWith.of_edist_le 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (h : ∀ (x y : α), edist (f x) (f y) ≤ edist x y) : LipschitzWith 1 f
• LipschitzWith.pow_end 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} [PseudoEMetricSpace α] {f : Function.End α} {K : NNReal} (h : LipschitzWith K f) (n : ℕ) : LipschitzWith (K ^ n) (f ^ n)
• LipschitzWith.prodMk 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {f : α → β} {Kf : NNReal} (hf : LipschitzWith Kf f) {g : α → γ} {Kg : NNReal} (hg : LipschitzWith Kg g) : LipschitzWith (max Kf Kg) fun x => (f x, g x)
• LipschitzWith.comp_lipschitzOnWith 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {Kf Kg : NNReal} {f : β → γ} {g : α → β} {s : Set α} (hf : LipschitzWith Kf f) (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (Kf * Kg) (f ∘ g) s
• LipschitzOnWith.prodMk 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {s : Set α} {f : α → β} {g : α → γ} {Kf Kg : NNReal} (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (max Kf Kg) (fun x => (f x, g x)) s
• LipschitzWith.edist_lt_top 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) {x y : α} (h : edist x y ≠ ⊤) : edist (f x) (f y) < ⊤
• LipschitzWith.uncurry 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {f : α → β → γ} {Kα Kβ : NNReal} (hα : ∀ (b : β), LipschitzWith Kα fun a => f a b) (hβ : ∀ (a : α), LipschitzWith Kβ (f a)) : LipschitzWith (Kα + Kβ) (Function.uncurry f)
• LipschitzWith.mul_end 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} [PseudoEMetricSpace α] {f g : Function.End α} {Kf Kg : NNReal} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (Kf * Kg) (f * g)
• continuous_prod_of_continuous_lipschitzWith 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) (K : NNReal) (ha : ∀ (a : α), Continuous fun y => f (a, y)) (hb : ∀ (b : β), LipschitzWith K fun x => f (x, b)) : Continuous f
• continuous_prod_of_continuous_lipschitzWith' 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) (K : NNReal) (ha : ∀ (a : α), LipschitzWith K fun y => f (a, y)) (hb : ∀ (b : β), Continuous fun x => f (x, b)) : Continuous f
• LipschitzOnWith.comp 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {K : NNReal} {s : Set α} {f : α → β} {g : β → γ} {t : Set β} {Kg : NNReal} (hg : LipschitzOnWith Kg g t) (hf : LipschitzOnWith K f s) (hmaps : Set.MapsTo f s t) : LipschitzOnWith (Kg * K) (g ∘ f) s
• LipschitzOnWith.mapsToRestrict 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} {t : Set β} (h : Set.MapsTo f s t) : LipschitzOnWith K f s → LipschitzWith K (Set.MapsTo.restrict f s t h)
• LipschitzWith.ediam_image_le 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) (s : Set α) : Metric.ediam (f '' s) ≤ ↑K * Metric.ediam s
• LipschitzWith.edist_le_mul 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (h : LipschitzWith K f) (x y : α) : edist (f x) (f y) ≤ ↑K * edist x y
• LipschitzWith.mapsTo_closedEBall 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (h : LipschitzWith K f) (x : α) (r : ENNReal) : Set.MapsTo f (Metric.closedEBall x r) (Metric.closedEBall (f x) (↑K * r))
• Set.MapsTo.lipschitzOnWith_iff_restrict 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} {t : Set β} (h : Set.MapsTo f s t) : LipschitzOnWith K f s ↔ LipschitzWith K (Set.MapsTo.restrict f s t h)
• LipschitzWith.mul_edist_le 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (h : LipschitzWith K f) (x y : α) : (↑K)⁻¹ * edist (f x) (f y) ≤ edist x y
• LipschitzWith.list_prod 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {ι : Type x} [PseudoEMetricSpace α] (f : ι → Function.End α) (K : ι → NNReal) (h : ∀ (i : ι), LipschitzWith (K i) (f i)) (l : List ι) : LipschitzWith (List.map K l).prod (List.map f l).prod
• LipschitzWith.edist_le_mul_of_le 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} {x y : α} {r : ENNReal} (h : LipschitzWith K f) (hr : edist x y ≤ r) : edist (f x) (f y) ≤ ↑K * r
• LipschitzWith.mapsTo_eball 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (h : LipschitzWith K f) (hK : K ≠ 0) (x : α) (r : ENNReal) : Set.MapsTo f (Metric.eball x r) (Metric.eball (f x) (↑K * r))
• LipschitzWith.edist_lt_of_edist_lt_div 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) {x y : α} {d : ENNReal} (h : edist x y < d / ↑K) : edist (f x) (f y) < d
• lipschitzOnWith_restrict 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} {t : Set ↑s} : LipschitzOnWith K (s.domRestrict f) t ↔ LipschitzOnWith K f (s ∩ Subtype.val '' t)
• continuous_prod_of_dense_continuous_lipschitzWith 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) (K : NNReal) {s : Set α} (hs : Dense s) (ha : ∀ a ∈ s, Continuous fun y => f (a, y)) (hb : ∀ (b : β), LipschitzWith K fun x => f (x, b)) : Continuous f
• continuous_prod_of_dense_continuous_lipschitzWith' 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) (K : NNReal) {t : Set β} (ht : Dense t) (ha : ∀ (a : α), LipschitzWith K fun y => f (a, y)) (hb : ∀ b ∈ t, Continuous fun x => f (x, b)) : Continuous f
• LipschitzWith.edist_lt_mul_of_lt 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} {x y : α} {r : ENNReal} (h : LipschitzWith K f) (hK : K ≠ 0) (hr : edist x y < r) : edist (f x) (f y) < ↑K * r
• LipschitzOnWith.edist_le_mul_of_le 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} (h : LipschitzOnWith K f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) {r : ENNReal} (hr : edist x y ≤ r) : edist (f x) (f y) ≤ ↑K * r
• LipschitzOnWith.edist_lt_of_edist_lt_div 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} (hf : LipschitzOnWith K f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) {d : ENNReal} (hd : edist x y < d / ↑K) : edist (f x) (f y) < d
• LipschitzWith.edist_iterate_succ_le_geometric 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} [PseudoEMetricSpace α] {K : NNReal} {f : α → α} (hf : LipschitzWith K f) (x : α) (n : ℕ) : edist (f^[n] x) (f^[n + 1] x) ≤ edist x (f x) * ↑K ^ n
• continuousOn_prod_of_continuousOn_lipschitzOnWith 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t : Set β} (K : NNReal) (ha : ∀ a ∈ s, ContinuousOn (fun y => f (a, y)) t) (hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s) : ContinuousOn f (s ×ˢ t)
• continuousOn_prod_of_continuousOn_lipschitzOnWith' 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t : Set β} (K : NNReal) (ha : ∀ a ∈ s, LipschitzOnWith K (fun y => f (a, y)) t) (hb : ∀ b ∈ t, ContinuousOn (fun x => f (x, b)) s) : ContinuousOn f (s ×ˢ t)
• continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s s' : Set α} {t : Set β} (hs' : s' ⊆ s) (hss' : s ⊆ closure s') (K : NNReal) (ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t) (hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s) : ContinuousOn f (s ×ˢ t)
• continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith' 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t t' : Set β} (ht' : t' ⊆ t) (htt' : t ⊆ closure t') (K : NNReal) (ha : ∀ a ∈ s, LipschitzOnWith K (fun y => f (a, y)) t) (hb : ∀ b ∈ t', ContinuousOn (fun x => f (x, b)) s) : ContinuousOn f (s ×ˢ t)
• LipschitzOnWith.ediam_image2_le 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : α → β → γ) {K₁ K₂ : NNReal} (s : Set α) (t : Set β) (hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x => f x b) s) (hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t) : Metric.ediam (Set.image2 f s t) ≤ ↑K₁ * Metric.ediam s + ↑K₂ * Metric.ediam t
• AntilipschitzWith 📋 Mathlib.Topology.MetricSpace.Antilipschitz
  {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : NNReal) (f : α → β) : Prop
• AntilipschitzWith.id 📋 Mathlib.Topology.MetricSpace.Antilipschitz
  {α : Type u_1} [PseudoEMetricSpace α] : AntilipschitzWith 1 id
• AntilipschitzWith.k 📋 Mathlib.Topology.MetricSpace.Antilipschitz
  {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (_hf : AntilipschitzWith K f) : NNReal
• AntilipschitzWith.of_subsingleton 📋 Mathlib.Topology.MetricSpace.Antilipschitz
  {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} [Subsingleton α] {K : NNReal} : AntilipschitzWith K f
• AntilipschitzWith.injective 📋 Mathlib.Topology.MetricSpace.Antilipschitz
  {α : Type u_4} {β : Type u_5} [EMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : AntilipschitzWith K f) : Function.Injective f
• AntilipschitzWith.subsingleton 📋 Mathlib.Topology.MetricSpace.Antilipschitz
  {α : Type u_4} {β : Type u_5} [EMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (h : AntilipschitzWith 0 f) : Subsingleton α
• AntilipschitzWith.to_rightInverse 📋 Mathlib.Topology.MetricSpace.Antilipschitz
  {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : AntilipschitzWith K f) {g : β → α} (hg : Function.RightInverse g f) : LipschitzWith K g
• LipschitzWith.to_rightInverse 📋 Mathlib.Topology.MetricSpace.Antilipschitz
  {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) {g : β → α} (hg : Function.RightInverse g f) : AntilipschitzWith K g
• AntilipschitzWith.pos 📋 Mathlib.Topology.MetricSpace.Antilipschitz
  {β : Type u_2} [PseudoEMetricSpace β] {K : NNReal} {α : Type u_4} [EMetricSpace α] [Nontrivial α] {f : α → β} (hf : AntilipschitzWith K f) : 0 < K
• AntilipschitzWith.isUniformInducing 📋 Mathlib.Topology.MetricSpace.Antilipschitz
  {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : AntilipschitzWith K f) (hfc : UniformContinuous f) : IsUniformInducing f
• AntilipschitzWith.edist_ne_top 📋 Mathlib.Topology.MetricSpace.Antilipschitz
  {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : α → β} (h : AntilipschitzWith K f) (x y : α) : edist x y ≠ ⊤

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 ce5dd8c