compact spaces

Stream: maths

[Reid Barton]

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$".

[Reid Barton]

Any thoughts?

[Kevin Buzzard]

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]

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