Commit 2025-09-15 09:41 1e49ea1b

View on Github →

feat: topological affine spaces (#28493) This PR adds a typeclass IsTopologicalAddTorsor for topological affine spaces and generalizes basic results which currently assume NormedAddTorsor.

Estimated changes

Modified Mathlib.lean

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

deleted theorem Continuous.vsub

deleted theorem ContinuousOn.vsub

deleted theorem Filter.Tendsto.vsub

deleted theorem IsClosed.vadd_right_of_isCompact

deleted theorem continuous_vsub

Created Mathlib/Topology/Algebra/Group/AddTorsor.lean

added theorem Continuous.vsub

added theorem ContinuousOn.vsub

added theorem Filter.Tendsto.vsub

added def Homeomorph.vaddConst

added theorem IsClosed.vadd_right_of_isCompact

added theorem IsTopologicalAddTorsor.to_isTopologicalAddGroup

Modified Mathlib/Topology/Algebra/Group/Pointwise.lean