Theorem TopologicalSpace.IrreducibleCloseds.map_strictMono_of_isInducing

Modification history

2025-11-03 14:11
Mathlib/Topology/Sets/Closeds.lean
feat(Topology/KrullDimension): add subspace dimension inequality (#29728) …
Added TopologicalSpace.IrreducibleCloseds.map_strictMono_of_isInducingView on Github →