Commit 2024-01-08 13:15 303bf519

View on Github →

chore(Topology/Maps): small clean-ups (#9268)

Make sure each new definition is in a separate section.
Add corresponding namespaces where missing.
Collect TopologicalSpace assumptions.
Collect variables ${f : \alpha \to \beta}$ and ${g : \beta \to \gamma}$ in theorems; we leave definitions alone.
In a later PR, we will rename the type variables in this file: this reduces the diff in doing so.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean

Modified Mathlib/Topology/Maps.lean

modified theorem ClosedEmbedding.closed_iff_image_closed

modified theorem ClosedEmbedding.closed_iff_preimage_closed

modified theorem ClosedEmbedding.closure_image_eq

modified theorem ClosedEmbedding.comp

modified theorem ClosedEmbedding.continuous

modified theorem ClosedEmbedding.isClosedMap

modified theorem ClosedEmbedding.tendsto_nhds_iff

modified theorem Embedding.continuous

modified theorem Embedding.continuous_iff

modified theorem Embedding.map_nhds_eq

modified theorem Embedding.map_nhds_of_mem

modified theorem Embedding.tendsto_nhds_iff

modified theorem Embedding.toOpenEmbedding_of_surjective

modified theorem Inducing.closure_eq_preimage_closure_image

modified theorem Inducing.continuousAt_iff'

modified theorem Inducing.continuousAt_iff

modified theorem Inducing.continuous_iff

modified theorem Inducing.dense_iff

modified theorem Inducing.image_mem_nhdsWithin

modified theorem Inducing.isClosedMap

modified theorem Inducing.isClosed_iff'

modified theorem Inducing.isClosed_iff

modified theorem Inducing.isClosed_preimage

modified theorem Inducing.isOpen_iff

modified theorem Inducing.mapClusterPt_iff

modified theorem Inducing.map_nhds_eq

modified theorem Inducing.map_nhds_of_mem

modified theorem Inducing.nhdsSet_eq_comap

modified theorem Inducing.nhds_eq_comap

modified theorem Inducing.setOf_isOpen

modified theorem Inducing.tendsto_nhds_iff

modified theorem IsClosedMap.closed_range

modified theorem IsClosedMap.closure_image_eq_of_continuous

modified theorem IsClosedMap.closure_image_subset

modified theorem IsClosedMap.lift'_closure_map_eq

modified theorem IsClosedMap.mapClusterPt_iff_lift'_closure

modified theorem IsClosedMap.of_inverse

modified theorem IsClosedMap.of_nonempty

modified theorem IsClosedMap.to_quotientMap

modified theorem IsOpenMap.of_inverse

modified theorem IsOpenMap.of_sections

modified theorem IsOpenMap.to_quotientMap

modified theorem OpenEmbedding.continuous

modified theorem OpenEmbedding.continuousAt_iff

modified theorem OpenEmbedding.isOpenMap

modified theorem OpenEmbedding.isOpenMap_iff

modified theorem OpenEmbedding.map_nhds_eq

modified theorem OpenEmbedding.of_comp

modified theorem OpenEmbedding.of_comp_iff

modified theorem OpenEmbedding.open_iff_image_open

modified theorem OpenEmbedding.open_iff_preimage_open

modified theorem OpenEmbedding.tendsto_nhds_iff'

modified theorem OpenEmbedding.tendsto_nhds_iff

modified theorem closedEmbedding_id

modified theorem closedEmbedding_of_continuous_injective_closed

modified theorem closedEmbedding_of_embedding_closed

modified theorem embedding_of_embedding_compose

modified theorem inducing_iff_nhds

modified theorem inducing_of_inducing_compose

modified theorem isClosedMap_iff_closure_image

modified theorem isClosedMap_iff_clusterPt

modified theorem isOpenMap_iff_interior

modified theorem isOpenMap_iff_nhds_le

modified theorem openEmbedding_iff_continuous_injective_open

modified theorem openEmbedding_iff_embedding_open

modified theorem openEmbedding_of_continuous_injective_open

modified theorem openEmbedding_of_embedding_open

modified theorem quotientMap_iff

modified theorem quotientMap_iff_closed