[Merged by Bors] - chore: tidy various files #7009
Conversation
Ruben-VandeVelde
commented
Sep 7, 2023
Ruben-VandeVelde
commented
Ruben-VandeVelde
added
awaiting-review
| @@ -456,12 +455,31 @@ def toLocalHomeomorph (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c) | |||
| continuous_invFun := hf.inverse_continuousOn hc | |||
| #align approximates_linear_on.to_local_homeomorph ApproximatesLinearOn.toLocalHomeomorph | |||
|
|
|||
| @[simp] | |||
There was a problem hiding this comment.
just to make sure all is good - they were moved up because of toHomeomorph, and otherwise unchanged, right?
There was a problem hiding this comment.
Yes, exactly
| exact | ||
| hf.approximates_deriv_on_nhds <| | ||
| f'.subsingleton_or_nnnorm_symm_pos.imp id fun hf' => half_pos <| inv_pos.2 hf' | ||
| · exact fun s t => ApproximatesLinearOn.mono_set |
There was a problem hiding this comment.
If we're tidying this, I'd rather inline it into the refine' and also turn it into a refine + use \mapsto
There was a problem hiding this comment.
That works. (I'm not touching => vs \mapsto.)
| @@ -175,9 +175,6 @@ section VolumeForm | |||
|
|
|||
| variable [_i : Fact (finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)) | |||
|
|
|||
| -- Porting note: added instance | |||
| instance : IsEmpty (Fin Nat.zero) := by simp only [Nat.zero_eq]; infer_instance | |||
There was a problem hiding this comment.
for other reviewers - this was moved to Logic/IsEmpty.lean
|
✌️ Ruben-VandeVelde can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
|
bors r+ |
|
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. |
bors
bot
changed the title
