Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-06 15:08 d45a8ace

View on Github →

refactor(topology/separation): redefine t0_space (#15046)

Estimated changes

Modified src/algebraic_geometry/prime_spectrum/basic.lean

added def prime_spectrum.nhds_order_embedding

Modified src/topology/alexandroff.lean

added theorem alexandroff.inseparable_coe

added theorem alexandroff.inseparable_iff

added theorem alexandroff.not_inseparable_coe_infty

added theorem alexandroff.not_inseparable_infty_coe

added theorem alexandroff.not_specializes_infty_coe

added theorem alexandroff.specializes_coe

Modified src/topology/separation.lean

deleted theorem t0_space_def

added theorem t0_space_iff_exists_is_open_xor_mem

added theorem t1_space_iff_specializes_imp_eq

Modified src/topology/uniform_space/separation.lean