Commit 2023-01-31 22:16 cdca9995

View on Github →

feat: port Topology.Inseparable (#1908)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Inseparable.lean

added theorem Continuous.specialization_monotone

added theorem Filter.HasBasis.specializes_iff

added theorem Inducing.inseparable_iff

added theorem Inducing.specializes_iff

added theorem Inseparable.map

added theorem Inseparable.map_of_continuousAt

added theorem Inseparable.mem_closed_iff

added theorem Inseparable.mem_open_iff

added theorem Inseparable.nhds_eq

added theorem Inseparable.of_eq

added theorem Inseparable.prod

added theorem Inseparable.refl

added theorem Inseparable.rfl

added theorem Inseparable.specializes'

added theorem Inseparable.specializes

added def Inseparable

added theorem IsClosed.not_inseparable

added theorem IsClosed.not_specializes

added theorem IsOpen.not_inseparable

added theorem IsOpen.not_specializes

added theorem SeparationQuotient.comap_mk_nhdsSet

added theorem SeparationQuotient.comap_mk_nhdsSet_image

added theorem SeparationQuotient.comap_mk_nhds_mk

added theorem SeparationQuotient.continuousAt_lift

added theorem SeparationQuotient.continuousAt_lift₂

added theorem SeparationQuotient.continuousOn_lift

added theorem SeparationQuotient.continuousOn_lift₂

added theorem SeparationQuotient.continuousWithinAt_lift

added theorem SeparationQuotient.continuousWithinAt_lift₂

added theorem SeparationQuotient.continuous_lift

added theorem SeparationQuotient.continuous_lift₂

added theorem SeparationQuotient.continuous_mk

added theorem SeparationQuotient.image_mk_closure

added theorem SeparationQuotient.inducing_mk

added theorem SeparationQuotient.isClosedMap_mk

added theorem SeparationQuotient.isOpenMap_mk

added def SeparationQuotient.lift

added theorem SeparationQuotient.lift_comp_mk

added theorem SeparationQuotient.lift_mk

added def SeparationQuotient.lift₂

added theorem SeparationQuotient.lift₂_mk

added theorem SeparationQuotient.map_mk_nhds

added theorem SeparationQuotient.map_mk_nhdsSet

added theorem SeparationQuotient.map_mk_nhdsWithin_preimage

added theorem SeparationQuotient.map_prod_map_mk_nhds

added def SeparationQuotient.mk

added theorem SeparationQuotient.mk_eq_mk

added theorem SeparationQuotient.preimage_image_mk_closed

added theorem SeparationQuotient.preimage_image_mk_open

added theorem SeparationQuotient.preimage_mk_closure

added theorem SeparationQuotient.preimage_mk_frontier

added theorem SeparationQuotient.preimage_mk_interior

added theorem SeparationQuotient.quotientMap_mk

added theorem SeparationQuotient.range_mk

added theorem SeparationQuotient.surjective_mk

added theorem SeparationQuotient.tendsto_lift_nhdsWithin_mk

added theorem SeparationQuotient.tendsto_lift_nhds_mk

added theorem SeparationQuotient.tendsto_lift₂_nhds

added theorem SeparationQuotient.tendsto_lift₂_nhdsWithin

added def SeparationQuotient

added theorem Specializes.antisymm

added theorem Specializes.map

added theorem Specializes.map_of_continuousAt

added theorem Specializes.mem_closed

added theorem Specializes.mem_open

added theorem Specializes.prod

added theorem Specializes.trans

added def Specializes

added def inseparableSetoid

added theorem inseparable_def

added theorem inseparable_iff_closure_eq

added theorem inseparable_iff_forall_closed

added theorem inseparable_iff_forall_open

added theorem inseparable_iff_mem_closure

added theorem inseparable_iff_specializes_and

added theorem inseparable_of_nhdsWithin_eq

added theorem inseparable_pi

added theorem inseparable_prod

added theorem not_inseparable_iff_exists_open

added theorem not_specializes_iff_exists_closed

added theorem not_specializes_iff_exists_open

added def specializationPreorder

added theorem specializes_TFAE

added theorem specializes_iff_closure_subset

added theorem specializes_iff_forall_closed

added theorem specializes_iff_forall_open

added theorem specializes_iff_mem_closure

added theorem specializes_iff_nhds

added theorem specializes_iff_pure

added theorem specializes_of_eq

added theorem specializes_of_nhdsWithin

added theorem specializes_pi

added theorem specializes_prod

added theorem specializes_refl

added theorem specializes_rfl

added theorem subtype_inseparable_iff

added theorem subtype_specializes_iff