Theorem Topology.IsInducing.completelyRegularSpace

Modification history

2025-05-14 15:37
Mathlib/Topology/Separation/CompletelyRegular.lean
feat: subspace of tychonoff space is tychonoff (#24815)
Added Topology.IsInducing.completelyRegularSpaceView on Github →