Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-27 21:32 fef4fb83

View on Github →

refactor(topology/inseparable): redefine specializes and inseparable (#14647)

  • Redefine specializes and inseparable in terms of nhds.
  • Review API.
  • Define inseparable_setoid and separation_quotient.
  • Add function.surjective.subsingleton.

Estimated changes

modified theorem inseparable.map
added theorem inseparable.nhds_eq
added theorem inseparable.refl
added theorem inseparable.rfl
added theorem inseparable.symm
added theorem inseparable.trans
modified def inseparable
added theorem inseparable_def
deleted theorem inseparable_iff_closed
deleted theorem inseparable_iff_closure
deleted theorem inseparable_iff_nhds_eq
added theorem specializes.antisymm
modified theorem specializes.map
added theorem specializes.mem_closed
added theorem specializes.mem_open
modified theorem specializes.trans
modified def specializes
deleted theorem specializes_def
modified theorem specializes_iff_forall_open
added theorem specializes_iff_nhds
added theorem specializes_iff_pure
modified theorem specializes_refl
modified theorem specializes_rfl
added theorem specializes_tfae
modified theorem subtype_inseparable_iff
deleted theorem specializes_antisymm