Commit 2024-05-07 10:24 740f52cf

View on Github →

feat: add *.of_comp_iff lemmas for Inducing, Embedding, etc. (#12639)

Estimated changes

Modified Mathlib/Topology/FiberBundle/Constructions.lean

Modified Mathlib/Topology/LocalAtTarget.lean

Modified Mathlib/Topology/Maps.lean

added theorem ClosedEmbedding.of_comp_iff

added theorem Embedding.of_comp_iff

added theorem Inducing.of_comp_iff

Modified Mathlib/Topology/UniformSpace/UniformEmbedding.lean

added theorem UniformEmbedding.of_comp_iff

added theorem UniformInducing.of_comp_iff