Skip to content

Commit 2de4015

Browse files
committed
fix error
1 parent 7717f2a commit 2de4015

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/Geometry/Manifold/VectorBundle/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -498,7 +498,7 @@ theorem contMDiffOn (e : Trivialization F (π F E)) [MemTrivializationAtlas e] :
498498

499499
theorem contMDiffOn_symm (e : Trivialization F (π F E)) [MemTrivializationAtlas e] :
500500
ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n e.toOpenPartialHomeomorph.symm e.target := by
501-
rw [e.contMDiffOn_iff e.toOpenPartialHomeomorph.symm_mapsTo]
501+
rw [e.contMDiffOn_iff e.toOpenPartialHomeomorph.mapsTo_symm]
502502
refine ⟨contMDiffOn_fst.congr fun x hx ↦ e.proj_symm_apply hx,
503503
contMDiffOn_snd.congr fun x hx ↦ ?_⟩
504504
rw [e.apply_symm_apply hx]

0 commit comments

Comments
 (0)