Commit 2023-03-02 16:17 28d1ea57

View on Github →

refactor: review API of UniformEmbedding (#2584) Forward-port leanprover-community/mathlib#18516

Estimated changes

Modified Mathlib/Logic/Equiv/Basic.lean

Modified Mathlib/Topology/Separation.lean

added theorem embedding_iff_inducing

Modified Mathlib/Topology/UniformSpace/Basic.lean

modified theorem Filter.HasBasis.uniformContinuousOn_iff

modified theorem Filter.HasBasis.uniformContinuous_iff

Modified Mathlib/Topology/UniformSpace/UniformEmbedding.lean

added theorem Filter.HasBasis.uniformEmbedding_iff'

added theorem Filter.HasBasis.uniformEmbedding_iff

deleted theorem UniformEmbedding.embedding

modified theorem UniformInducing.inducing

deleted theorem uniformEmbedding_def'

deleted theorem uniformEmbedding_def

added theorem uniformEmbedding_iff'

added theorem uniformEmbedding_iff_uniformInducing

added theorem uniformInducing_iff'