Skip to content

Commit 2a8a77c

Browse files
remove use of deprecated lemma
1 parent cc563a4 commit 2a8a77c

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Mathlib/Topology/ContinuousMap/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -401,7 +401,7 @@ be lifted into a continuous map from `s` to `t`. -/
401401
def mapsTo (f : α → β) (s : Set α) (t : Set β) (h : MapsTo f s t) (hf : ContinuousOn f s) :
402402
C(s, t) where
403403
toFun := MapsTo.restrict f s t h
404-
continuous_toFun := ContinuousOn.restrict_mapsTo hf _
404+
continuous_toFun := ContinuousOn.mapsToRestrict hf _
405405

406406
end Restrict
407407

0 commit comments

Comments
 (0)