Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-04 13:17 50024528

View on Github →

refactor(topology): move code around (#14525) Create a new file topology/inseparable and more the definitions of specializes and inseparable to this file. This is a preparation to a larger refactor of these definitions.

Estimated changes

added theorem inseparable.map
added def inseparable
added theorem inseparable_iff_closed
added theorem specializes.map
added theorem specializes.trans
added def specializes
added theorem specializes_def
added theorem specializes_refl
added theorem specializes_rfl
deleted theorem inseparable.map
deleted def inseparable
deleted theorem inseparable_iff_closed
deleted theorem inseparable_iff_closure
deleted theorem inseparable_iff_nhds_eq
added theorem specializes.eq
added theorem specializes_antisymm
added theorem specializes_iff_eq
deleted theorem subtype_inseparable_iff
deleted theorem specializes.eq
deleted theorem specializes.map
deleted theorem specializes.trans
deleted def specializes
deleted theorem specializes_antisymm
deleted theorem specializes_def
deleted theorem specializes_iff_eq
deleted theorem specializes_refl
deleted theorem specializes_rfl