Commit 2024-09-28 16:01 96fdd12a

View on Github →

feat(Alternating/Topology): add ClosedEmbedding (#17200) Add ContinuousAlternatingMap.isClosed_range_toContinuousMultilinearMap and ContinuousAlternatingMap.closedEmbedding_toContinuousMultilinearMap

Estimated changes

Modified Mathlib/Topology/Algebra/Module/Alternating/Topology.lean

added theorem ContinuousAlternatingMap.closedEmbedding_toContinuousMultilinearMap

added theorem ContinuousAlternatingMap.isClosed_range_toContinuousMultilinearMap