Theorem completelyRegularSpace_iff_isInducing_stoneCechUnit

Modification history

2025-06-07 14:03
Mathlib/Topology/Separation/CompletelyRegular.lean
feat: tychonoff space ↔ embedded on Stone-Čech compactification (#24909) …
Added completelyRegularSpace_iff_isInducing_stoneCechUnitView on Github →