# 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:

• IsOpenMap f means the image of an open set under f is open.
• IsClosedMap f means the image of a closed set under f is closed.

(Open and closed maps need not be continuous.)

• Inducing f means the topology on X is the one induced via f from the topology on Y. These behave like embeddings except they need not be injective. Instead, points of X which are identified by f are also inseparable in the topology on X.

• Embedding f means f is inducing and also injective. Equivalently, f identifies X with a subspace of Y.

• OpenEmbedding f means f is an embedding with open image, so it identifies X with an open subspace of Y. Equivalently, f is an embedding and an open map.

• ClosedEmbedding f similarly means f is an embedding with closed image, so it identifies X with a closed subspace of Y. Equivalently, f is an embedding and a closed map.

• QuotientMap f is the dual condition to Embedding f: f is surjective and the topology on Y is the one coinduced via f from the topology on X. Equivalently, f identifies Y with a quotient of X. Quotient maps are also sometimes known as identification maps.

## Tags #

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

theorem inducing_iff {α : Type u_1} {β : Type u_2} [tα : ] [tβ : ] (f : αβ) :
=
structure Inducing {α : Type u_1} {β : Type u_2} [tα : ] [tβ : ] (f : αβ) :
• induced : =

The topology on the domain is equal to the induced topology.

A function f : α → β between topological spaces is inducing if the topology on α is induced by the topology on β through f, meaning that a set s : Set α is open iff it is the preimage under f of some open set t : Set β.

Instances For
theorem inducing_induced {α : Type u_1} {β : Type u_2} [] (f : αβ) :
theorem inducing_id {α : Type u_1} [] :
theorem Inducing.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} (hg : ) (hf : ) :
theorem inducing_of_inducing_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : αβ} {g : βγ} (hf : ) (hg : ) (hgf : Inducing (g f)) :
theorem inducing_iff_nhds {α : Type u_1} {β : Type u_2} [] [] {f : αβ} :
∀ (a : α), nhds a = Filter.comap f (nhds (f a))
theorem Inducing.nhds_eq_comap {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (a : α) :
nhds a = Filter.comap f (nhds (f a))
theorem Inducing.nhdsSet_eq_comap {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (s : Set α) :
theorem Inducing.map_nhds_eq {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (a : α) :
Filter.map f (nhds a) = nhdsWithin (f a) ()
theorem Inducing.map_nhds_of_mem {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (a : α) (h : nhds (f a)) :
Filter.map f (nhds a) = nhds (f a)
theorem Inducing.mapClusterPt_iff {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) {a : α} {l : } :
MapClusterPt (f a) l f
theorem Inducing.image_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) {a : α} {s : Set α} (hs : s nhds a) :
f '' s nhdsWithin (f a) ()
theorem Inducing.tendsto_nhds_iff {β : Type u_2} {γ : Type u_3} [] [] {ι : Type u_5} {f : ιβ} {g : βγ} {a : } {b : β} (hg : ) :
Filter.Tendsto f a (nhds b) Filter.Tendsto (g f) a (nhds (g b))
theorem Inducing.continuousAt_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : αβ} {g : βγ} (hg : ) {x : α} :
theorem Inducing.continuous_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : αβ} {g : βγ} (hg : ) :
theorem Inducing.continuousAt_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : αβ} {g : βγ} (hf : ) {x : α} (h : nhds (f x)) :
theorem Inducing.continuous {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
theorem Inducing.inducing_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : αβ} {g : βγ} (hg : ) :
theorem Inducing.closure_eq_preimage_closure_image {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (s : Set α) :
= f ⁻¹' closure (f '' s)
theorem Inducing.isClosed_iff {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) {s : Set α} :
t, f ⁻¹' t = s
theorem Inducing.isClosed_iff' {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) {s : Set α} :
∀ (x : α), f x closure (f '' s)x s
theorem Inducing.isClosed_preimage {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (h : ) (s : Set β) (hs : ) :
theorem Inducing.isOpen_iff {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) {s : Set α} :
t, f ⁻¹' t = s
theorem Inducing.setOf_isOpen {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
{s | } = '' {t | }
theorem Inducing.dense_iff {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) {s : Set α} :
∀ (x : α), f x closure (f '' s)
theorem embedding_iff {α : Type u_1} {β : Type u_2} [] [] (f : αβ) :
structure Embedding {α : Type u_1} {β : Type u_2} [] [] (f : αβ) extends :

A function between topological spaces is an embedding if it is injective, and for all s : Set α, s is open iff it is the preimage of an open set.

Instances For
theorem Function.Injective.embedding_induced {α : Type u_1} {β : Type u_2} [t : ] {f : αβ} (hf : ) :
theorem Embedding.mk' {α : Type u_1} {β : Type u_2} [] [] (f : αβ) (inj : ) (induced : ∀ (a : α), Filter.comap f (nhds (f a)) = nhds a) :
theorem embedding_id {α : Type u_1} [] :
theorem Embedding.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} (hg : ) (hf : ) :
theorem embedding_of_embedding_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : αβ} {g : βγ} (hf : ) (hg : ) (hgf : Embedding (g f)) :
theorem Function.LeftInverse.embedding {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : βα} (h : ) (hf : ) (hg : ) :
theorem Embedding.map_nhds_eq {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (a : α) :
Filter.map f (nhds a) = nhdsWithin (f a) ()
theorem Embedding.map_nhds_of_mem {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (a : α) (h : nhds (f a)) :
Filter.map f (nhds a) = nhds (f a)
theorem Embedding.tendsto_nhds_iff {β : Type u_2} {γ : Type u_3} [] [] {ι : Type u_5} {f : ιβ} {g : βγ} {a : } {b : β} (hg : ) :
Filter.Tendsto f a (nhds b) Filter.Tendsto (g f) a (nhds (g b))
theorem Embedding.continuous_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : αβ} {g : βγ} (hg : ) :
theorem Embedding.continuous {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
theorem Embedding.closure_eq_preimage_closure_image {α : Type u_1} {β : Type u_2} [] [] {e : αβ} (he : ) (s : Set α) :
= e ⁻¹' closure (e '' s)
theorem Embedding.discreteTopology {X : Type u_5} {Y : Type u_6} [] [] [] {f : XY} (hf : ) :

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

def QuotientMap {α : Type u_5} {β : Type u_6} [tα : ] [tβ : ] (f : αβ) :

A function between topological spaces is a quotient map if it is surjective, and for all s : Set β, s is open iff its preimage is an open set.

Instances For
theorem quotientMap_iff {α : Type u_1} {β : Type u_2} [] [] {f : αβ} :
∀ (s : Set β), IsOpen (f ⁻¹' s)
theorem quotientMap_iff_closed {α : Type u_1} {β : Type u_2} [] [] {f : αβ} :
∀ (s : Set β), IsClosed (f ⁻¹' s)
theorem QuotientMap.id {α : Type u_1} [] :
theorem QuotientMap.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} (hg : ) (hf : ) :
theorem QuotientMap.of_quotientMap_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} (hf : ) (hg : ) (hgf : QuotientMap (g f)) :
theorem QuotientMap.of_inverse {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : βα} (hf : ) (hg : ) (h : ) :
theorem QuotientMap.continuous_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} (hf : ) :
theorem QuotientMap.continuous {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
theorem QuotientMap.surjective {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
theorem QuotientMap.isOpen_preimage {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) {s : Set β} :
theorem QuotientMap.isClosed_preimage {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) {s : Set β} :
def IsOpenMap {α : Type u_1} {β : Type u_2} [] [] (f : αβ) :

A map f : α → β is said to be an open map, if the image of any open U : Set α is open in β.

Instances For
theorem IsOpenMap.id {α : Type u_1} [] :
theorem IsOpenMap.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} (hg : ) (hf : ) :
theorem IsOpenMap.isOpen_range {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
theorem IsOpenMap.image_mem_nhds {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) {x : α} {s : Set α} (hx : s nhds x) :
f '' s nhds (f x)
theorem IsOpenMap.range_mem_nhds {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (x : α) :
nhds (f x)
theorem IsOpenMap.mapsTo_interior {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) {s : Set α} {t : Set β} (h : Set.MapsTo f s t) :
Set.MapsTo f () ()
theorem IsOpenMap.image_interior_subset {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (s : Set α) :
f '' interior (f '' s)
theorem IsOpenMap.nhds_le {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (a : α) :
nhds (f a) Filter.map f (nhds a)
theorem IsOpenMap.of_nhds_le {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ∀ (a : α), nhds (f a) Filter.map f (nhds a)) :
theorem IsOpenMap.of_sections {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (h : ∀ (x : α), g, ContinuousAt g (f x) g (f x) = x ) :
theorem IsOpenMap.of_inverse {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {f' : βα} (h : ) (l_inv : ) (r_inv : ) :
theorem IsOpenMap.to_quotientMap {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (open_map : ) (cont : ) (surj : ) :

A continuous surjective open map is a quotient map.

theorem IsOpenMap.interior_preimage_subset_preimage_interior {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) {s : Set β} :
theorem IsOpenMap.preimage_interior_eq_interior_preimage {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf₁ : ) (hf₂ : ) (s : Set β) :
theorem IsOpenMap.preimage_closure_subset_closure_preimage {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) {s : Set β} :
theorem IsOpenMap.preimage_closure_eq_closure_preimage {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (hfc : ) (s : Set β) :
theorem IsOpenMap.preimage_frontier_subset_frontier_preimage {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) {s : Set β} :
theorem IsOpenMap.preimage_frontier_eq_frontier_preimage {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (hfc : ) (s : Set β) :
theorem isOpenMap_iff_nhds_le {α : Type u_1} {β : Type u_2} [] [] {f : αβ} :
∀ (a : α), nhds (f a) Filter.map f (nhds a)
theorem isOpenMap_iff_interior {α : Type u_1} {β : Type u_2} [] [] {f : αβ} :
∀ (s : Set α), f '' interior (f '' s)
theorem Inducing.isOpenMap {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hi : ) (ho : IsOpen ()) :

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

def IsClosedMap {α : Type u_1} {β : Type u_2} [] [] (f : αβ) :

A map f : α → β is said to be a closed map, if the image of any closed U : Set α is closed in β.

Instances For
theorem IsClosedMap.id {α : Type u_1} [] :
theorem IsClosedMap.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} (hg : ) (hf : ) :
theorem IsClosedMap.closure_image_subset {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (s : Set α) :
closure (f '' s) f ''
theorem IsClosedMap.of_inverse {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {f' : βα} (h : ) (l_inv : ) (r_inv : ) :
theorem IsClosedMap.of_nonempty {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (h : ∀ (s : Set α), IsClosed (f '' s)) :
theorem IsClosedMap.closed_range {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
theorem IsClosedMap.to_quotientMap {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hcl : ) (hcont : ) (hsurj : ) :
theorem Inducing.isClosedMap {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (h : ) :
theorem isClosedMap_iff_closure_image {α : Type u_1} {β : Type u_2} [] [] {f : αβ} :
∀ (s : Set α), closure (f '' s) f ''
theorem isClosedMap_iff_clusterPt {α : Type u_1} {β : Type u_2} [] [] {f : αβ} :
∀ (s : Set α) (y : β), x, f x = y

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 {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (f_closed : ) (f_cont : ) (s : Set α) :
closure (f '' s) = f ''
theorem IsClosedMap.lift'_closure_map_eq {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (f_closed : ) (f_cont : ) (F : ) :
Filter.lift' () closure = Filter.map f (Filter.lift' F closure)
theorem IsClosedMap.mapClusterPt_iff_lift'_closure {α : Type u_1} {β : Type u_2} [] [] {F : } {f : αβ} (f_closed : ) (f_cont : ) {y : β} :
theorem openEmbedding_iff {α : Type u_1} {β : Type u_2} [] [] (f : αβ) :
structure OpenEmbedding {α : Type u_1} {β : Type u_2} [] [] (f : αβ) extends :

An open embedding is an embedding with open image.

Instances For
theorem OpenEmbedding.isOpenMap {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
theorem OpenEmbedding.map_nhds_eq {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (a : α) :
Filter.map f (nhds a) = nhds (f a)
theorem OpenEmbedding.open_iff_image_open {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) {s : Set α} :
IsOpen (f '' s)
theorem OpenEmbedding.tendsto_nhds_iff {β : Type u_2} {γ : Type u_3} [] [] {ι : Type u_5} {f : ιβ} {g : βγ} {a : } {b : β} (hg : ) :
Filter.Tendsto f a (nhds b) Filter.Tendsto (g f) a (nhds (g b))
theorem OpenEmbedding.tendsto_nhds_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : αβ} (hf : ) {g : βγ} {l : } {a : α} :
Filter.Tendsto (g f) (nhds a) l Filter.Tendsto g (nhds (f a)) l
theorem OpenEmbedding.continuous {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
theorem OpenEmbedding.open_iff_preimage_open {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) {s : Set β} (hs : s ) :
theorem openEmbedding_of_embedding_open {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (h₁ : ) (h₂ : ) :
theorem openEmbedding_iff_embedding_open {α : Type u_1} {β : Type u_2} [] [] {f : αβ} :
theorem openEmbedding_of_continuous_injective_open {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (h₁ : ) (h₂ : ) (h₃ : ) :
theorem openEmbedding_iff_continuous_injective_open {α : Type u_1} {β : Type u_2} [] [] {f : αβ} :
theorem openEmbedding_id {α : Type u_1} [] :
theorem OpenEmbedding.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} (hg : ) (hf : ) :
theorem OpenEmbedding.isOpenMap_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} (hg : ) :
theorem OpenEmbedding.of_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : αβ) {g : βγ} (hg : ) :
theorem OpenEmbedding.of_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : αβ) {g : βγ} (hg : ) (h : OpenEmbedding (g f)) :
theorem closedEmbedding_iff {α : Type u_1} {β : Type u_2} [] [] (f : αβ) :
structure ClosedEmbedding {α : Type u_1} {β : Type u_2} [] [] (f : αβ) extends :
• induced : inst✝¹ = TopologicalSpace.induced f inst✝
• inj :
• closed_range :

The range of a closed embedding is a closed set.

A closed embedding is an embedding with closed image.

Instances For
theorem ClosedEmbedding.tendsto_nhds_iff {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {ι : Type u_5} {g : ια} {a : } {b : α} (hf : ) :
Filter.Tendsto g a (nhds b) Filter.Tendsto (f g) a (nhds (f b))
theorem ClosedEmbedding.continuous {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
theorem ClosedEmbedding.isClosedMap {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
theorem ClosedEmbedding.closed_iff_image_closed {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) {s : Set α} :
IsClosed (f '' s)
theorem ClosedEmbedding.closed_iff_preimage_closed {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) {s : Set β} (hs : s ) :
theorem closedEmbedding_of_embedding_closed {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (h₁ : ) (h₂ : ) :
theorem closedEmbedding_of_continuous_injective_closed {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (h₁ : ) (h₂ : ) (h₃ : ) :
theorem closedEmbedding_id {α : Type u_1} [] :
theorem ClosedEmbedding.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} (hg : ) (hf : ) :
theorem ClosedEmbedding.closure_image_eq {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (s : Set α) :
closure (f '' s) = f ''