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
[Merged by Bors] - move(Topology/Order): Move anything that doesn't concern algebra #11610
Conversation
Move files from `Topology.Algebra.Order` to `Topology.Order` when they do not contain any algebra. Also move `Topology.LocalExtr` to `Topology.Order.LocalExtr`.
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
maintainer merge
🚀 Pull request has been placed on the maintainer queue by eric-wieser. |
bors merge |
👎 Rejected by label |
bors delegate+ |
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
) Move files from `Topology.Algebra.Order` to `Topology.Order` when they do not contain any algebra. Also move `Topology.LocalExtr` to `Topology.Order.LocalExtr`. According to git, the moves are: * `Mathlib/Topology/{Algebra => }/Order/ExtendFrom.lean` * `Mathlib/Topology/{Algebra => }/Order/ExtrClosure.lean` * `Mathlib/Topology/{Algebra => }/Order/Filter.lean` * `Mathlib/Topology/{Algebra => }/Order/IntermediateValue.lean` * `Mathlib/Topology/{Algebra => }/Order/LeftRight.lean` * `Mathlib/Topology/{Algebra => }/Order/LeftRightLim.lean` * `Mathlib/Topology/{Algebra => }/Order/MonotoneContinuity.lean` * `Mathlib/Topology/{Algebra => }/Order/MonotoneConvergence.lean` * `Mathlib/Topology/{Algebra => }/Order/ProjIcc.lean` * `Mathlib/Topology/{Algebra => }/Order/T5.lean` * `Mathlib/Topology/{ => Order}/LocalExtr.lean`
Pull request successfully merged into master. Build succeeded: |
) Move files from `Topology.Algebra.Order` to `Topology.Order` when they do not contain any algebra. Also move `Topology.LocalExtr` to `Topology.Order.LocalExtr`. According to git, the moves are: * `Mathlib/Topology/{Algebra => }/Order/ExtendFrom.lean` * `Mathlib/Topology/{Algebra => }/Order/ExtrClosure.lean` * `Mathlib/Topology/{Algebra => }/Order/Filter.lean` * `Mathlib/Topology/{Algebra => }/Order/IntermediateValue.lean` * `Mathlib/Topology/{Algebra => }/Order/LeftRight.lean` * `Mathlib/Topology/{Algebra => }/Order/LeftRightLim.lean` * `Mathlib/Topology/{Algebra => }/Order/MonotoneContinuity.lean` * `Mathlib/Topology/{Algebra => }/Order/MonotoneConvergence.lean` * `Mathlib/Topology/{Algebra => }/Order/ProjIcc.lean` * `Mathlib/Topology/{Algebra => }/Order/T5.lean` * `Mathlib/Topology/{ => Order}/LocalExtr.lean`
) Move files from `Topology.Algebra.Order` to `Topology.Order` when they do not contain any algebra. Also move `Topology.LocalExtr` to `Topology.Order.LocalExtr`. According to git, the moves are: * `Mathlib/Topology/{Algebra => }/Order/ExtendFrom.lean` * `Mathlib/Topology/{Algebra => }/Order/ExtrClosure.lean` * `Mathlib/Topology/{Algebra => }/Order/Filter.lean` * `Mathlib/Topology/{Algebra => }/Order/IntermediateValue.lean` * `Mathlib/Topology/{Algebra => }/Order/LeftRight.lean` * `Mathlib/Topology/{Algebra => }/Order/LeftRightLim.lean` * `Mathlib/Topology/{Algebra => }/Order/MonotoneContinuity.lean` * `Mathlib/Topology/{Algebra => }/Order/MonotoneConvergence.lean` * `Mathlib/Topology/{Algebra => }/Order/ProjIcc.lean` * `Mathlib/Topology/{Algebra => }/Order/T5.lean` * `Mathlib/Topology/{ => Order}/LocalExtr.lean`
) Move files from `Topology.Algebra.Order` to `Topology.Order` when they do not contain any algebra. Also move `Topology.LocalExtr` to `Topology.Order.LocalExtr`. According to git, the moves are: * `Mathlib/Topology/{Algebra => }/Order/ExtendFrom.lean` * `Mathlib/Topology/{Algebra => }/Order/ExtrClosure.lean` * `Mathlib/Topology/{Algebra => }/Order/Filter.lean` * `Mathlib/Topology/{Algebra => }/Order/IntermediateValue.lean` * `Mathlib/Topology/{Algebra => }/Order/LeftRight.lean` * `Mathlib/Topology/{Algebra => }/Order/LeftRightLim.lean` * `Mathlib/Topology/{Algebra => }/Order/MonotoneContinuity.lean` * `Mathlib/Topology/{Algebra => }/Order/MonotoneConvergence.lean` * `Mathlib/Topology/{Algebra => }/Order/ProjIcc.lean` * `Mathlib/Topology/{Algebra => }/Order/T5.lean` * `Mathlib/Topology/{ => Order}/LocalExtr.lean`
) Move files from `Topology.Algebra.Order` to `Topology.Order` when they do not contain any algebra. Also move `Topology.LocalExtr` to `Topology.Order.LocalExtr`. According to git, the moves are: * `Mathlib/Topology/{Algebra => }/Order/ExtendFrom.lean` * `Mathlib/Topology/{Algebra => }/Order/ExtrClosure.lean` * `Mathlib/Topology/{Algebra => }/Order/Filter.lean` * `Mathlib/Topology/{Algebra => }/Order/IntermediateValue.lean` * `Mathlib/Topology/{Algebra => }/Order/LeftRight.lean` * `Mathlib/Topology/{Algebra => }/Order/LeftRightLim.lean` * `Mathlib/Topology/{Algebra => }/Order/MonotoneContinuity.lean` * `Mathlib/Topology/{Algebra => }/Order/MonotoneConvergence.lean` * `Mathlib/Topology/{Algebra => }/Order/ProjIcc.lean` * `Mathlib/Topology/{Algebra => }/Order/T5.lean` * `Mathlib/Topology/{ => Order}/LocalExtr.lean`
) Move files from `Topology.Algebra.Order` to `Topology.Order` when they do not contain any algebra. Also move `Topology.LocalExtr` to `Topology.Order.LocalExtr`. According to git, the moves are: * `Mathlib/Topology/{Algebra => }/Order/ExtendFrom.lean` * `Mathlib/Topology/{Algebra => }/Order/ExtrClosure.lean` * `Mathlib/Topology/{Algebra => }/Order/Filter.lean` * `Mathlib/Topology/{Algebra => }/Order/IntermediateValue.lean` * `Mathlib/Topology/{Algebra => }/Order/LeftRight.lean` * `Mathlib/Topology/{Algebra => }/Order/LeftRightLim.lean` * `Mathlib/Topology/{Algebra => }/Order/MonotoneContinuity.lean` * `Mathlib/Topology/{Algebra => }/Order/MonotoneConvergence.lean` * `Mathlib/Topology/{Algebra => }/Order/ProjIcc.lean` * `Mathlib/Topology/{Algebra => }/Order/T5.lean` * `Mathlib/Topology/{ => Order}/LocalExtr.lean`
Move files from
Topology.Algebra.Order
toTopology.Order
when they do not contain any algebra. Also moveTopology.LocalExtr
toTopology.Order.LocalExtr
.According to git, the moves are:
Mathlib/Topology/{Algebra => }/Order/ExtendFrom.lean
Mathlib/Topology/{Algebra => }/Order/ExtrClosure.lean
Mathlib/Topology/{Algebra => }/Order/Filter.lean
Mathlib/Topology/{Algebra => }/Order/IntermediateValue.lean
Mathlib/Topology/{Algebra => }/Order/LeftRight.lean
Mathlib/Topology/{Algebra => }/Order/LeftRightLim.lean
Mathlib/Topology/{Algebra => }/Order/MonotoneContinuity.lean
Mathlib/Topology/{Algebra => }/Order/MonotoneConvergence.lean
Mathlib/Topology/{Algebra => }/Order/ProjIcc.lean
Mathlib/Topology/{Algebra => }/Order/T5.lean
Mathlib/Topology/{ => Order}/LocalExtr.lean
This is a rehash of leanprover-community/mathlib#17859.