Commit 2024-07-18 08:27 3109eab8

View on Github →

feat(Topology): stoneCechUnit injective for T35Space (#12536) The mapstoneCechUnit is injective when the underlying space is a T35Space.

Estimated changes

Modified Mathlib/Topology/CompletelyRegular.lean

added theorem injective_stoneCechUnit_of_t35Space

added theorem separatesPoints_continuous_of_t35Space_Icc

Modified Mathlib/Topology/StoneCech.lean

added theorem eq_if_stoneCechUnit_eq