Theorem Filter.Tendsto.pathExtend

Modification history

2025-05-06 13:07
Mathlib/Topology/Path.lean
refactor(Path): turn `Path.extend` into a `ContinuousMap` (#24066) …
Added Filter.Tendsto.pathExtendView on Github →