Stream: maths

Topic: compact spaces

Reid Barton (Sep 22 2018 at 20:24):

I'm inclined to add the following class, following the naming scheme of t2_space, separable_space, etc.

structure compact_space {α : Type*} [topological_space α] :=
(compact_univ : compact (univ : set α))


Advantages: we can write a lot of instances, and various theorems have "$X$ compact" as a hypothesis, and it's not always possible or useful to generalize to "Let $S$ be a compact subset of $X$".

Any thoughts?

Kevin Buzzard (Sep 22 2018 at 20:51):

My only comment was that ever since I saw the definition of compact I was surprised it applied to a subspace rather than the space. What is the advantage of the subset approach? It's not how mathematicians traditionally do it.

Mario Carneiro (Sep 22 2018 at 22:32):

I agree. I don't think there is much advantage to working with subsets here, since you get exactly the right behavior with compact_space s with the subtype coercion

Last updated: May 18 2021 at 07:19 UTC