Commit 2023-02-04 08:44 3af293c6

View on Github →

feat: port Topology.UniformSpace.UniformEmbedding (#2038)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Separation.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

added theorem comp3_mem_uniformity

modified theorem comp_le_uniformity3

added theorem uniformContinuous_inl

added theorem uniformContinuous_inr

Created Mathlib/Topology/UniformSpace/UniformEmbedding.lean

added def Embedding.comapUniformSpace

added theorem Embedding.to_uniformEmbedding

added theorem Equiv.uniformEmbedding

added theorem IsClosed.completeSpace_coe

added theorem IsComplete.completeSpace_coe

added theorem UniformEmbedding.comp

added theorem UniformEmbedding.denseEmbedding

added theorem UniformEmbedding.embedding

added theorem UniformEmbedding.prod

added structure UniformEmbedding

added theorem UniformInducing.basis_uniformity

added theorem UniformInducing.cauchy_map_iff

added theorem UniformInducing.comp

added theorem UniformInducing.denseInducing

added theorem UniformInducing.inducing

added theorem UniformInducing.isComplete_range

added theorem UniformInducing.mk'

added theorem UniformInducing.prod

added theorem UniformInducing.uniformContinuous

added theorem UniformInducing.uniformContinuous_iff

added structure UniformInducing

added theorem closedEmbedding_of_spaced_out

added theorem closure_image_mem_nhds_of_uniformInducing

added theorem comap_uniformity_of_spaced_out

added theorem completeSpace_coe_iff_isComplete

added theorem completeSpace_congr

added theorem completeSpace_extension

added theorem completeSpace_iff_isComplete_range

added theorem isComplete_image_iff

added theorem isComplete_of_complete_image

added theorem totallyBounded_preimage

added theorem uniformContinuous_uniformly_extend

added theorem uniformEmbedding_comap

added theorem uniformEmbedding_def'

added theorem uniformEmbedding_def

added theorem uniformEmbedding_inl

added theorem uniformEmbedding_inr

added theorem uniformEmbedding_of_spaced_out

added theorem uniformEmbedding_set_inclusion

added theorem uniformEmbedding_subtypeEmb

added theorem uniformEmbedding_subtype_val

added theorem uniformInducing_id

added theorem uniformInducing_of_compose

added theorem uniform_extend_subtype

added theorem uniformly_extend_exists

added theorem uniformly_extend_of_ind

added theorem uniformly_extend_spec

added theorem uniformly_extend_unique