Theorem Inducing.r1Space

Modification history

2024-10-29 14:36

Mathlib/Topology/Separation/Basic.lean

chore: Rename `Inducing` to `IsInducing` (#18330) …

Deleted Inducing.r1Space View on Github →

2024-03-05 15:28

Mathlib/Topology/Separation.lean

feat(Separation): add `T25Space (Subtype p)` (#11055) …

Modified Inducing.r1Space View on Github →

2024-01-29 18:36

Mathlib/Topology/Separation.lean

feat(Topology/Separation): define R₁ spaces, review API (#10085) …

Added Inducing.r1Space View on Github →