Small addition to topology.connected

Stream: maths

[Antoine Chambert-Loir]

As a first test in writing a few lines in Lean, I formalized the minor generalization of the theorem is_preconnected.closure that says that if s is connected then its closure is connected as well. The statement is : if s is connected, then for all t such that s ⊆ t ∧ t ⊆ closure s, t is connected.

theorem is_preconnected.inclosure {s : set α} {t : set α}
  (H : is_preconnected s) (K : s ⊆ t ∧ t ⊆ closure s) :
  is_preconnected (t) :=
λ u v hu hv htuv ⟨y, hyt, hyu⟩ ⟨z, hzt, hzv⟩ ,
let ⟨p, hpu, hps⟩ := mem_closure_iff.1 (K.right hyt) u hu hyu in
let ⟨q, hqv, hqs⟩ := mem_closure_iff.1 (K.right hzt) v hv hzv in
let ⟨r, hrs, hruv⟩ := H u v hu hv (subset.trans K.left htuv)
  ⟨p, hps, hpu⟩ ⟨q, hqs, hqv⟩ in ⟨r, K.left hrs, hruv⟩

There is the analogous is_connected.inclosure.
I'd gladly try a pull request.

One question is whether is_preconnected.closure and is_connected.closure should be redefined as corollaries of that more general statement, or left untouched.

[Adam Topaz]

Looks like a good lemma that should certainly be in mathlib!

One minor comment: It would be better to split up your hypothesis (K : s ⊆ t ∧ t ⊆ closure s) into two hypotheses (h1 : s ⊆ t) and (h2 : t ⊆ closure s). In practice, it's easier to apply lemmas when their hypotheses are split up like this.

The proof of is_precommented.closure is essentially the same, so I do think it's worthwhile to simplify its proof using this generalization (and similarly for is_connected.closure).

[Scott Morrison]

Let us know your github username here, and we can give you permission to push branches to the repository.

[Antoine Chambert-Loir]

It is AntoineChambert-Loir

[Johan Commelin]

@Antoine Chambert-Loir Voila: https://github.com/leanprover-community/mathlib/invitations

[Antoine Chambert-Loir]

Bien reçu, thanks! (Now, I need to understand how to make git push --set-upstream origin bark_treework, I am struggling with authentification.

[Patrick Massot]

Did you put a public ssh key on GitHub?

[Floris van Doorn]

See https://docs.github.com/en/authentication/connecting-to-github-with-ssh/generating-a-new-ssh-key-and-adding-it-to-the-ssh-agent on how to authenticate using SSH with Github. (In step 7 you'll be redirected to a different page where you have to add your ssh key to Github, as Patrick mentions).

[Floris van Doorn]

It's quite some steps, but it is a one-time thing (1 time per device you use)

[Antoine Chambert-Loir]

I had done all that, and ssh -T git@ssh.github.com works as indicated, but the git push keeps asking me for username and password…

[Alex J. Best]

Does the advice at https://stackoverflow.com/questions/6565357/git-push-requires-username-and-password help?

[Matthew Ballard]

Is this linux or macos?

[Johan Commelin]

@Antoine Chambert-Loir Did you clone the repo using ssh or https? I think that if you clone using https (which might be the default), it will ask for a password.

[Adam Topaz]

If you don't have an ssh key set up on your local machine, I think leanproject will automatically pull using https instead of ssh.
Honestly it's a bit of a pain to manually edit the git config file in this case.

[Antoine Chambert-Loir]

Yes, finally, I made it, thanks!
It has been necessary to add some git remote set-url origin git@github.com:leanprover-community/mathlib.git so that the git command uses ssh-authentication rather than https.

[Antoine Chambert-Loir]

So, it seems that I'm now the proud author of a PR. Let's see what happens next!
(Bad news, I'm in the midst of proving another easy lemma…)

[Adam Topaz]

@Antoine Chambert-Loir if you paste your PR number with a #, it will automatically generate a link (e.g. #9633 )

[Antoine Chambert-Loir]

OK, thanks! What do I need to do now?
In particular, with respect to the stylistic adjustments made by @Adam Topaz and @Johan Commelin ? Do I need to implement them myself or are they already implemented into PR #9633?

[Adam Topaz]

Johan and I left some comments, but you should decide what changes to actually make.
Github's PR system lets commenters suggest explicit changes in the code, so as you can see there are some comments which have a button saying commit suggestion or something like that.

It's a matter of personal taste whether you want to actually use these buttons, or implement the changes in your editor and commit/push manually (personally, I prefer to make the changes in the editor unless it's something very trivial).

[Adam Topaz]

Any additional commits you make to this branch (and push to the branch on github) will automatically show up in the PR.

[Adam Topaz]

when you're done making the changes, it's good practice to remove the awating author and add the awaiting review label in the PR. This is a signal to the maintainers that the PR is ready for further review.

[Adam Topaz]

@Antoine Chambert-Loir one more thing to note: if you look at your PR, you will see an icon next to your most recent commit
Screenshot-2021-10-08-at-16-08-42-feattopology-connected-lean-add-theorems-about-connectedness-o...-by-AntoineChambert-Loir....png
The little red X indicates that the continuous integration checks have failed for some reason. You can click on this to see what went wrong (this is only relevant for the most recent commit, as a push cancels the checks for previous commits). In this case, you have a line that is too long (which you can also see by clicking on Files Changed near the top of the PR page.

[Antoine Chambert-Loir]

Yes, I just saw this and pushed a new commit.

[Antoine Chambert-Loir]

I pushed a new PL #10005 with another classic result on connected spaces. I fear it will require some rewriting, but let's see!