[Merged by Bors] - feat(topology/connected): Connectedness of unions of sets #10005

AntoineChambert-Loir · 2021-10-27T13:54:16Z

Add multiple results about when unions of sets are (pre)connected. In particular, the union of connected sets indexed by ℕ such that each set intersects the next is connected.
Remove some set. prefixes in the file
There are two minor fixes in other files, presumably caused by the fact that they now import order.succ_pred
Co-authored by Floris van Doorn fpvdoorn@gmail.com

depends on: [Merged by Bors] - feat(order/succ_pred/relation): succ/pred inductions on relations #11518

Add a theorem that unions of preconnected sets indexed by integers such that each of them meets the next one is preconnected In a separate file (src/data/set/increasing_union.lean), add a series of possibly lemma on increasing unions It is possible that these lemmas have a neater proof.

src/data/set/increasing_union.lean

eric-wieser · 2021-10-27T14:55:25Z

src/data/set/increasing_union.lean

+
+Given a sequence of sets s : ℕ → set α,
+we construct its increasing Union by
+λ n:ℕ, Union (set restrict s { j : ℕ | j ≤ n}) -/


Are you sure you don't want

Suggested change

λ n:ℕ, Union (set restrict s { j : ℕ | j ≤ n}) -/

λ n:ℕ, Union (subtype.restrict s (≤ n)) -/

This also looks a lot like partial_sups, cc @YaelDillies

And accumulate.

Yeah it is partial_sups. I'm sorry you wrote it all, Antoine, because this is duplicate 😕

I was almost certain something like that would exist, and I am truly glad that it already exists.
I'll try to understand how it works tomorrow and to adjust the other file accordingly.

@YaelDillies , OK, it was nice and easy to use partial_sups.
At first, I thought that the assertion that partial_sups s is monotone was missing, but it seems to be included in the galois connection…

partial_sups is defined as a monotone function. That's what the little m to the right of the arrow stands for. You can look at the API for preorder_hom for how to use this.

Unfortunately, I can't read that little symbol on the right of the arrow, it is printed as a box in both vim and VisualStudio, all I know is that it has Unicode code 8344…

@AntoineChambert-Loir In that case I think you are in dire need of a font with more unicode support 😉

That I could guess, but I think I use the standard VisualStudioCode (on Mac OS)…

src/topology/connected.lean

AntoineChambert-Loir · 2021-10-28T09:21:13Z

I left unfortunate bugs in the commit (bad interaction between my two branches).
Moreover, the theorems on monotone Unions are essentially, I may simplify them.

A new commit will appear soon.

AntoineChambert-Loir · 2021-10-28T09:31:56Z

Finally, I left the two theorems is_preconnected.Union_of_monotone and is_preconnected.sUnion_of_filtered, but I wonder whether they should remain in this form.
Indeed, at least under the assumption that the sets are nonempty, they follow rightly from is_preconnected.Union. And in the case where I use them, the sets are nonempty.
What do you think?

eric-wieser

Some initial style comments

src/topology/connected.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

…thlib into ad-connectedness

src/topology/connected.lean

PatrickMassot · 2021-11-05T09:21:31Z

@AntoineChambert-Loir , I worked on the first two lemmas to show you some tricks and answer some questions. My advice is to study the diff at 1a1bb97 and see whether you can learn something and clean up this PR. Unfortunately git is a bit confused when displaying the diff (because it can't figure out which of my blank lines match yours) so you may have to create a new version of the file on your computer and compare them by putting them side by side.

src/topology/connected.lean

fpvandoorn · 2022-01-17T15:58:46Z

Thanks for the review! It is indeed much nicer to do this for is_succ_archimedean (I didn't know we had this type class).
To make the review process easier, I moved all the stuff I added about relations in a separate PR: #11518.

YaelDillies · 2022-01-17T16:26:34Z

Yeah, this is all fairly new. Nothing in mathlib uses it yet, so I'm very happy to see people needing it!

leanprover-community-bot-assistant · 2022-01-28T00:40:54Z

This PR/issue depends on:

~~[Merged by Bors] - feat(order/succ_pred/relation): succ/pred inductions on relations #11518~~
By Dependent Issues (🤖). Happy coding!

jcommelin

Thanks 🎉 It took a while, but this looks really great now!

bors merge

* Add multiple results about when unions of sets are (pre)connected. In particular, the union of connected sets indexed by `ℕ` such that each set intersects the next is connected. * Remove some `set.` prefixes in the file * There are two minor fixes in other files, presumably caused by the fact that they now import `order.succ_pred` * Co-authored by Floris van Doorn fpvdoorn@gmail.com Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

YaelDillies · 2022-02-02T16:52:37Z

src/topology/connected.lean

-theorem is_connected.Union_nat_of_chain {s : ℕ → set α}
-  (H : ∀ n : ℕ, is_connected (s n))
-  (K : ∀ n : ℕ, (s n ∩ s n.succ).nonempty) :
+/-- The Union of connected sets indexed by a type with an archimedian successor (like `ℕ` or `ℤ`)


Suggested change

/-- The Union of connected sets indexed by a type with an archimedian successor (like `ℕ` or `ℤ`)

/-- The Union of connected sets indexed by a type with an archimedean successor (like `ℕ` or `ℤ`)

YaelDillies · 2022-02-02T16:53:03Z

src/topology/connected.lean

+
+/-- The Union of connected sets indexed by a type with an archimedian successor (like `ℕ` or `ℤ`)
+  such that any two neighboring sets meet is preconnected. -/
+theorem is_preconnected.Union_of_chain {s : β → set α}


I would get rid of dot notation here and below because you can't actually use it.

I agree you cannot actually use it (though I kinda hope we can change the way projection notation works in Lean 4 so that H.Union_of_chain K works in this case).
However, I'm not sure if that means we should change the . to a _: it might be more predictable to guess the name if we consistently keep using . even when projection notation doesn't apply.

At least, there's precedent for not using it when the condition is in a forall. For example, star_convex_Union.

I believe there is a bunch of precedent for both options. We have not decided on a rule here. (measurable_set.pi to pick one)

bors · 2022-02-02T18:40:28Z

Pull request successfully merged into master.

Build succeeded:

AntoineChambert-Loir added the awaiting-review The author would like community review of the PR label Oct 27, 2021

jcommelin reviewed Oct 27, 2021

View reviewed changes

src/data/set/increasing_union.lean Outdated Show resolved Hide resolved

src/data/set/increasing_union.lean Outdated Show resolved Hide resolved

style(src/data/set/increasing_union.lean): add copyright and title

054de6b

eric-wieser reviewed Oct 27, 2021

View reviewed changes

src/data/set/increasing_union.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Oct 27, 2021

View reviewed changes

urkud reviewed Oct 27, 2021

View reviewed changes

src/topology/connected.lean Outdated Show resolved Hide resolved

Antoine Chambert-Loir added 2 commits October 28, 2021 11:01

style: use partial_sups and delete useless additions of first commit

8d563dd

style: suppress invocation of deleted file

78d7c40

AntoineChambert-Loir added incomplete and removed awaiting-review The author would like community review of the PR labels Oct 28, 2021

style: add the necessary import

efda789

AntoineChambert-Loir added awaiting-review The author would like community review of the PR and removed incomplete labels Oct 28, 2021

style: remove noisy #lint

44c592d

eric-wieser reviewed Oct 28, 2021

View reviewed changes

AntoineChambert-Loir and others added 4 commits October 28, 2021 18:15

Update src/topology/connected.lean

54d664d

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Update src/topology/connected.lean

e56689c

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

style: remove double spaces and begin/end in have

fc21ea9

Merge branch 'ad-connectedness' of github.com:leanprover-community/ma…

2215ef0

…thlib into ad-connectedness

urkud reviewed Oct 30, 2021

View reviewed changes

src/topology/connected.lean Outdated Show resolved Hide resolved

jcommelin changed the title ~~feat(src/topology/connected.lean): add a theorem on connected unions~~ feat(src/topology/connected): add a theorem on connected unions Nov 4, 2021

Use some tricks of the trade

1a1bb97

PatrickMassot added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Nov 5, 2021

YaelDillies changed the title ~~feat(src/topology/connected): add a theorem on connected unions~~ feat(topology/connected): A increasing union indexed by a chain is connected Nov 5, 2021

eric-wieser reviewed Nov 5, 2021

View reviewed changes

src/topology/connected.lean Outdated Show resolved Hide resolved

leanprover-community-bot-assistant added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jan 17, 2022

fpvandoorn mentioned this pull request Jan 17, 2022

[Merged by Bors] - feat(order/succ_pred/relation): succ/pred inductions on relations #11518

Closed

leanprover-community-bot-assistant removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jan 28, 2022

leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jan 28, 2022

fpvandoorn added 3 commits January 28, 2022 15:30

Merge remote-tracking branch 'origin/master' into ad-connectedness

adaa0e6

some preliminary fixes, probably still broken

afd5d85

fix

902b515

leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jan 28, 2022

fpvandoorn added 5 commits January 28, 2022 15:45

generalize Z

c8ffba9

sort imports

57e50aa

fix

fa3bb6a

I don't know why this simplified

9b4aaf5

Merge remote-tracking branch 'origin/master' into ad-connectedness

ff5f06a

fpvandoorn added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Feb 1, 2022

fpvandoorn changed the title ~~feat(topology/connected): A increasing union indexed by a chain is connected~~ feat(topology/connected): Connectedness of unions Feb 2, 2022

fpvandoorn changed the title ~~feat(topology/connected): Connectedness of unions~~ feat(topology/connected): Connectedness of unions of sets Feb 2, 2022

rename some results and generalize nat to succ_order

769a491

jcommelin approved these changes Feb 2, 2022

View reviewed changes

leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Feb 2, 2022

YaelDillies reviewed Feb 2, 2022

View reviewed changes

bors bot changed the title ~~feat(topology/connected): Connectedness of unions of sets~~ [Merged by Bors] - feat(topology/connected): Connectedness of unions of sets Feb 2, 2022

bors bot closed this Feb 2, 2022

bors bot deleted the ad-connectedness branch February 2, 2022 18:40

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(topology/connected): Connectedness of unions of sets #10005

[Merged by Bors] - feat(topology/connected): Connectedness of unions of sets #10005

AntoineChambert-Loir commented Oct 27, 2021 •

edited by fpvandoorn

Loading

eric-wieser Oct 27, 2021

eric-wieser Oct 27, 2021

urkud Oct 27, 2021

YaelDillies Oct 27, 2021

AntoineChambert-Loir Oct 27, 2021

AntoineChambert-Loir Oct 28, 2021

YaelDillies Oct 28, 2021

AntoineChambert-Loir Oct 28, 2021

jcommelin Oct 28, 2021

AntoineChambert-Loir Oct 28, 2021

AntoineChambert-Loir commented Oct 28, 2021

AntoineChambert-Loir commented Oct 28, 2021

eric-wieser left a comment

PatrickMassot commented Nov 5, 2021

fpvandoorn commented Jan 17, 2022

YaelDillies commented Jan 17, 2022

leanprover-community-bot-assistant commented Jan 28, 2022

jcommelin left a comment

YaelDillies Feb 2, 2022

YaelDillies Feb 2, 2022

fpvandoorn Feb 3, 2022

YaelDillies Feb 3, 2022

fpvandoorn Feb 3, 2022 •

edited

Loading

bors bot commented Feb 2, 2022

	λ n:ℕ, Union (set restrict s { j : ℕ \| j ≤ n}) -/
	λ n:ℕ, Union (subtype.restrict s (≤ n)) -/

	/-- The Union of connected sets indexed by a type with an archimedian successor (like `ℕ` or `ℤ`)
	/-- The Union of connected sets indexed by a type with an archimedean successor (like `ℕ` or `ℤ`)

[Merged by Bors] - feat(topology/connected): Connectedness of unions of sets #10005

[Merged by Bors] - feat(topology/connected): Connectedness of unions of sets #10005

Conversation

AntoineChambert-Loir commented Oct 27, 2021 • edited by fpvandoorn Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

AntoineChambert-Loir commented Oct 28, 2021

AntoineChambert-Loir commented Oct 28, 2021

eric-wieser left a comment

Choose a reason for hiding this comment

PatrickMassot commented Nov 5, 2021

fpvandoorn commented Jan 17, 2022

YaelDillies commented Jan 17, 2022

leanprover-community-bot-assistant commented Jan 28, 2022

jcommelin left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

fpvandoorn Feb 3, 2022 • edited Loading

Choose a reason for hiding this comment

bors bot commented Feb 2, 2022

AntoineChambert-Loir commented Oct 27, 2021 •

edited by fpvandoorn

Loading

fpvandoorn Feb 3, 2022 •

edited

Loading