[Merged by Bors] - chore: tidy various files#4304
[Merged by Bors] - chore: tidy various files#4304Ruben-VandeVelde wants to merge 5 commits intomasterfrom
Conversation
Mathlib/Topology/PathConnected.lean
Outdated
| continuous_subtype_val <;> | ||
| -- TODO: the following are provable by `continuity` but it is too slow | ||
| -- porting note: the new `continuity` succeeds and it isn't too slow! | ||
| -- Porting note: used `continuity` |
There was a problem hiding this comment.
| -- Porting note: used `continuity` |
I think just drop this, it's confusing without the context, and doesn't really need to be recorded.
Mathlib/Topology/PathConnected.lean
Outdated
| @[continuity] | ||
| theorem truncate_const_continuous_family {X : Type _} [TopologicalSpace X] {a b : X} (γ : Path a b) | ||
| (t : ℝ) : Continuous ↿(γ.truncate t) := by | ||
| -- Porting note: used `continuity` |
|
bors d+ |
|
✌️ Ruben-VandeVelde can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
|
Canceled. |
|
This can be merged after it's fixed bors d+ |
|
✌️ Ruben-VandeVelde can now approve this pull request. To approve and merge a pull request, simply reply with |
|
I'll let #4360 go first in case it conflicts |
|
This PR/issue depends on:
|
|
bors merge |
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Uh oh!
There was an error while loading. Please reload this page.