Commit 2023-01-31 12:11 493d1014

View on Github →

feat: port Topology.Maps (#1873)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Maps.lean

added theorem ClosedEmbedding.closed_iff_image_closed

added theorem ClosedEmbedding.closed_iff_preimage_closed

added theorem ClosedEmbedding.closure_image_eq

added theorem ClosedEmbedding.comp

added theorem ClosedEmbedding.continuous

added theorem ClosedEmbedding.isClosedMap

added theorem ClosedEmbedding.tendsto_nhds_iff

added structure ClosedEmbedding

added theorem Embedding.closure_eq_preimage_closure_image

added theorem Embedding.continuous

added theorem Embedding.continuous_iff

added theorem Embedding.discreteTopology

added theorem Embedding.map_nhds_eq

added theorem Embedding.map_nhds_of_mem

added theorem Embedding.mk'

added theorem Embedding.tendsto_nhds_iff

added structure Embedding

added theorem Function.Injective.embedding_induced

added theorem Inducing.closure_eq_preimage_closure_image

added theorem Inducing.continuousAt_iff'

added theorem Inducing.continuousAt_iff

added theorem Inducing.continuous_iff

added theorem Inducing.dense_iff

added theorem Inducing.image_mem_nhdsWithin

added theorem Inducing.isClosedMap

added theorem Inducing.isClosed_iff'

added theorem Inducing.isClosed_iff

added theorem Inducing.isClosed_preimage

added theorem Inducing.isOpen_iff

added theorem Inducing.map_nhds_eq

added theorem Inducing.map_nhds_of_mem

added theorem Inducing.nhdsSet_eq_comap

added theorem Inducing.nhds_eq_comap

added theorem Inducing.tendsto_nhds_iff

added structure Inducing

added theorem IsClosedMap.closed_range

added theorem IsClosedMap.closure_image_subset

added theorem IsClosedMap.of_inverse

added theorem IsClosedMap.of_nonempty

added def IsClosedMap

added theorem IsOpenMap.image_interior_subset

added theorem IsOpenMap.image_mem_nhds

added theorem IsOpenMap.interior_preimage_subset_preimage_interior

added theorem IsOpenMap.isOpen_range

added theorem IsOpenMap.mapsTo_interior

added theorem IsOpenMap.nhds_le

added theorem IsOpenMap.of_inverse

added theorem IsOpenMap.of_nhds_le

added theorem IsOpenMap.of_sections

added theorem IsOpenMap.preimage_closure_eq_closure_preimage

added theorem IsOpenMap.preimage_closure_subset_closure_preimage

added theorem IsOpenMap.preimage_frontier_eq_frontier_preimage

added theorem IsOpenMap.preimage_frontier_subset_frontier_preimage

added theorem IsOpenMap.preimage_interior_eq_interior_preimage

added theorem IsOpenMap.range_mem_nhds

added theorem IsOpenMap.to_quotientMap

added def IsOpenMap

added theorem OpenEmbedding.continuous

added theorem OpenEmbedding.isOpenMap

added theorem OpenEmbedding.isOpenMap_iff

added theorem OpenEmbedding.map_nhds_eq

added theorem OpenEmbedding.of_comp

added theorem OpenEmbedding.of_comp_iff

added theorem OpenEmbedding.open_iff_image_open

added theorem OpenEmbedding.open_iff_preimage_open

added theorem OpenEmbedding.tendsto_nhds_iff

added structure OpenEmbedding

added theorem QuotientMap.of_inverse

added def QuotientMap

added theorem closedEmbedding_id

added theorem closedEmbedding_of_continuous_injective_closed

added theorem closedEmbedding_of_embedding_closed

added theorem embedding_id

added theorem embedding_of_embedding_compose

added theorem inducing_id

added theorem inducing_iff_nhds

added theorem inducing_induced

added theorem inducing_of_inducing_compose

added theorem isClosedMap_iff_closure_image

added theorem isOpenMap_iff_interior

added theorem isOpenMap_iff_nhds_le

added theorem openEmbedding_id

added theorem openEmbedding_iff_continuous_injective_open

added theorem openEmbedding_iff_embedding_open

added theorem openEmbedding_of_continuous_injective_open

added theorem openEmbedding_of_embedding_open

added theorem quotientMap_iff