Commit 2023-10-31 02:45 23717cb8

View on Github →

feat(Topology/CompletelyRegular): Add definition CompletelyRegularSpace (#7926) Add definitions CompletelyRegularSpace and T35Space.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.disjoint_of_map

Created Mathlib/Topology/CompletelyRegular.lean

Modified Mathlib/Topology/NhdsSet.lean

added theorem Continuous.tendsto_nhdsSet_nhds