Skip to content

[Merged by Bors] - feat: port Order.Heyting.Basic#793

Closed
kim-em wants to merge 14 commits intomasterfrom
Heyting
Closed

[Merged by Bors] - feat: port Order.Heyting.Basic#793
kim-em wants to merge 14 commits intomasterfrom
Heyting

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Nov 30, 2022 •
edited by ChrisHughes24
Loading

mathlib3 sha 4e42a9d0a79d151ee359c270e498b1a00cc6fa4e

@kim-em kim-em changed the title Heyting feat: port Order.Heyting.Basic Nov 30, 2022
@kim-em kim-em added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) awaiting-review labels Nov 30, 2022
@kim-em kim-em mentioned this pull request Nov 30, 2022
Closed
1 task
@kim-em kim-em added mathlib-port This is a port of a theory file from mathlib. and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Nov 30, 2022
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Nov 30, 2022

This PR/issue depends on:

Ruben-VandeVelde
Ruben-VandeVelde reviewed Nov 30, 2022
View reviewed changes
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Dec 1, 2022

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Dec 1, 2022
bors bot pushed a commit that referenced this pull request Dec 1, 2022
@kim-em @Ruben-VandeVelde @ChrisHughes24
feat: port Order.Heyting.Basic (#793)
7ee8c7b 
mathlib3 sha 4e42a9d0a79d151ee359c270e498b1a00cc6fa4e 


- [x] depends on: #792 
- [x] depends on: #800

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Dec 1, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Order.Heyting.Basic [Merged by Bors] - feat: port Order.Heyting.Basic Dec 1, 2022
@bors bors bot closed this Dec 1, 2022
@bors bors bot deleted the Heyting branch December 1, 2022 23:22
@github-actions github-actions bot mentioned this pull request Dec 2, 2022
Closed
bors bot pushed a commit that referenced this pull request Dec 2, 2022
@kim-em @Ruben-VandeVelde @ChrisHughes24
feat: port Order.BooleanAlgebra (#794)
608fd2f 
mathlib3 sha 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

- [x] depends on: #793 

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Dec 2, 2022
chore(*): add mathlib4 synchronization comments (#17790)
02ca4ad 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.order.sub.canonical`: leanprover-community/mathlib4#814
* `category_theory.category.Rel`: leanprover-community/mathlib4#822
* `category_theory.category.basic`: leanprover-community/mathlib4#749
* `category_theory.functor.basic`: leanprover-community/mathlib4#749
* `category_theory.functor.category`: leanprover-community/mathlib4#749
* `category_theory.functor.functorial`: leanprover-community/mathlib4#822
* `category_theory.isomorphism`: leanprover-community/mathlib4#749
* `category_theory.natural_transformation`: leanprover-community/mathlib4#749
* `category_theory.thin`: leanprover-community/mathlib4#822
* `combinatorics.quiver.basic`: leanprover-community/mathlib4#749
* `combinatorics.quiver.path`: leanprover-community/mathlib4#811
* `data.psigma.order`: leanprover-community/mathlib4#815
* `data.stream.defs`: leanprover-community/mathlib4#665
* `order.boolean_algebra`: leanprover-community/mathlib4#794
* `order.heyting.basic`: leanprover-community/mathlib4#793
* `order.rel_iso.group`: leanprover-community/mathlib4#813
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Dec 3, 2022
chore(*): add mathlib4 synchronization comments (#17790)
308f6d0 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.order.sub.canonical`: leanprover-community/mathlib4#814
* `category_theory.category.Rel`: leanprover-community/mathlib4#822
* `category_theory.category.basic`: leanprover-community/mathlib4#749
* `category_theory.functor.basic`: leanprover-community/mathlib4#749
* `category_theory.functor.category`: leanprover-community/mathlib4#749
* `category_theory.functor.functorial`: leanprover-community/mathlib4#822
* `category_theory.isomorphism`: leanprover-community/mathlib4#749
* `category_theory.natural_transformation`: leanprover-community/mathlib4#749
* `category_theory.thin`: leanprover-community/mathlib4#822
* `combinatorics.quiver.basic`: leanprover-community/mathlib4#749
* `combinatorics.quiver.path`: leanprover-community/mathlib4#811
* `data.psigma.order`: leanprover-community/mathlib4#815
* `data.stream.defs`: leanprover-community/mathlib4#665
* `order.boolean_algebra`: leanprover-community/mathlib4#794
* `order.heyting.basic`: leanprover-community/mathlib4#793
* `order.rel_iso.group`: leanprover-community/mathlib4#813
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@hrmacbeth hrmacbeth hrmacbeth left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments

+1 more reviewer

@ChrisHughes24 ChrisHughes24 ChrisHughes24 left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

mathlib-port This is a port of a theory file from mathlib. 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.

4 participants

@kim-em @hrmacbeth @ChrisHughes24 @Ruben-VandeVelde