Cantor-Bendixson

Stream: maths

[Felix Weilacher]

Hi all,

I've been working on the Cantor-Bendixson theorem, following Chapter 6 of Kechris. I thought I'd share what I have here and ask what people think. The complete file is here.

The main things are:

A definition of a perfect subset of a topological space:

def perfect [topological_space α ] (C : set α) : Prop :=
  is_closed C ∧ ∀ x ∈ C, ∀ U ∈ nhds x, ∃ y ∈ U ∩ C, y ≠ x

def perf_nonempty [topological_space α] (C : set α) : Prop := set.nonempty C ∧ perfect C

Any perfect nonempty subset of a complete metric space contains a homeomorphic copy of the Cantor space:

theorem cantor_of_perf_nonempty [metric_space α] [complete_space α] {C : set α}
  (hC : perf_nonempty C) : ∃ f : (ℕ → bool) → α,
  (range f) ⊆ C ∧ continuous f ∧ injective f

Any closed subset of a second countable space can be written as the union of a perfect set and a countable set:

theorem ctble_union_perfect_of_closed [second_countable_topology α] {C : set α} (hclosed : is_closed C) :
∃ V D : set α, (V.countable) ∧ (perfect D) ∧ (C = V ∪ D)

Combining these two, any uncountable closed subset of a Polish space contains a homeomorphic copy of the Cantor space:

theorem cantor_of_closed_unc [polish_space α] {C : set α}
  (hclosed : is_closed C) (hunc : ¬ C.countable) :
  ∃ f : (ℕ → bool) → α, (range f) ⊆ C ∧ continuous f ∧ function.injective f

[Vincent Beffara]

It might be relevant to look at a recent discussion about accumulation points here https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Accumulation.20point for the definition of perfect subsets

[Felix Weilacher]

Vincent Beffara said:

It might be relevant to look at a recent discussion about accumulation points here https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Accumulation.20point for the definition of perfect subsets

I see, so ∀ U ∈ nhds x, ∃ y ∈ U ∩ C, y ≠ x could be (𝓝[≠] x ⊓ 𝓟 C).ne_bot or ∃ᶠ y in 𝓝[≠] x, y ∈ C ?

[Vincent Beffara]

Yes, exactly. Or ∃ᶠ y in 𝓝[C] x, y ≠ x which would match what you wrote.
Or if you are building some API around prefect subsets, maybe it would be a good occasion to introduce accumulation_pt C x or something like this if it makes sense to have API for that as well.

[Felix Weilacher]

By the way, is ℕ → bool the best way to represent the Cantor space? There are a lot of 2 element types and I'm not sure which are preferred for which situations.

[Adam Topaz]

I think bool is the only two-term type with a topological space instance by default, so I would say, yes!

[Adam Topaz]

we have docs#sierpinski_space as well, but that’s not the right topology

[Mario Carneiro]

doesn't fin n have a topology?

[Adam Topaz]

Does it?

[Mario Carneiro]

(not that I disagree with your judgment here, just being pedantic)

[Mario Carneiro]

I would expect it to be equipped with the discrete topology

[Mario Carneiro]

otherwise stuff like R^n would not "just work"

[Adam Topaz]

Sure it would, you don’t need a topology on the domain, but rather the codomain

[Mario Carneiro]

oh, is it not using compact-open?

[Adam Topaz]

No it’s the product topology

[Adam Topaz]

docs#Pi.topological_space

[Mario Carneiro]

ah right, compact-open is for C(A, B)

[Mario Carneiro]

but I think it probably still comes up when looking at those spaces in the finite dimensional case

[Yaël Dillies]

Doesn't Prop also get a topology by default?

[Mario Carneiro]

it does but it's the sierpinski topology

[Yaël Dillies]

Hmm, that instance is badly named, then.

[Mario Carneiro]

really? It's literally called docs#sierpinski_space which seems apt

[Yaël Dillies]

There's no Prop in the name! Every time I've looked for a topology on Prop, I look for Prop.topological_space, which doesn't exist, so surely it does not have a topology. But clearly it does, so it must come from another instance through the order.

[Mario Carneiro]

If it was called Prop.topological_space it would be a lot less obvious that it's the sierpinski topology

[Yaël Dillies]

That's what docstrings are for.

[Mario Carneiro]

who looks at docstrings on instances?

[Yaël Dillies]

sierpinski_space sounds like the topology given to a type synonym, not the topology given to Prop itself.

[Yaël Dillies]

I do, for a fact.

[Mario Carneiro]

I mean I'm sure that's a self-fulfilling prophecy

[Mario Carneiro]

Yaël Dillies said:

sierpinski_space sounds like the topology given to a type synonym, not the topology given to Prop itself.

I think this is the deeper issue. I'm curious whether the topology has ever been used in mathlib, and if so whether it was an error

[Mario Carneiro]

it strikes me as something that was added just because the sierpinski space is cool

[Yaël Dillies]

Oh actually, doesn't that make the compact-open topology on α → Prop the correct topology on set α?

[Adam Topaz]

The whole point of the Sierpinski space is that continuous functions from X to it correspond to open sets in X.

[Adam Topaz]

I don't really understand what you mean by the '"correct" topology on set X, and you also didn't restrict to continuous maps.

[Adam Topaz]

I think I used this space somewhere in the context of profinite sets (I don't remember if this was in LTE or mathlib)

[Reid Barton]

I used it here to prove that a pushout of an embedding is an embedding.

[Reid Barton]

I'm confused why one would look for instances by name rather than using #check infer_instance or whatever.

[Reid Barton]

In general, the Sierpinski space is quite useful for working out the topology of colimits because maps from X into it correspond to open sets of X as mentioned above, and a colimit X is defined in terms of how to map out of it.

[Patrick Stevens]

(If one is looking by name, is there anything wrong with adding the name Prop.topological_space_sierpinski?)