Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Cluster1 #850

Merged
merged 6 commits into from
Feb 22, 2023
Merged

Cluster1 #850

merged 6 commits into from
Feb 22, 2023

Conversation

zstone1
Copy link
Contributor

@zstone1 zstone1 commented Feb 17, 2023

Motivation for this change

This should be an easy review. We prove a classic topology result that in compact spaces, a filter F with one cluster point x converges to x. This is another nice application of the near_covering definition. I claim this formalization is a good approximation of the classical proof:

Pick an open neighborhood U of x. For each point y in ~U, the filter does not cluster at y. So we have a neighborhood V of y with F (~V). This forms a cover of ~U which is closed therefore compact. Taking finite intersections, F (~V_1 \cap ... \cap ~V_n) and ~U <= V_1 \cup ... \cup V_n -> ~V_1 \cap ... \cap ~V_n \subset U. So F converges to x.

In coq, the powerset_filter_from F encodes "finite intersections" and the property (fun x W => ~ W x) encodes the complements. Plugging these into the statement that V \ U is near_covering compact, we get a new goal to build the cover. Then given a y with ~U y we know y <> x. So ~ cluster F y, and we get our neighborhood. The rest is just bookkeeping (pushing negations through quantifiers and handling the a vacuous ~V t case).

Things done/to do
  • added corresponding entries in CHANGELOG_UNRELEASED.md
    (do not edit former entries, only append new ones, be careful:
    merge and rebase have a tendency to mess up CHANGELOG_UNRELEASED.md)
  • added corresponding documentation in the headers
Automatic note to reviewers

Read this Checklist and put a milestone if possible.

theories/topology.v Outdated Show resolved Hide resolved
Comment on lines 2863 to 2866
Proof.
apply/ predeqP => ?.
by split; [exact: compact_near_covering| exact: near_covering_compact].
Qed.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
Proof.
apply/ predeqP => ?.
by split; [exact: compact_near_covering| exact: near_covering_compact].
Qed.
Proof. by rewrite eqEsubset; exact: compact_near_coveringP. Qed.

theories/topology.v Outdated Show resolved Hide resolved
Comment on lines 3045 to 3049
have cptVU : compact (V `\` U).
apply: (subclosed_compact _ cptV) => //.
by apply: closedI; [exact: compact_closed | exact: open_closedC].
rewrite compact_near_coveringE in cptVU.
have [] := cptVU _ (powerset_filter_from F) (fun W x => ~ W x).
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is where compact_near_coveringE is used. Wouldn't

Lemma blah A : compact A <-> near_covering A.

be more useful here? We can /blah at line 3045, line 3048 is not need anymore, and we do not need to name the fact compact (V \ U). But maybe there is some combinator to from compact_near_coveringP to blah that I miss...

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it's cleaner to just change compact_near_coveringP to be compact A <-> near_covering A. It seems a bit more idiomatic. I've made the updatee with that change.

@affeldt-aist affeldt-aist self-requested a review February 22, 2023 14:57
Copy link
Member

@affeldt-aist affeldt-aist left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I just noticed that an intermediate hypothesis needn't be named but that's ok to remove this commit if you want.

@zstone1
Copy link
Contributor Author

zstone1 commented Feb 22, 2023

Sounds good, that hypo doesn't need a name.

@zstone1 zstone1 merged commit 3809ed3 into math-comp:master Feb 22, 2023
hoheinzollern pushed a commit to hoheinzollern/analysis that referenced this pull request Mar 9, 2023
* cluster1 proof

* updating changelog

* Update theories/topology.v

Co-authored-by: affeldt-aist <[email protected]>

* Update theories/topology.v

Co-authored-by: affeldt-aist <[email protected]>

* change to signature of compact_near_coveringP

* no need to name intermediate hypo

---------

Co-authored-by: affeldt-aist <[email protected]>
Co-authored-by: Reynald Affeldt <[email protected]>
proux01 pushed a commit that referenced this pull request Mar 24, 2023
* cluster1 proof

* updating changelog

* Update theories/topology.v

Co-authored-by: affeldt-aist <[email protected]>

* Update theories/topology.v

Co-authored-by: affeldt-aist <[email protected]>

* change to signature of compact_near_coveringP

* no need to name intermediate hypo

---------

Co-authored-by: affeldt-aist <[email protected]>
Co-authored-by: Reynald Affeldt <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants