Characterization of `ClusterPt` by closure

Stream: Is there code for X?

[Anatole Dedecker]

Do we have the following?

import Mathlib.Topology.Basic

open Filter Topology Function Prod Set

theorem clusterPt_iff_forall_mem_closure [TopologicalSpace X] {F : Filter X} {x : X} :
    ClusterPt x F ↔ ∀ s ∈ F, x ∈ closure s := by
  simp only [ClusterPt, inf_comm, inf_neBot_iff, inter_comm, mem_closure_iff_nhds]

Bonus points for the equivalent:

theorem clusterPt_iff_lift'_closure [TopologicalSpace X] {F : Filter X} {x : X} :
    ClusterPt x F ↔ ((F.lift' closure) ⊓ pure x).NeBot := by
  simp_rw [clusterPt_iff_forall_mem_closure, ← principal_singleton,
    F.basis_sets.lift'_closure.inf_principal_neBot_iff, inter_singleton_nonempty,
    mem_closure_iff_nhds, id]

[Anatole Dedecker]

Context: I got nerdsniped by discussions on #5969 and decided it's about time that we develop the basic theory of proper maps, but the proofs in Bourbaki are just not filter-y enough.

[Oliver Nash]

Looking now, I don't see these results.

[Oliver Nash]

I presume you've seen that we have a the type of bundled maps docs#CocompactMap though we know almost nothing about it.

[Anatole Dedecker]

Yes but these are only true proper maps for locally compact spaces, I will try to make a usable bridge between the two APIs (although for now I'm going for unbundled proper maps whereas docs#CocompactMap only has a bundled version iirc)

[Patrick Massot]

It's not there. I'm sad to see inf_comm, inf_neBot_iff, inter_comm in your proof. I thought our convention to order stuff was sufficiently consistent to avoid that. Maybe we need a inf_neBot_iff' to avoid that.

[Anatole Dedecker]

Well in some sense the fact that I need to revert by using inter_comm after inf_comm means that the convention is almost perfect! But indeed adding inf_neBot_iff' seems like the cleanest thing to do.