Theorem AffineSubspace.isClosed_direction_iff

Modification history

2025-09-15 12:07

Mathlib/Analysis/Normed/Affine/AddTorsor.lean

chore: generalize `AffineSubspace.isClosed_direction_iff` to `IsTopologicalAddTorsor` (#29619)

Modified AffineSubspace.isClosed_direction_iff View on Github →

2023-04-17 15:15

Mathlib/Analysis/NormedSpace/AddTorsor.lean

feat: port Analysis.NormedSpace.AddTorsor (#3477)

Added AffineSubspace.isClosed_direction_iff View on Github →