Commit 2023-02-12 22:01 54e0758a

View on Github →

feat: port Topology.UniformSpace.AbstractCompletion (#2238)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/UniformSpace/AbstractCompletion.lean

added theorem AbstractCompletion.closure_range

added def AbstractCompletion.compare

added def AbstractCompletion.compareEquiv

added theorem AbstractCompletion.compare_coe

added theorem AbstractCompletion.continuous_coe

added theorem AbstractCompletion.continuous_extend

added theorem AbstractCompletion.continuous_map

added theorem AbstractCompletion.continuous_map₂

added theorem AbstractCompletion.denseInducing

added theorem AbstractCompletion.extend_coe

added theorem AbstractCompletion.extend_comp_coe

added theorem AbstractCompletion.extend_def

added theorem AbstractCompletion.extend_map

added theorem AbstractCompletion.extend_unique

added theorem AbstractCompletion.extension₂_coe_coe

added theorem AbstractCompletion.induction_on

added theorem AbstractCompletion.inverse_compare

added theorem AbstractCompletion.map_coe

added theorem AbstractCompletion.map_comp

added theorem AbstractCompletion.map_id

added theorem AbstractCompletion.map_unique

added theorem AbstractCompletion.map₂_coe_coe

added def AbstractCompletion.ofComplete

added theorem AbstractCompletion.uniformContinuous_coe

added theorem AbstractCompletion.uniformContinuous_compare

added theorem AbstractCompletion.uniformContinuous_compareEquiv

added theorem AbstractCompletion.uniformContinuous_compareEquiv_symm

added theorem AbstractCompletion.uniformContinuous_extend

added theorem AbstractCompletion.uniformContinuous_extension₂

added theorem AbstractCompletion.uniformContinuous_map

added theorem AbstractCompletion.uniformContinuous_map₂

added structure AbstractCompletion