Commit 2023-02-18 18:53 9f20a012

View on Github →

feat: port Topology.UniformSpace.Completion (#2269)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/UniformSpace/Completion.lean

added theorem CauchyFilter.cauchyCat_eq

added theorem CauchyFilter.denseEmbedding_pureCauchy

added theorem CauchyFilter.denseInducing_pureCauchy

added theorem CauchyFilter.denseRange_pureCauchy

added def CauchyFilter.extend

added theorem CauchyFilter.extend_pureCauchy

added def CauchyFilter.gen

added theorem CauchyFilter.mem_uniformity'

added theorem CauchyFilter.mem_uniformity

added theorem CauchyFilter.monotone_gen

added theorem CauchyFilter.nonempty_cauchyCat_iff

added def CauchyFilter.pureCauchy

added theorem CauchyFilter.separated_pureCauchy_injective

added theorem CauchyFilter.uniformContinuous_extend

added theorem CauchyFilter.uniformEmbedding_pureCauchy

added theorem CauchyFilter.uniformInducing_pureCauchy

added def CauchyFilter

added def UniformSpace.Completion.UniformCompletion.completeEquivSelf

added def UniformSpace.Completion.cPkg

added theorem UniformSpace.Completion.coe_injective

added theorem UniformSpace.Completion.comap_coe_eq_uniformity

added def UniformSpace.Completion.completionSeparationQuotientEquiv

added theorem UniformSpace.Completion.continuous_coe

added theorem UniformSpace.Completion.continuous_extension

added theorem UniformSpace.Completion.continuous_map

added theorem UniformSpace.Completion.continuous_map₂

added theorem UniformSpace.Completion.denseEmbedding_coe

added theorem UniformSpace.Completion.denseInducing_coe

added theorem UniformSpace.Completion.denseRange_coe

added theorem UniformSpace.Completion.denseRange_coe₂

added theorem UniformSpace.Completion.denseRange_coe₃

added theorem UniformSpace.Completion.ext'

added theorem UniformSpace.Completion.ext

added theorem UniformSpace.Completion.extension_coe

added theorem UniformSpace.Completion.extension_comp_coe

added theorem UniformSpace.Completion.extension_map

added theorem UniformSpace.Completion.extension_unique

added theorem UniformSpace.Completion.extension₂_coe_coe

added theorem UniformSpace.Completion.induction_on

added theorem UniformSpace.Completion.induction_on₂

added theorem UniformSpace.Completion.induction_on₃

added theorem UniformSpace.Completion.map_coe

added theorem UniformSpace.Completion.map_comp

added theorem UniformSpace.Completion.map_id

added theorem UniformSpace.Completion.map_unique

added theorem UniformSpace.Completion.map₂_coe_coe

added theorem UniformSpace.Completion.nonempty_completion_iff

added theorem UniformSpace.Completion.uniformContinuous_coe

added theorem UniformSpace.Completion.uniformContinuous_completionSeparationQuotientEquiv

added theorem UniformSpace.Completion.uniformContinuous_completionSeparationQuotientEquiv_symm

added theorem UniformSpace.Completion.uniformContinuous_extension

added theorem UniformSpace.Completion.uniformContinuous_extension₂

added theorem UniformSpace.Completion.uniformContinuous_map

added theorem UniformSpace.Completion.uniformContinuous_map₂

added theorem UniformSpace.Completion.uniformEmbedding_coe

added theorem UniformSpace.Completion.uniformInducing_coe

added def UniformSpace.Completion