Commit 2025-10-15 07:25 1a640d9b

View on Github →

feat(Homotopy/Path): add missing lemmas (#30552)

  • Add @[simps] to ContinuousMap.Homotopy.evalAt.
  • Add ContinuousMap.Homotopy.pathExtend_evalAt.
  • Reuse section variables.

Estimated changes