Commit 2023-04-10 15:17 28c8a705

View on Github →

feat: port Topology.LocalAtTarget (#2205)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/LocalAtTarget.lean

added theorem Set.restrictPreimage_closedEmbedding

added theorem Set.restrictPreimage_embedding

added theorem Set.restrictPreimage_inducing

added theorem Set.restrictPreimage_isClosedMap

added theorem Set.restrictPreimage_openEmbedding

added theorem closedEmbedding_iff_closedEmbedding_of_supᵢ_eq_top

added theorem embedding_iff_embedding_of_supᵢ_eq_top

added theorem inducing_iff_inducing_of_supᵢ_eq_top

added theorem isClosedMap_iff_isClosedMap_of_supᵢ_eq_top

added theorem isClosed_iff_coe_preimage_of_supᵢ_eq_top

added theorem isOpen_iff_coe_preimage_of_supᵢ_eq_top

added theorem isOpen_iff_inter_of_supᵢ_eq_top

added theorem openEmbedding_iff_openEmbedding_of_supᵢ_eq_top