Commit 2024-03-05 15:28 923d04ad

View on Github →

feat(Separation): add T25Space (Subtype p) (#11055) Add Filter.Tendsto.lift'_closure, R1Space.of_continuous_specializes_imp, and T25Space.of_injective_continuous.

Estimated changes

Modified Mathlib/Topology/Basic.lean

added theorem Filter.Tendsto.lift'_closure

added theorem tendsto_lift'_closure_nhds

Modified Mathlib/Topology/Separation.lean

modified theorem Inducing.r1Space

added theorem R1Space.of_continuous_specializes_imp

added theorem T25Space.of_injective_continuous