Accumulation point

Stream: Is there code for X?

[Bhavik Mehta]

Since we now have a version of the identity theorem in mathlib, I'm trying to write a version which matches wikipedia's statement more closely - in particular using accumulation points. My understanding was that docs#cluster_pt is how mathlib talks about accumulation points, but stating the theorem like this

lemma identity_theorem {f : ℂ → ℂ} {D S : set ℂ}
  (hfD : analytic_on ℂ f D) (hD : is_open D)
  (hD' : is_connected D) -- probably preconnected is enough
  (hSD : S ⊆ D) (hfS : S.eq_on f 0) {z : ℂ}
  (hz : cluster_pt z (𝓟 S)) : -- z is an accumulation point of S
  D.eq_on f 0 :=

can't work (it's not hard to show this is false). So what am I misunderstanding here? Presumably it's about accumulation points vs cluster_pt, but I can't quite figure it out

[Junyan Xu]

I commeted about this here: https://github.com/leanprover-community/mathlib/pull/16489#discussion_r971039654

[Bhavik Mehta]

Ah I see, so docs#cluster_pt on principal filters doesn't correspond to accumulation points of sets, thanks!

[Patrick Massot]

Don't you simply want the analogue of cluster_pt but with punctured neighborhoods?

[Patrick Massot]

I mean 𝓝[≠] x instead of 𝓝 x

[Bhavik Mehta]

Ah, so hz should instead be (hz : (𝓝[≠] z ⊓ 𝓟 S).ne_bot)? That seems reasonable to me

[Patrick Massot]

Indeed it is suspicious that cluster_pt doesn't give back the right notion for set. Maybe mathlib's definition is not the right one. We should check that.

[Patrick Massot]

I checked the definition of cluster point of a filter is the same in Bourbaki and in mathlib.

[Bhavik Mehta]

Patrick Massot said:

I checked the definition of cluster point of a filter is the same in Bourbaki and in mathlib.

Hmm, does this then mean that cluster points of filters don't align as closely as I guessed to cluster points of sets?

[Jireh Loreaux]

No, it's just that cluster points and accumulation points are in general different concepts.

[Jireh Loreaux]

(At least, with the terminology I am used to)

[Bhavik Mehta]

Jireh Loreaux said:

No, it's just that cluster points and accumulation points are in general different concepts.

In this case I'm confused at the docstring for cluster_pt, which says that these are also called accumulation points

[Jireh Loreaux]

aha, well, Wikipedia says my version of the terminology is nonstandard. It says that cluster point, accumulation point and limit point are all synonymous (with punctured nhds definition), and that adherent point is what mathlib currently calls cluster point. (I've never heard anyone use the term "adherent point" before though.)

[Jireh Loreaux]

Personally, I've frequently heard "cluster point" or "limit point" for the nhds version, and "accumulation point" for the punctured nhds version, but maybe I have just been exposed to weird sources.

[Patrick Massot]

It's pretty clear there are different notions and people disagree on terminology. It simply means we need to write really clear docstrings.

[Patrick Massot]

Jireh Loreaux said:

(I've never heard anyone use the term "adherent point" before though.)

This may come from French. In French the closure of a set is called the "adhérence" of the set.

[Bhavik Mehta]

So now that I understand cluster_pt, my new goal is

example {S : set ℂ} (hS : is_compact S) (hS' : S.infinite) :
  ∃ z ∈ S, (𝓝[≠] z ⊓ 𝓟 S).ne_bot :=
begin

end

Any hints?

[Vincent Beffara]

It would certainly be useful to have some API around accumulation points and variants of that. I chose to spell it as ∃ᶠ z in 𝓝[≠] w, p z because that felt natural at the time, but it probably isn't optimal.

[Patrick Massot]

Bahvik, are you asking for a Lean proof or a paper proof?

[Bhavik Mehta]

Patrick Massot said:

Bahvik, are you asking for a Lean proof or a paper proof?

I understand the proof on paper - but I suspected there'd be a cleaner filter proof that I wouldn't be able to come up with on paper

[Damiano Testa]

Bhavik Mehta said:

So now that I understand cluster_pt, my new goal is

example {S : set ℂ} (hS : is_compact S) (hS' : S.infinite) :
  ∃ z ∈ S, (𝓝[≠] z ⊓ 𝓟 S).ne_bot :=
begin

end

Any hints?

The same statement is true with bounded, instead of compact, right? It might be easier to prove with bounded, since any subset of a bounded set is again bounded.

[Bhavik Mehta]

(In particular, on paper I'd pick a point from S, construct a sequence in S which is never equal to that point, then find a convergent subsequence, and its limit would be my choice of z. But my hope was that a cleverer filters proof could avoid going to sequences at all?)

[Damiano Testa]

Ah, sorry, I missed z is in S, not in the closure!

[Patrick Massot]

There is no need to use sequences

[Bhavik Mehta]

Patrick Massot said:

There is no need to use sequences

In that case I don't see how to proceed, other than using sequences... I can't seem to find much linking infinite sets and topology in mathlib

[Vincent Beffara]

Something to do with docs#is_seq_compact.subseq_of_frequently_in, docs#is_compact.is_seq_compact and (∃ᶠ x in 𝓝[≠] z, x ∈ s) ↔ (𝓝[≠] z ⊓ 𝓟 s).ne_bot (which I'm not sure is true)?

[Bhavik Mehta]

Vincent Beffara said:

Something to do with docs#is_seq_compact.subseq_of_frequently_in, docs#is_compact.is_seq_compact and (∃ᶠ x in 𝓝[≠] z, x ∈ s) ↔ (𝓝[≠] z ⊓ 𝓟 s).ne_bot (which I'm not sure is true)?

Yeah this is what I guessed too - but this uses sequences!

[Patrick Massot]

Ok, I'll have a look.

[Bhavik Mehta]

Thanks!

[Adam Topaz]

you can always choose a nonprincipal ultrafilter on S, push it forward to C, and take its limit as your z.

[Adam Topaz]

I'm sure Patrick has a more elegant argument in mind ;)

[Patrick Massot]

It's getting late here so I wrote a blunt proof.

import topology.subset_properties

open_locale filter topological_space

open filter set

example {α : Type*} [topological_space α] {S : set α} (hS : is_compact S) (hS' : S.infinite) :
  ∃ z ∈ S, (𝓝[≠] z ⊓ 𝓟 S).ne_bot :=
begin
  simp_rw inf_principal_ne_bot_iff,
  by_contra' H,
  apply hS',
  simp_rw [← ne_empty_iff_nonempty, not_ne_iff] at H,
  choose! U hU hU' using H,
  have : ∀ x ∈ S, insert x (U x) ∈ 𝓝 x,
  { intros z hz,
    exact insert_mem_nhds_iff.mpr (hU z hz) },
  rcases hS.elim_nhds_subcover (λ a, insert a (U a)) this with ⟨T, hT, hT' : S ⊆ ⋃ x ∈ T, insert x (U x)⟩,
  have : S = T,
  { apply subset.antisymm _ hT,
    intros z hz,
    specialize hT' hz,
    simp only [mem_Union, mem_insert_iff, exists_prop] at hT',
    rcases hT' with ⟨y, H, rfl | hzy⟩,
    exact H,
    exfalso,
    have : z ∈ U y ∩ S, from ⟨hzy, hz⟩,
    rwa hU' y (hT y H) at this },
  rw this,
  exact T.finite_to_set
end

[Patrick Massot]

It's really not polished at all, but it types-check.

[Bhavik Mehta]

Thank you!

[Patrick Massot]

A bit of polish:

example {α : Type*} [topological_space α] {S : set α} (hS : is_compact S) (hS' : S.infinite) :
  ∃ z ∈ S, (𝓝[≠] z ⊓ 𝓟 S).ne_bot :=
begin
  simp_rw inf_principal_ne_bot_iff,
  by_contra' H,
  apply hS',
  simp_rw [← ne_empty_iff_nonempty, not_ne_iff] at H,
  choose! U hU hU' using H,
  obtain ⟨T: finset α,  hT : ↑T ⊆ S, hT': S ⊆ ⋃ x ∈ T, insert x (U x)⟩ :=
    hS.elim_nhds_subcover (λ a, insert a (U a)) (λ z hz, insert_mem_nhds_iff.mpr (hU z hz)),
  have : S = T,
  { apply subset.antisymm _ hT,
    intros z hz,
    specialize hT' hz,
    simp only [mem_Union, mem_insert_iff, exists_prop] at hT',
    rcases hT' with ⟨y, H, rfl | hzy⟩,
    exact H,
    exfalso,
    have : z ∈ U y ∩ S, from ⟨hzy, hz⟩,
    rwa hU' y (hT H) at this },
  rw this,
  exact T.finite_to_set
end

[Vincent Beffara]

With a sequence :wink:

example {S : set ℂ} (hS : is_compact S) (hS' : S.infinite) :
  ∃ z ∈ S, (𝓝[≠] z ⊓ 𝓟 S).ne_bot :=
begin
  let f := hS'.nat_embedding S,
  obtain ⟨ℓ, hℓ, φ, hφ1, hφ2⟩ := hS.is_seq_compact (λ n, (f n).prop),
  refine ⟨ℓ, hℓ, inf_principal_ne_bot_iff.mpr (λ U hU, _)⟩,
  have h3 := hφ2 (insert_mem_nhds_iff.mpr hU), simp at h3,
  have h4 : ∃ N, ∀ n, N ≤ n → (f n).val ≠ ℓ,
    { by_contra',
      obtain ⟨n₁, h₁, h'₁⟩ := this 0,
      obtain ⟨n₂, h₂, h'₂⟩ := this (n₁ + 1),
      linarith [f.inj' (subtype.coe_injective (h'₁.trans h'₂.symm))] },
  obtain ⟨N, hN⟩ := h4,
  obtain ⟨N', hN'⟩ := h3,
  specialize hN' (N ⊔ N') le_sup_right,
  specialize hN (φ (N ⊔ N')) _,
  refine le_sup_left.trans (hφ1.id_le _),
  refine ⟨f (φ (N ⊔ N')), _⟩,
  simp [hN, hN'],
  exact hN'.resolve_left hN
end

[Junyan Xu]

Generalization to any topological space:

import order.filter.basic
import topology.subset_properties
import topology.basic

open_locale filter topological_space

example {X} [topological_space X] {S : set X} (hS : is_compact S) (hS' : S.infinite) :
  ∃ z ∈ S, (𝓝[≠] z ⊓ 𝓟 S).ne_bot :=
begin
  contrapose! hS',
  simp_rw [filter.not_ne_bot, filter.inf_principal_eq_bot, mem_nhds_within] at hS',
  have := hS.elim_nhds_subcover' (λ z hz, Sᶜ ∪ {z}) (λ z hz, _),
  { obtain ⟨t, ht⟩ := this,
    refine set.not_infinite.2 ((t.finite_to_set.image $ λ x : S, x.1).subset $ λ x hx, _),
    specialize ht hx, simp_rw set.mem_Union at ht,
    obtain ⟨y, hy, hx'|hx'⟩ := ht,
    exacts [(hx' hx).elim, ⟨y, hy, hx'.symm⟩] },
  { obtain ⟨u, hu, hzu, hs⟩ := hS' z hz,
    simp only [mem_nhds_iff, set.union_comm],
    exact ⟨u, set.diff_subset_iff.1 hs, hu, hzu⟩ },
end

[Junyan Xu]

The idea is that if S has no accumulation point then every point is isolated so it's a discrete subspace of X, which is compact iff it's finite.

[Patrick Massot]

My version was already in the same generality, with almost the same proof. The issue is not to compress a couple of lines, it is adding some api lemmas to make it obvious. Concretely, the target is to avoid using covers (which are really bad taste from a mathlib point of view). I'm away from my computer all day but I will do it tonight.

[Anatole Dedecker]

Ah, it’s a shame that I didn’t see that earlier because I’ve thought quite deeply about this last year during my course on holomorphic functions (and I’ve been explaining it periodically to some of my friends since then). Of course we weren’t talking about filters but the generalization is pretty straightforward. The proof I’ve been taught is the one Junyan describes, and I think that this is the right one but we don’t have the API ready for this. Basically I think any mathlib proof should go through docs#finite_of_compact_of_discrete.

[Anatole Dedecker]

We might also be able to cook up a direct proof not going through covers, but I think we want to have all the API to make that proof trivial anyway, so I don’t think it is a problem to transitively use covers

[Anatole Dedecker]

That said, Adam's suggestion does look nice, at least in the non-relative case:

import topology.subset_properties
import order.filter.ultrafilter

open_locale filter topological_space

open filter set

lemma foo (α : Type*) [topological_space α] [compact_space α] [infinite α] :
  ∃ z : α, (𝓝[≠] z).ne_bot :=
begin
  let f := hyperfilter α,
  have : ((f : filter α) ⊓ 𝓟 {f.Lim}ᶜ).ne_bot,
  { rw ← not_mem_iff_inf_principal_compl,
    exact (finite_singleton _).nmem_hyperfilter },
  exact ⟨f.Lim, @@ne_bot_of_le this (inf_le_inf_right (𝓟 {f.Lim}ᶜ) f.le_nhds_Lim)⟩
end

[Anatole Dedecker]

Going from the absolute case to the relative case is then a bit annoying, but here it is:

example {α : Type*} [topological_space α] {S : set α} (hS : is_compact S) (hS' : S.infinite) :
  ∃ z ∈ S, (𝓝[≠] z ⊓ 𝓟 S).ne_bot :=
begin
  haveI : compact_space S := is_compact_iff_compact_space.mp hS,
  haveI : infinite S := hS'.to_subtype,
  rcases foo S with ⟨⟨z, hzS⟩, hz⟩,
  refine ⟨z, hzS, @@ne_bot_of_le (@@filter.map_ne_bot (coe : S → α) hz) _⟩,
  rw [nhds_within, nhds_within, map_inf subtype.coe_injective, inf_assoc, inf_principal,
      map_principal, ← subtype.image_preimage_coe, preimage_compl],
  refine inf_le_inf (continuous_subtype_coe).continuous_at
    (principal_mono.mpr $ monotone_image $ compl_subset_compl.mpr _),
  rintros x (rfl : coe x = z),
  ext,
  refl
end

[Anatole Dedecker]

Here is my last word, now I have to focus on the lecture:

import topology.subset_properties
import order.filter.ultrafilter

open_locale filter topological_space

open filter set

lemma foo (α : Type*) [topological_space α] [compact_space α] [infinite α] :
  ∃ z : α, (𝓝[≠] z).ne_bot :=
begin
  let f := hyperfilter α,
  have : ((f : filter α) ⊓ 𝓟 {f.Lim}ᶜ).ne_bot,
  { rw ← not_mem_iff_inf_principal_compl,
    exact (finite_singleton _).nmem_hyperfilter },
  exact ⟨f.Lim, @@ne_bot_of_le this (inf_le_inf_right (𝓟 {f.Lim}ᶜ) f.le_nhds_Lim)⟩
end

lemma nhds_within_inf_principal {α : Type*} [topological_space α] {S T : set α} {x : α} :
  𝓝[S] x ⊓ 𝓟 T = 𝓝[T] x ⊓ 𝓟 S :=
by rw [nhds_within, nhds_within, inf_assoc, @inf_comm _ _ (𝓟 _), ← inf_assoc]

example {α : Type*} [topological_space α] {S : set α} (hS : is_compact S) (hS' : S.infinite) :
  ∃ z ∈ S, (𝓝[≠] z ⊓ 𝓟 S).ne_bot :=
begin
  haveI : compact_space S := is_compact_iff_compact_space.mp hS,
  haveI : infinite S := hS'.to_subtype,
  rcases foo S with ⟨⟨z, hzS⟩, hz⟩,
  refine ⟨z, hzS, @@ne_bot_of_le (@@filter.map_ne_bot (coe : S → α) hz) _⟩,
  rw [nhds_within, map_inf subtype.coe_injective, ← nhds_within_eq_map_subtype_coe,
      nhds_within_inf_principal, map_principal],
  refine inf_le_inf_left _ (principal_mono.mpr _),
  convert image_compl_subset subtype.coe_injective,
  rw [image_singleton, singleton_eq_singleton_iff],
  refl
end

[Bhavik Mehta]

I realised that we can use cluster_pt, just slightly differently: cluster_pt x (𝓟 (S \ {x})) ↔ (𝓝[≠] x ⊓ 𝓟 S).ne_bot ↔ x ∈ closure (S \ {x})

[Anatole Dedecker]

Last version, proving directly the relative case, is still not satisfying, and I need to stop playing with this :sweat_smile:

import topology.subset_properties
import order.filter.ultrafilter

open_locale filter topological_space

open filter set

lemma map_coe_le_principal {α : Type*} {S : set α} {f : filter S} : map coe f ≤ 𝓟 S :=
le_principal_iff.mpr $ @@mem_of_superset (@univ_mem _ f) (λ x _, x.2)

example {α : Type*} [topological_space α] {S : set α} (hS : is_compact S) (hS' : S.infinite) :
  ∃ z ∈ S, (𝓝[≠] z ⊓ 𝓟 S).ne_bot :=
begin
  simp_rw [nhds_within, inf_assoc, inf_principal],
  haveI : infinite S := hS'.to_subtype,
  let f : ultrafilter α := ultrafilter.map coe (hyperfilter S),
  rcases hS.ultrafilter_le_nhds f map_coe_le_principal with ⟨z, hzS, hz⟩,
  have : ((f : filter α) ⊓ 𝓟 ({z}ᶜ ∩ S)).ne_bot,
  { rw [← compl_compl S, ← compl_union, ← not_mem_iff_inf_principal_compl],
    change coe ⁻¹' _ ∉ hyperfilter S,
    rw [preimage_union, subtype.preimage_coe_compl, union_empty],
    exact ((finite_singleton _).preimage $ subtype.coe_injective.inj_on _).nmem_hyperfilter },
  refine ⟨z, hzS, @@ne_bot_of_le this (inf_le_inf_right _ hz)⟩
end

[Anatole Dedecker]

I'd say we should add API for both the version through docs#finite_of_compact_of_discrete and the version using ultrafilters and then see which one is cleaner, because both proofs should be easier than what they are right now

[Patrick Massot]

Here is my proposal filling API holes for the finite_of_compact_of_discrete route:

import topology.subset_properties

open_locale filter topological_space

open filter set

lemma filter.principal_eq_map_coe_top {α : Type*} (s : set α) : 𝓟 s = map (coe : s → α) ⊤ :=
by simp

open filter

lemma filter.inf_principal_eq_bot_iff_comap {α : Type*} {f : filter α} {s : set α} :
  f ⊓ 𝓟 s = ⊥ ↔ comap (coe : s → α) f = ⊥ :=
by rw [filter.principal_eq_map_coe_top s, ← filter.push_pull',inf_top_eq, map_eq_bot_iff]

variables {α : Type*} [topological_space α]

lemma discrete_topology_iff_nhds : discrete_topology α ↔ ∀ x : α, 𝓝 x = pure x :=
begin
  split ; introI h,
  { intro x,
    rw nhds_discrete },
  { constructor,
    apply eq_of_nhds_eq_nhds,
    simp [h, nhds_discrete] },
end

lemma discrete_topology_iff_nhds_neq : discrete_topology α ↔ ∀ x : α, 𝓝[≠] x = ⊥ :=
begin
  rw discrete_topology_iff_nhds,
  apply forall_congr (λ x, _),
  rw [nhds_within, inf_principal_eq_bot, compl_compl],
  split ; intro h,
  { rw h,
    exact singleton_mem_pure },
  { exact le_antisymm (le_pure_iff.mpr h) (pure_le_nhds x) }
end

lemma subtype.discrete_topology_iff {S : set α} : discrete_topology S ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥ :=
begin
  rw [discrete_topology_iff_nhds_neq, set_coe.forall'],
  apply forall_congr (λ x, _),
  rw [filter.inf_principal_eq_bot_iff_comap, nhds_within, nhds_within, comap_inf, comap_principal,
      preimage_compl, ← image_singleton, function.injective.preimage_image subtype.coe_injective,
      nhds_induced]
end

lemma is_compact.finite {S : set α} (hS : is_compact S) (hS' : discrete_topology S) : S.finite :=
finite_coe_iff.mp (@finite_of_compact_of_discrete _ _ (is_compact_iff_compact_space.mp hS) hS')


example {α : Type*} [topological_space α] {S : set α} (hS : is_compact S) (hS' : S.infinite) :
  ∃ z ∈ S, (𝓝[≠] z ⊓ 𝓟 S).ne_bot :=
begin
  by_contra' H,
  simp_rw not_ne_bot at H,
  exact hS' (hS.finite $ subtype.discrete_topology_iff.mpr H),
end

[Patrick Massot]

I'll do the ultrafilter road later.

[Patrick Massot]

I went back to this. Now I claim the preliminaries for both roads are:

import topology.subset_properties

open_locale filter topological_space

open set

namespace filter
lemma principal_eq_map_coe_top {α : Type*} (s : set α) : 𝓟 s = map (coe : s → α) ⊤ :=
by simp

lemma inf_principal_eq_bot_iff_comap {α : Type*} {f : filter α} {s : set α} :
  f ⊓ 𝓟 s = ⊥ ↔ comap (coe : s → α) f = ⊥ :=
by rw [filter.principal_eq_map_coe_top s, ← filter.push_pull',inf_top_eq, map_eq_bot_iff]

lemma ne_bot_of_comap {α β : Type*} {f : α → β} {F : filter β} (h : (comap f F).ne_bot) : F.ne_bot :=
begin
  rw ne_bot_iff at *,
  contrapose! h,
  rw h,
  exact comap_bot
end
end filter

open filter

variables {α : Type*} [topological_space α]

lemma discrete_topology_iff_nhds : discrete_topology α ↔ ∀ x : α, 𝓝 x = pure x :=
begin
  split ; introI h,
  { intro x,
    rw nhds_discrete },
  { constructor,
    apply eq_of_nhds_eq_nhds,
    simp [h, nhds_discrete] },
end

lemma discrete_topology_iff_nhds_neq : discrete_topology α ↔ ∀ x : α, 𝓝[≠] x = ⊥ :=
begin
  rw discrete_topology_iff_nhds,
  apply forall_congr (λ x, _),
  rw [nhds_within, inf_principal_eq_bot, compl_compl],
  split ; intro h,
  { rw h,
    exact singleton_mem_pure },
  { exact le_antisymm (le_pure_iff.mpr h) (pure_le_nhds x) }
end

lemma subtype.nhds_within_eq_bot_iff {s t : set α} {x : s} :
  𝓝[(coe : s → α) ⁻¹' t] x = ⊥ ↔ 𝓝[t] (x : α) ⊓ 𝓟 s = ⊥ :=
by rw [inf_principal_eq_bot_iff_comap, nhds_within, nhds_within, comap_inf, comap_principal,
       nhds_induced]

lemma subtype.nhds_ne_eq_bot_iff {S : set α} {x : S} : 𝓝[{x}ᶜ] x = ⊥ ↔ 𝓝[{x}ᶜ] (x : α) ⊓ 𝓟 S = ⊥ :=
by rw [← subtype.nhds_within_eq_bot_iff, preimage_compl, ← image_singleton,
       subtype.coe_injective.preimage_image ]

lemma subtype.nhds_ne_ne_bot_iff {S : set α} {x : S} :
  (𝓝[{x}ᶜ] x).ne_bot ↔ (𝓝[{x}ᶜ] (x : α) ⊓ 𝓟 S).ne_bot :=
by rw [ne_bot_iff, ne_bot_iff, not_iff_not, subtype.nhds_ne_eq_bot_iff]

lemma subtype.discrete_topology_iff {S : set α} : discrete_topology S ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥ :=
by simp_rw [discrete_topology_iff_nhds_neq, set_coe.forall', subtype.nhds_ne_eq_bot_iff]

lemma is_compact.finite {S : set α} (hS : is_compact S) (hS' : discrete_topology S) : S.finite :=
finite_coe_iff.mp (@finite_of_compact_of_discrete _ _ (is_compact_iff_compact_space.mp hS) hS')

[Patrick Massot]

And then we get to choose between the discrete road:

example (α : Type*) [topological_space α] [compact_space α] [infinite α] :
  ∃ z : α, (𝓝[≠] z).ne_bot :=
begin
  by_contra' H,
  simp_rw not_ne_bot at H,
  haveI := discrete_topology_iff_nhds_neq.mpr H,
  exact infinite.not_finite (finite_of_compact_of_discrete : finite α),
end

example {α : Type*} [topological_space α] {S : set α} (hS : is_compact S) (hS' : S.infinite) :
  ∃ z ∈ S, (𝓝[≠] z ⊓ 𝓟 S).ne_bot :=
begin
  by_contra' H,
  simp_rw not_ne_bot at H,
  exact hS' (hS.finite $ subtype.discrete_topology_iff.mpr H),
end

and the ultrafilter road:

lemma foo (α : Type*) [topological_space α] [compact_space α] [infinite α] :
  ∃ z : α, (𝓝[≠] z).ne_bot :=
begin
  let f := hyperfilter α,
  have : ((f : filter α) ⊓ 𝓟 {f.Lim}ᶜ).ne_bot,
    from not_mem_iff_inf_principal_compl.mp (finite_singleton _).nmem_hyperfilter,
  exact ⟨f.Lim, @@ne_bot_of_le this (inf_le_inf_right _ f.le_nhds_Lim)⟩
end

example {α : Type*} [topological_space α] {S : set α} (hS : is_compact S) (hS' : S.infinite) :
  ∃ z ∈ S, (𝓝[≠] z ⊓ 𝓟 S).ne_bot :=
begin
  haveI : compact_space S := is_compact_iff_compact_space.mp hS,
  haveI : infinite S := hS'.to_subtype,
  rcases foo S with ⟨⟨z, hzS⟩, hz⟩,
  refine ⟨z, hzS, subtype.nhds_ne_ne_bot_iff.mp hz⟩
end

[Patrick Massot]

Anatole, note in particular how deducing the relative version from the absolute one is now painless.

[Patrick Massot]

And of course the last proof above deducing the relative version from the absolute one could also be used in the discrete road.

[Patrick Massot]

I just opened #16862. I used the discrete set path since it is more elementary and not longer, but I included preliminary lemmas for both proofs.

[Vincent Beffara]

Should we also settle on one definition to be named accumulation_pt and something or other for the relative version, and add two tfae lemmas for the various equivalent versions? And use that instead of the explicit ne_bot version in mathlib where possible?

[Bhavik Mehta]

Vincent Beffara said:

Should we also settle on one definition to be named accumulation_pt and something or other for the relative version, and add two tfae lemmas for the various equivalent versions? And use that instead of the explicit ne_bot version in mathlib where possible?

I don't think this is necessary any more, since we can use cluster_pt x (𝓟 (S \ {x})) in place of (𝓝[≠] x ⊓ 𝓟 S).ne_bot

[Bhavik Mehta]

Patrick Massot said:

I just opened #16862. I used the discrete set path since it is more elementary and not longer, but I included preliminary lemmas for both proofs.

Thanks so much for this Patrick!

[Vincent Beffara]

Bhavik Mehta said:

Vincent Beffara said:

Should we also settle on one definition to be named accumulation_pt and something or other for the relative version, and add two tfae lemmas for the various equivalent versions? And use that instead of the explicit ne_bot version in mathlib where possible?

I don't think this is necessary any more, since we can use cluster_pt x (𝓟 (S \ {x})) in place of (𝓝[≠] x ⊓ 𝓟 S).ne_bot

I'm not sure I agree with this, especially if one of our goals is to cover the whole undergrad curriculum and be accessible to "normal mathematicians" who know about accumulation points and not about filters. They would likely prefer either x ∈ closure (S \ {x}) or perhaps ∃ᶠ z in 𝓝[≠] x, z ∈ S (which I always read in my head as "there is a sequence tending to x, except without the pathological stuff about sequences not appearing because something something filter). That being the same as a statement in terms of principal filters, which indeed make some proofs easier further down the line, is an "implementation detail", and IMHO should be hidden from the API.

After all we do have a definition of continuous_at in mathlib even though we could inline it everywhere as tendsto f (𝓝 x) (𝓝 (f x)) :grinning:

[Patrick Massot]

The cluster_pt definition was already introduced for the sake of having more readable statements. This has a cost since every definition must come with lemmas, otherwise the first step in any proof is always to unfold the definition. But if there are sufficiently many statements that would benefit from the definition then it can be worth the trouble. So you can try. Note also that tendsto f A B is already a somewhat useless wrapper around the core definitions which are docs#filter.map and docs#filter.partial_order, and map f A ≤ B is actually shorter to type and more evocative. And you can read ∃ᶠ z in 𝓝[≠] x, z ∈ S as "there exist a point near x but different from x that belongs to S", without thinking in terms of sequences.

[Vincent Beffara]

Agreed on everything, except that very few people in math departments would find map f A ≤ B on filters to be more evocative than tendsto or continuous_at :-) and tendsto is not so useless if it is close to everyday mathematicians' use while at the same time enabling dot-notation use in proofs.

I was partly joking about ∃ᶠ (only partly because depending on the kind of math one is doing, "you can find a point arbitrarily close to x" and "you can find a sequence that converges to x" can feel indistinguishable), but I maintain that informal mathematicians would prefer it to cluster points of filters...

[Patrick Massot]

Sure, I wasn't suggesting we get rid of tendsto, this was an argument in favor of keeping "useless" definitions. It would still be nice to have more mathematicians thinking in terms of filters, but this is unlikely to happen.