Documentation

Mathlib.Topology.Maps

Specific classes of maps between topological spaces #

This file introduces the following properties of a map f : X → Y between topological spaces:

(Open and closed maps need not be continuous.)

References #

Tags #

open map, closed map, embedding, quotient map, identification map

theorem inducing_induced {X : Type u_1} {Y : Type u_2} [TopologicalSpace Y] (f : XY) :
theorem Inducing.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : XY} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : Inducing g) (hf : Inducing f) :
theorem inducing_of_inducing_compose {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : XY} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hf : Continuous f) (hg : Continuous g) (hgf : Inducing (g f)) :
theorem inducing_iff_nhds {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] :
Inducing f ∀ (x : X), nhds x = Filter.comap f (nhds (f x))
theorem Inducing.nhds_eq_comap {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) (x : X) :
nhds x = Filter.comap f (nhds (f x))
theorem Inducing.basis_nhds {X : Type u_1} {Y : Type u_2} {ι : Type u_4} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] {p : ιProp} {s : ιSet Y} (hf : Inducing f) {x : X} (h_basis : Filter.HasBasis (nhds (f x)) p s) :
theorem Inducing.nhdsSet_eq_comap {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) (s : Set X) :
theorem Inducing.map_nhds_eq {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) (x : X) :
theorem Inducing.map_nhds_of_mem {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) (x : X) (h : Set.range f nhds (f x)) :
Filter.map f (nhds x) = nhds (f x)
theorem Inducing.mapClusterPt_iff {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) {x : X} {l : Filter X} :
MapClusterPt (f x) l f ClusterPt x l
theorem Inducing.image_mem_nhdsWithin {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) {x : X} {s : Set X} (hs : s nhds x) :
f '' s nhdsWithin (f x) (Set.range f)
theorem Inducing.tendsto_nhds_iff {Y : Type u_2} {Z : Type u_3} {ι : Type u_4} {g : YZ} [TopologicalSpace Y] [TopologicalSpace Z] {f : ιY} {l : Filter ι} {y : Y} (hg : Inducing g) :
Filter.Tendsto f l (nhds y) Filter.Tendsto (g f) l (nhds (g y))
theorem Inducing.continuousAt_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : XY} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : Inducing g) {x : X} :
theorem Inducing.continuous_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : XY} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : Inducing g) :
theorem Inducing.continuousAt_iff' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : XY} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hf : Inducing f) {x : X} (h : Set.range f nhds (f x)) :
theorem Inducing.continuous {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) :
theorem Inducing.inducing_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : XY} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : Inducing g) :
theorem Inducing.closure_eq_preimage_closure_image {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) (s : Set X) :
theorem Inducing.isClosed_iff {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) {s : Set X} :
IsClosed s ∃ (t : Set Y), IsClosed t f ⁻¹' t = s
theorem Inducing.isClosed_iff' {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) {s : Set X} :
IsClosed s ∀ (x : X), f x closure (f '' s)x s
theorem Inducing.isClosed_preimage {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (h : Inducing f) (s : Set Y) (hs : IsClosed s) :
theorem Inducing.isOpen_iff {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) {s : Set X} :
IsOpen s ∃ (t : Set Y), IsOpen t f ⁻¹' t = s
theorem Inducing.setOf_isOpen {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) :
{s : Set X | IsOpen s} = Set.preimage f '' {t : Set Y | IsOpen t}
theorem Inducing.dense_iff {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) {s : Set X} :
Dense s ∀ (x : X), f x closure (f '' s)
theorem Function.Injective.embedding_induced {X : Type u_1} {Y : Type u_2} {f : XY} [t : TopologicalSpace Y] (hf : Function.Injective f) :
theorem Embedding.mk' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) (inj : Function.Injective f) (induced : ∀ (x : X), Filter.comap f (nhds (f x)) = nhds x) :
theorem Embedding.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : XY} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : Embedding g) (hf : Embedding f) :
theorem embedding_of_embedding_compose {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : XY} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hf : Continuous f) (hg : Continuous g) (hgf : Embedding (g f)) :
theorem Function.LeftInverse.embedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {g : YX} (h : Function.LeftInverse f g) (hf : Continuous f) (hg : Continuous g) :
theorem Embedding.map_nhds_eq {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : Embedding f) (x : X) :
theorem Embedding.map_nhds_of_mem {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : Embedding f) (x : X) (h : Set.range f nhds (f x)) :
Filter.map f (nhds x) = nhds (f x)
theorem Embedding.tendsto_nhds_iff {Y : Type u_2} {Z : Type u_3} {ι : Type u_4} {g : YZ} [TopologicalSpace Y] [TopologicalSpace Z] {f : ιY} {l : Filter ι} {y : Y} (hg : Embedding g) :
Filter.Tendsto f l (nhds y) Filter.Tendsto (g f) l (nhds (g y))
theorem Embedding.continuous_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : XY} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : Embedding g) :
theorem Embedding.continuous {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : Embedding f) :
theorem Embedding.closure_eq_preimage_closure_image {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : Embedding f) (s : Set X) :
theorem Embedding.discreteTopology {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] [DiscreteTopology Y] (hf : Embedding f) :

The topology induced under an inclusion f : X → Y from a discrete topological space Y is the discrete topology on X.

See also DiscreteTopology.of_continuous_injective.

theorem quotientMap_iff {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] :
theorem quotientMap_iff_closed {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] :
theorem QuotientMap.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : XY} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : QuotientMap g) (hf : QuotientMap f) :
theorem QuotientMap.of_quotientMap_compose {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : XY} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hf : Continuous f) (hg : Continuous g) (hgf : QuotientMap (g f)) :
theorem QuotientMap.of_inverse {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] {g : YX} (hf : Continuous f) (hg : Continuous g) (h : Function.LeftInverse g f) :
theorem QuotientMap.continuous_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : XY} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hf : QuotientMap f) :
theorem QuotientMap.continuous {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : QuotientMap f) :
theorem QuotientMap.surjective {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : QuotientMap f) :
theorem QuotientMap.isOpen_preimage {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : QuotientMap f) {s : Set Y} :
theorem QuotientMap.isClosed_preimage {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : QuotientMap f) {s : Set Y} :
theorem IsOpenMap.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : XY} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : IsOpenMap g) (hf : IsOpenMap f) :
theorem IsOpenMap.isOpen_range {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) :
theorem IsOpenMap.image_mem_nhds {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) {x : X} {s : Set X} (hx : s nhds x) :
f '' s nhds (f x)
theorem IsOpenMap.range_mem_nhds {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) (x : X) :
theorem IsOpenMap.mapsTo_interior {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) {s : Set X} {t : Set Y} (h : Set.MapsTo f s t) :
theorem IsOpenMap.image_interior_subset {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) (s : Set X) :
theorem IsOpenMap.nhds_le {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) (x : X) :
nhds (f x) Filter.map f (nhds x)
theorem IsOpenMap.of_nhds_le {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : ∀ (x : X), nhds (f x) Filter.map f (nhds x)) :
theorem IsOpenMap.of_sections {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (h : ∀ (x : X), ∃ (g : YX), ContinuousAt g (f x) g (f x) = x Function.RightInverse g f) :
theorem IsOpenMap.of_inverse {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] {f' : YX} (h : Continuous f') (l_inv : Function.LeftInverse f f') (r_inv : Function.RightInverse f f') :
theorem IsOpenMap.to_quotientMap {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (open_map : IsOpenMap f) (cont : Continuous f) (surj : Function.Surjective f) :

A continuous surjective open map is a quotient map.

theorem IsOpenMap.preimage_interior_eq_interior_preimage {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf₁ : IsOpenMap f) (hf₂ : Continuous f) (s : Set Y) :
theorem IsOpenMap.preimage_closure_eq_closure_preimage {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) (hfc : Continuous f) (s : Set Y) :
theorem IsOpenMap.preimage_frontier_eq_frontier_preimage {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) (hfc : Continuous f) (s : Set Y) :
theorem isOpenMap_iff_nhds_le {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] :
IsOpenMap f ∀ (x : X), nhds (f x) Filter.map f (nhds x)
theorem isOpenMap_iff_interior {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] :
IsOpenMap f ∀ (s : Set X), f '' interior s interior (f '' s)
theorem Inducing.isOpenMap {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hi : Inducing f) (ho : IsOpen (Set.range f)) :

An inducing map with an open range is an open map.

theorem IsClosedMap.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : XY} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : IsClosedMap g) (hf : IsClosedMap f) :
theorem IsClosedMap.closure_image_subset {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsClosedMap f) (s : Set X) :
closure (f '' s) f '' closure s
theorem IsClosedMap.of_inverse {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] {f' : YX} (h : Continuous f') (l_inv : Function.LeftInverse f f') (r_inv : Function.RightInverse f f') :
theorem IsClosedMap.of_nonempty {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (h : ∀ (s : Set X), IsClosed sSet.Nonempty sIsClosed (f '' s)) :
theorem IsClosedMap.isClosed_range {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsClosedMap f) :
@[deprecated IsClosedMap.isClosed_range]
theorem IsClosedMap.closed_range {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsClosedMap f) :

Alias of IsClosedMap.isClosed_range.

theorem IsClosedMap.to_quotientMap {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hcl : IsClosedMap f) (hcont : Continuous f) (hsurj : Function.Surjective f) :
theorem Inducing.isClosedMap {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) (h : IsClosed (Set.range f)) :
theorem isClosedMap_iff_closure_image {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] :
IsClosedMap f ∀ (s : Set X), closure (f '' s) f '' closure s
theorem isClosedMap_iff_clusterPt {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] :
IsClosedMap f ∀ (s : Set X) (y : Y), MapClusterPt y (Filter.principal s) f∃ (x : X), f x = y ClusterPt x (Filter.principal s)

A map f : X → Y is closed if and only if for all sets s, any cluster point of f '' s is the image by f of some cluster point of s. If you require this for all filters instead of just principal filters, and also that f is continuous, you get the notion of proper map. See isProperMap_iff_clusterPt.

theorem IsClosedMap.closure_image_eq_of_continuous {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (f_closed : IsClosedMap f) (f_cont : Continuous f) (s : Set X) :
closure (f '' s) = f '' closure s
theorem IsClosedMap.lift'_closure_map_eq {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (f_closed : IsClosedMap f) (f_cont : Continuous f) (F : Filter X) :
Filter.lift' (Filter.map f F) closure = Filter.map f (Filter.lift' F closure)
theorem IsClosedMap.mapClusterPt_iff_lift'_closure {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] {F : Filter X} (f_closed : IsClosedMap f) (f_cont : Continuous f) {y : Y} :
theorem OpenEmbedding.isOpenMap {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : OpenEmbedding f) :
theorem OpenEmbedding.map_nhds_eq {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : OpenEmbedding f) (x : X) :
Filter.map f (nhds x) = nhds (f x)
theorem OpenEmbedding.open_iff_image_open {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : OpenEmbedding f) {s : Set X} :
theorem OpenEmbedding.tendsto_nhds_iff {Y : Type u_2} {Z : Type u_3} {ι : Type u_4} {g : YZ} [TopologicalSpace Y] [TopologicalSpace Z] {f : ιY} {l : Filter ι} {y : Y} (hg : OpenEmbedding g) :
Filter.Tendsto f l (nhds y) Filter.Tendsto (g f) l (nhds (g y))
theorem OpenEmbedding.tendsto_nhds_iff' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : XY} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] (hf : OpenEmbedding f) {l : Filter Z} {x : X} :
Filter.Tendsto (g f) (nhds x) l Filter.Tendsto g (nhds (f x)) l
theorem OpenEmbedding.continuousAt_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : XY} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hf : OpenEmbedding f) {x : X} :
theorem OpenEmbedding.continuous {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : OpenEmbedding f) :
theorem OpenEmbedding.open_iff_preimage_open {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : OpenEmbedding f) {s : Set Y} (hs : s Set.range f) :
theorem openEmbedding_of_embedding_open {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (h₁ : Embedding f) (h₂ : IsOpenMap f) :
theorem Embedding.toOpenEmbedding_of_surjective {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : Embedding f) (hsurj : Function.Surjective f) :

A surjective embedding is an OpenEmbedding.

theorem openEmbedding_of_continuous_injective_open {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (h₁ : Continuous f) (h₂ : Function.Injective f) (h₃ : IsOpenMap f) :
theorem OpenEmbedding.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : XY} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : OpenEmbedding g) (hf : OpenEmbedding f) :
theorem OpenEmbedding.isOpenMap_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : XY} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : OpenEmbedding g) :
theorem OpenEmbedding.of_comp_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : XY) (hg : OpenEmbedding g) :
theorem OpenEmbedding.of_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : XY) (hg : OpenEmbedding g) (h : OpenEmbedding (g f)) :
theorem ClosedEmbedding.tendsto_nhds_iff {X : Type u_1} {Y : Type u_2} {ι : Type u_4} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] {g : ιX} {l : Filter ι} {x : X} (hf : ClosedEmbedding f) :
Filter.Tendsto g l (nhds x) Filter.Tendsto (f g) l (nhds (f x))
theorem ClosedEmbedding.continuous {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : ClosedEmbedding f) :
theorem ClosedEmbedding.isClosedMap {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : ClosedEmbedding f) :
theorem ClosedEmbedding.closed_iff_image_closed {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : ClosedEmbedding f) {s : Set X} :
theorem ClosedEmbedding.closed_iff_preimage_closed {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : ClosedEmbedding f) {s : Set Y} (hs : s Set.range f) :
theorem closedEmbedding_of_embedding_closed {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (h₁ : Embedding f) (h₂ : IsClosedMap f) :
theorem ClosedEmbedding.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : XY} {g : YZ} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : ClosedEmbedding g) (hf : ClosedEmbedding f) :
theorem ClosedEmbedding.closure_image_eq {X : Type u_1} {Y : Type u_2} {f : XY} [TopologicalSpace X] [TopologicalSpace Y] (hf : ClosedEmbedding f) (s : Set X) :
closure (f '' s) = f '' closure s