mathlib

f7e477fd - feat(topology/separation): define `T₅` spaces (#16533)

feat(topology/separation): define `T₅` spaces (#16533) I'm going to prove that any `order_topology` is a `t5_space` in a follow-up PR. This will imply that any set in an `order_topology` is a normal space.