Commit 2023-02-03 07:23 dc6aa6ba

View on Github →

feat: port Topology.UniformSpace.Separation (#2014)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/UniformSpace/Separation.lean

added theorem Filter.HasBasis.mem_separationRel

added def UniformSpace.SeparationQuotient.lift

added theorem UniformSpace.SeparationQuotient.lift_mk

added def UniformSpace.SeparationQuotient.map

added theorem UniformSpace.SeparationQuotient.map_comp

added theorem UniformSpace.SeparationQuotient.map_id

added theorem UniformSpace.SeparationQuotient.map_mk

added theorem UniformSpace.SeparationQuotient.map_unique

added theorem UniformSpace.SeparationQuotient.uniformContinuous_lift

added theorem UniformSpace.SeparationQuotient.uniformContinuous_map

added def UniformSpace.SeparationQuotient

added theorem UniformSpace.comap_quotient_eq_uniformity

added theorem UniformSpace.comap_quotient_le_uniformity

added theorem UniformSpace.eq_of_separated_of_uniformContinuous

added theorem UniformSpace.separated_of_uniformContinuous

added def UniformSpace.separationSetoid

added theorem UniformSpace.separation_prod

added theorem UniformSpace.uniformContinuous_quotient

added theorem UniformSpace.uniformContinuous_quotient_lift

added theorem UniformSpace.uniformContinuous_quotient_lift₂

added theorem UniformSpace.uniformContinuous_quotient_mk'

added theorem UniformSpace.uniformContinuous_quotient_mk

added theorem UniformSpace.uniformity_quotient

added theorem eq_of_clusterPt_uniformity

added theorem eq_of_forall_symmetric

added theorem eq_of_uniformity

added theorem eq_of_uniformity_basis

added theorem idRel_sub_separationRel

added theorem isClosed_of_spaced_out

added theorem isClosed_range_of_spaced_out

added theorem isClosed_separationRel

added theorem separatedSpace_iff

added theorem separated_def'

added theorem separated_def

added theorem separated_equiv

added theorem separated_iff_t2

added def separationRel

added theorem separationRel_comap

added theorem separationRel_eq_inter_closure

added theorem separationRel_iff_inseparable

added theorem separationRel_iff_specializes