Mathlib v3 is deprecated. Go to Mathlib v4

Theorem separated_by_open_embedding

Modification history

2020-11-27 15:35

src/topology/separation.lean

feat(topology/separation): Adds t2_space instances for disjoint unions (sums and sigma types). (#5113)

Added separated_by_open_embedding View on Github →