Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-01 17:27 0950ba3d

View on Github →

refactor(topology/separation): rename indistinguishable to inseparable (#14401)

  • Replace indistinguishable by inseparable in the definition and lemma names. The word "indistinguishable" is too generic.
  • Rename t0_space_iff_distinguishable to t0_space_iff_not_inseparable because the name t0_space_iff_separable is misleading, slightly golf the proof.
  • Add t0_space_iff_nhds_injective, nhds_injective, reorder lemmas around these two.

Estimated changes

added theorem metric.inseparable_iff
deleted theorem indistinguishable.eq
deleted theorem indistinguishable.map
deleted def indistinguishable
added theorem inseparable.eq
added theorem inseparable.map
added def inseparable
added theorem inseparable_iff_closed
added theorem nhds_injective