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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat: sync Data.Set.Intervals.OrdConnected #3077

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - feat: sync Data.Set.Intervals.OrdConnected #3077

wants to merge 2 commits into from

Conversation

joneugster
Copy link
Collaborator

This matches the way it is in mathlib3, but is it correct that the new statement is Set.IsAntichain.ordConnected instead of IsAntichain.ordConnected?

Open in Gitpod

@joneugster joneugster added awaiting-review mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged labels Mar 24, 2023
@eric-wieser
Copy link
Member

eric-wieser commented Mar 24, 2023 •
edited
Loading

This matches the way it is in mathlib3, but is it correct that the new statement is Set.IsAntichain.ordConnected instead of IsAntichain.ordConnected?

no, mathport doesn't know about _root_.

@YaelDillies
Copy link
Collaborator

Uh oh. Let me fix that quick.

@YaelDillies
Copy link
Collaborator

maintainer merge

@semorrison
Copy link
Contributor

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Mar 26, 2023
bors bot pushed a commit that referenced this pull request Mar 27, 2023
@joneugster @YaelDillies
feat: sync Data.Set.Intervals.OrdConnected (#3077)
6e9bc1c 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@bors
Copy link

bors bot commented Mar 27, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: sync Data.Set.Intervals.OrdConnected [Merged by Bors] - feat: sync Data.Set.Intervals.OrdConnected Mar 27, 2023
@bors bors bot closed this Mar 27, 2023
@bors bors bot deleted the sync_data.set.intervals.ord_connected branch March 27, 2023 01:41
@eric-wieser eric-wieser mentioned this pull request Mar 27, 2023
Closed
bors bot pushed a commit that referenced this pull request Mar 27, 2023
@Parcly-Taxel
chore: forward-port leanprover-community/mathlib#18636 (#3125)
5121293 
The change to `Mathlib/Data/Set/Intervals/OrdConnected.lean` was already forward-ported in #3077.

Also fixes a remaining `simple_graph` in the comments of one of the files.



Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
@YaelDillies YaelDillies mentioned this pull request Mar 27, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@YaelDillies YaelDillies YaelDillies left review comments

Assignees

@YaelDillies YaelDillies

Labels
mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@joneugster @eric-wieser @YaelDillies @semorrison