Commit 2025-06-07 14:03 dcd738d0

View on Github →

feat: tychonoff space ↔ embedded on Stone-Čech compactification (#24909) The main lemma is t35Space_iff_isEmbedding_stoneCechUnit. This property is stated in Wikipedia.

Estimated changes

Modified Mathlib/Topology/Separation/CompletelyRegular.lean

added theorem completelyRegularSpace_iff_isInducing_stoneCechUnit

added theorem isDenseEmbedding_stoneCechUnit

added theorem isDenseInducing_stoneCechUnit

added theorem isEmbedding_stoneCechUnit

added theorem isInducing_stoneCechUnit

added theorem t35Space_iff_isEmbedding_stoneCechUnit

Modified Mathlib/Topology/StoneCech.lean

modified theorem preStoneCechExtend_extends

added theorem preStoneCechExtend_preStoneCechUnit

modified theorem stoneCechExtend_extends

added theorem stoneCechExtend_stoneCechUnit

modified theorem ultrafilter_extend_extends

added theorem ultrafilter_extend_pure