MapClusterPt and EventuallyEq

Stream: Is there code for X?

[Thomas Browning]

Does a result like this exist in Mathlib, or is there a more idiomatic proof?

import Mathlib.MeasureTheory.Measure.Regular

lemma MapClusterPt.eq_of_eventually
    {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X]
    {f g : Y → X} {y : Y}
    {ι : Type*} {F : Filter ι} {z : ι → Y}
    (h : MapClusterPt y F z) (ha : ContinuousAt f y) (hb : ContinuousAt g y)
    (hfg : f ∘ z =ᶠ[F] g ∘ z) : f y = g y := by
  refine tendsto_nhds_unique_of_frequently_eq ha hb ?_
  rw [Filter.eventuallyEq_iff_exists_mem] at hfg
  obtain ⟨s, hs1, hs2⟩ := hfg
  rw [mapClusterPt_def] at h
  have key : z '' s ∈ F.map z := Filter.image_mem_map hs1
  rw [clusterPt_iff_frequently] at h
  rw [frequently_nhds_iff]
  intro U hy hU
  specialize h U (hU.mem_nhds hy)
  rw [Filter.frequently_iff] at h
  specialize h key
  obtain ⟨T, hT1, hT2⟩ := h
  use T
  use hT2
  obtain ⟨i, hi, rfl⟩ := hT1
  apply hs2
  exact hi

[Aaron Liu]

import Mathlib.Topology.Separation.Hausdorff

open Filter

lemma MapClusterPt.eq_of_eventually
    {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X]
    {f g : Y → X} {y : Y}
    {ι : Type*} {F : Filter ι} {z : ι → Y}
    (h : MapClusterPt y F z) (ha : ContinuousAt f y) (hb : ContinuousAt g y)
    (hfg : f ∘ z =ᶠ[F] g ∘ z) : f y = g y := by
  replace h := h.neBot.map f
  apply eq_of_nhds_neBot
  replace hfg : map f (nhds y ⊓ map z F) = map g (nhds y ⊓ map z F) :=
    Filter.map_congr ((eventuallyEq_map.mpr hfg).filter_mono inf_le_right)
  rw [← inf_of_le_left hfg.le] at h
  apply h.mono
  apply inf_le_inf
  · apply map_inf_le.trans
    apply inf_le_of_left_le
    exact ha.tendsto
  · apply map_inf_le.trans
    apply inf_le_of_left_le
    exact hb.tendsto

[Aaron Liu]

I think in filters

[Thomas Browning]

Thanks! Working off of this, I think I've found something more-or-less idomatic. I'm just surprised the first lemma isn't in mathlib yet

import Mathlib.Topology.Separation.Hausdorff

open Filter

variable {X Y ι : Type*} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] {y : Y}

lemma ClusterPt.frequently' {F : Filter Y} (h : ClusterPt y F)
    {p : Y → Prop} (hp : ∀ᶠ x in F, p x) :
    ∃ᶠ x in nhds y, p x := by
  rw [eventually_iff, ← le_principal_iff] at hp
  exact clusterPt_principal_iff_frequently.mp (h.mono hp)

lemma ClusterPt.apply_eq_of_eventually {F : Filter Y} (h : ClusterPt y F)
    {f g : Y → X} (ha : ContinuousAt f y) (hb : ContinuousAt g y) (hfg : f =ᶠ[F] g) :
    f y = g y :=
  tendsto_nhds_unique_of_frequently_eq ha hb (h.frequently' hfg)

lemma MapClusterPt.apply_eq_of_eventually {F : Filter ι} {z : ι → Y} (h : MapClusterPt y F z)
    {f g : Y → X} (ha : ContinuousAt f y) (hb : ContinuousAt g y) (hfg : f ∘ z =ᶠ[F] g ∘ z) :
    f y = g y :=
  ClusterPt.apply_eq_of_eventually h ha hb hfg