Theorem TopologicalSpace.IrreducibleCloseds.coe_map

Modification history

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