Commit 2022-09-17 16:29 f7e477fd

View on Github →

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.

Estimated changes

Modified counterexamples/sorgenfrey_line.lean

Modified src/topology/maps.lean

added theorem inducing.nhds_set_eq_comap

Modified src/topology/nhds_set.lean

added theorem bUnion_mem_nhds_set

Modified src/topology/separation.lean

added theorem embedding.t5_space

added theorem separated_iff_disjoint