Commit 2025-09-16 18:56 d5352336

View on Github →

chore(Topology/Algebra/Affine): generalize Filter.Tendsto.{lineMap, midpoint} (#29621)

Estimated changes

Modified Mathlib/Analysis/Normed/Affine/AddTorsor.lean

Modified Mathlib/Analysis/Normed/Affine/Isometry.lean

Modified Mathlib/Analysis/Normed/Group/AddTorsor.lean

deleted theorem Filter.Tendsto.lineMap

deleted theorem Filter.Tendsto.midpoint

Modified Mathlib/Topology/Algebra/Affine.lean

added theorem Filter.Tendsto.lineMap

added theorem Filter.Tendsto.midpoint

Modified Mathlib/Topology/UrysohnsLemma.lean