[Merged by Bors] - refactor(topology/subset_properties): more properties of compact_covering

[urkud]

Modify the definition of compact_covering α n to ensure that it is monotone in n.

Also, in a locally compact space, prove the existence of a compact exhaustion, i.e. a sequence which satisfies the properties for compact_covering and in which, moreover, the interior of the next set includes the previous set.

---

• depends on: [Merged by Bors] - chore(topology): move exists_compact_superset, drop assumption t2_space #6327
• depends on: [Merged by Bors] - chore(topology/bases): golf a proof #6326 (actually, unrelated but it's already on the queue)

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - chore(topology): move exists_compact_superset, drop assumption t2_space #6327
• [Merged by Bors] - chore(topology/bases): golf a proof #6326

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[hrmacbeth]

Given the redefinition to require that the covering be monotone, I propose renaming to compact_exhaustion, which is standard enough terminology that (eg) it is used on Wikipedia; what do you think?

Edit -- I read your definition more closely, I see that your definition does not always have the "closure subset interior" property, so my suggestion was wrong.

But how about adding the definition

def compact_exhaustion (K : ℕ → set α) : Prop := (∀ n, is_compact (K n)) ∧
  (∀ n, K n ⊆ interior (K (n + 1))) ∧ (⋃ n, K n) = univ

(probably as a structure), and separately changing the definition of compact_covering to require monotonicity (without the part about upgrading it if possible) -- then just making two separate series of lemmas? It's not immediately clear to me why it would be beneficial to combine the two definitions in an "if possible, extra properties" way, as you do.

[hrmacbeth]

Also, is [sigma_compact_space α] equivalent to (cocompact α).is_countably_generated? Might this redefinition streamline some proofs? I could try it sometime if you think it's a good idea.

[urkud]

You're right, it's easier to have two definitions. Modified.

[urkud]

Also, is [sigma_compact_space α] equivalent to (cocompact α).is_countably_generated? Might this redefinition streamline some proofs? I could try it sometime if you think it's a good idea.

Seems to be true but I'm not sure that this is useful for golfing proofs.

[hrmacbeth]

Nice! This review is mostly docstring suggestions, feel free to take or leave. (I made a rough edit of the PR comment, too.)

[hrmacbeth]

I have a question about strategy. You could have made a definition

structure compact_exhaustion := 
(K : ℕ → set α) 
(compact : ∀ n, is_compact (K n))
(monotone : ∀ n, K n ⊆ interior (K (n + 1)))
(union : (⋃ n, K n) = univ)

(or some variant, eg an unbundled version

structure is_compact_exhaustion (K : ℕ → set α) : Prop := 
(compact : ∀ n, is_compact (K n))
(monotone : ∀ n, K n ⊆ interior (K (n + 1)))
(union : (⋃ n, K n) = univ)

) and then proved the lemmas such as compact_exhaustion_subset and
compact_exhaustion_subset_interior not just for the particular compact_exhaustion produced by choice, but for all compact exhaustions. (Possibly useful if, in the future, one constructs a special compact exhaustion for a proof, which has certain other properties.). Is there a reason you didn't do it this way?

[urkud]

The main reason is that we have only two lemmas not included in the definition, and they follow from is_compact_exhaustion.monotone in 1-2 lines of code.

UPD: it seems that some proofs i #6395 can be golfed using is_compact_exhaustion, lemmas, and operation "prepend empty set".

[hrmacbeth]

bors d+

Thank you for adding the compact_exhaustion structure!

If the linter is happy, feel free to merge.

[hrmacbeth]

Suggested change

	If `X` is a locally compact sigma compact space, then `compact_exhaustion.some X` provides a choice
	If `X` is a locally compact sigma compact space, then `compact_exhaustion.choice X` provides a choice

(I don't have an opinion on whether it's better to use some or choice, but I think you use choice below.)

[hrmacbeth]

Do you need the monotonicity of the general compact covering, now that you have a separate construction of compact exhaustion in the locally compact case? You could revert the edits here and on the next two lemmas. But on the other hand, it does no harm and might be useful at some point, so if you want to leave it, that's also fine with me.

[urkud]

I would prefer to leave accumulate here because the new definition is at least as useful as the old one.

[bors]

✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[urkud]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests