Theorem TopologicalSpace.IrreducibleCloseds.map_mono

Modification history

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