Theorem t1Space_of_t0Space_of_r0Space

Modification history

2025-07-03 14:43
Mathlib/Topology/Separation/Basic.lean
chore: register the fact that a topological space that is `T₀` and `R₀` is `T₁` as a typeclass instance (#26550) …
Deleted t1Space_of_t0Space_of_r0SpaceView on Github →
2025-06-23 08:19
Mathlib/Topology/Separation/Basic.lean
feat: T₁ iff T₀ and R₀ (#26064)
Added t1Space_of_t0Space_of_r0SpaceView on Github →