Zulip Chat Archive

Stream: maths

Topic: compact spaces


view this post on Zulip 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 "XX compact" as a hypothesis, and it's not always possible or useful to generalize to "Let SS be a compact subset of XX".

view this post on Zulip Reid Barton (Sep 22 2018 at 20:24):

Any thoughts?

view this post on Zulip 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.

view this post on Zulip 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