continuous_iff_continuous_edist

Stream: Is there code for X?

[Yaël Dillies]

Is the edist version of docs#continuous_iff_continuous_dist true? Do we have it somewhere?

[Aaron Liu]

It is true at least:

import Mathlib

open Filter Topology Uniformity Set
variable {α β : Type*} [PseudoEMetricSpace α]

theorem EMetric.uniformity_eq_comap_nhds_zero :
    𝓤 α = comap (fun p : α × α => edist p.1 p.2) (𝓝 (0 : ENNReal)) := by
  ext s
  simp only [mem_uniformity_edist, (nhds_basis_eball.comap _).mem_iff]
  simp [subset_def, Real.dist_0_eq_abs]

theorem nhds_comap_edist (a : α) : ((𝓝 (0 : ENNReal)).comap (edist · a)) = 𝓝 a := by
  simp only [@nhds_eq_comap_uniformity α, Metric.uniformity_eq_comap_nhds_zero, comap_comap,
    Function.comp_def, dist_comm]

theorem tendsto_iff_edist_tendsto_zero {f : β → α} {x : Filter β} {a : α} :
    Tendsto f x (𝓝 a) ↔ Tendsto (fun b => edist (f b) a) x (𝓝 0) := by
  rw [← nhds_comap_edist a, tendsto_comap_iff, Function.comp_def]

lemma continuous_iff_continuous_edist [TopologicalSpace β] {f : β → α} :
    Continuous f ↔ Continuous fun x : β × β => edist (f x.1) (f x.2) :=
  ⟨fun h => h.fst'.edist h.snd', fun h =>
    continuous_iff_continuousAt.2 fun _ => tendsto_iff_edist_tendsto_zero.2 <|
      (h.comp (.prodMk_left _)).tendsto' _ _ <| edist_self _⟩

[Yaël Dillies]

Thanks! But your proofs don't compile on latest mathlib

[Yaël Dillies]

Here are the fixed proofs:

import Mathlib.Topology.Instances.ENNReal.Lemmas

open Filter Topology Uniformity Set
open scoped ENNReal

variable {α β : Type*} [PseudoEMetricSpace α]

lemma EMetric.uniformity_eq_comap_nhds_zero :
    𝓤 α = comap (fun p : α × α => edist p.1 p.2) (𝓝 (0 : ENNReal)) := by
  ext s
  simp_rw [mem_uniformity_edist, (ENNReal.nhds_zero_basis.comap _).mem_iff]
  simp [subset_def, Real.dist_0_eq_abs]

lemma nhds_comap_edist (a : α) : ((𝓝 (0 : ENNReal)).comap (edist · a)) = 𝓝 a := by
  simp only [@nhds_eq_comap_uniformity α, EMetric.uniformity_eq_comap_nhds_zero, comap_comap,
    Function.comp_def, edist_comm]

lemma tendsto_iff_edist_tendsto_zero {f : β → α} {x : Filter β} {a : α} :
    Tendsto f x (𝓝 a) ↔ Tendsto (fun b => edist (f b) a) x (𝓝 0) := by
  rw [← nhds_comap_edist a, tendsto_comap_iff, Function.comp_def]

lemma continuous_iff_continuous_edist [TopologicalSpace β] {f : β → α} :
    Continuous f ↔ Continuous fun x : β × β => edist (f x.1) (f x.2) where
  mp h := h.fst'.edist h.snd'
  mpr h := continuous_iff_continuousAt.2 fun _ ↦ tendsto_iff_edist_tendsto_zero.2 <|
    (h.comp (.prodMk_left _)).tendsto' _ _ <| edist_self _