Commit 2025-05-14 15:37 6f9d8400

View on Github →

feat: subspace of tychonoff space is tychonoff (#24815)

Estimated changes

Modified Mathlib/Topology/Separation/CompletelyRegular.lean

added theorem Topology.IsEmbedding.t35Space

added theorem Topology.IsInducing.completelyRegularSpace