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.

References

Tags

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

theorem inducing_iff {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) : Inducing f ↔ tX = TopologicalSpace.induced f tY

structure Inducing {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) : Prop

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

• induced : tX = TopologicalSpace.induced f tY

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

theorem inducing_induced {X : Type u_1} {Y : Type u_2} [TopologicalSpace Y] (f : X → Y) : Inducing f

theorem inducing_id {X : Type u_1} [TopologicalSpace X] : Inducing id

theorem Inducing.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : Inducing g) (hf : Inducing f) : Inducing (g ∘ f)

theorem inducing_of_inducing_compose {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hf : Continuous f) (hg : Continuous g) (hgf : Inducing (g ∘ f)) : Inducing f

theorem inducing_iff_nhds {X : Type u_1} {Y : Type u_2} {f : X → Y} [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 : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) (x : X) : nhds x = Filter.comap f (nhds (f x))

theorem Inducing.nhdsSet_eq_comap {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) (s : Set X) : nhdsSet s = Filter.comap f (nhdsSet (f '' s))

theorem Inducing.map_nhds_eq {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) (x : X) : Filter.map f (nhds x) = nhdsWithin (f x) (Set.range f)

theorem Inducing.map_nhds_of_mem {X : Type u_1} {Y : Type u_2} {f : X → Y} [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 : X → Y} [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 : X → Y} [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 : Y → Z} [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 : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : Inducing g) {x : X} : ContinuousAt f x ↔ ContinuousAt (g ∘ f) x

theorem Inducing.continuous_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : Inducing g) : Continuous f ↔ Continuous (g ∘ f)

theorem Inducing.continuousAt_iff' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hf : Inducing f) {x : X} (h : Set.range f ∈ nhds (f x)) : ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)

theorem Inducing.continuous {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) : Continuous f

theorem Inducing.inducing_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : Inducing g) : Inducing f ↔ Inducing (g ∘ f)

theorem Inducing.closure_eq_preimage_closure_image {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) (s : Set X) : closure s = f ⁻¹' closure (f '' s)

theorem Inducing.isClosed_iff {X : Type u_1} {Y : Type u_2} {f : X → Y} [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 : X → Y} [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 : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (h : Inducing f) (s : Set Y) (hs : IsClosed s) : IsClosed (f ⁻¹' s)

theorem Inducing.isOpen_iff {X : Type u_1} {Y : Type u_2} {f : X → Y} [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 : X → Y} [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 : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) {s : Set X} : Dense s ↔ ∀ (x : X), f x ∈ closure (f '' s)

theorem embedding_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : Embedding f ↔ Inducing f ∧ Function.Injective f

structure Embedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) extends Inducing : Prop

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

• induced : inst✝¹ = TopologicalSpace.induced f inst✝
• inj : Function.Injective f

  A topological embedding is injective.

theorem Function.Injective.embedding_induced {X : Type u_1} {Y : Type u_2} {f : X → Y} [t : TopologicalSpace Y] (hf : Function.Injective f) : Embedding f

theorem Embedding.mk' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (inj : Function.Injective f) (induced : ∀ (x : X), Filter.comap f (nhds (f x)) = nhds x) : Embedding f

theorem embedding_id {X : Type u_1} [TopologicalSpace X] : Embedding id

theorem Embedding.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : Embedding g) (hf : Embedding f) : Embedding (g ∘ f)

theorem embedding_of_embedding_compose {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hf : Continuous f) (hg : Continuous g) (hgf : Embedding (g ∘ f)) : Embedding f

theorem Function.LeftInverse.embedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {g : Y → X} (h : Function.LeftInverse f g) (hf : Continuous f) (hg : Continuous g) : Embedding g

theorem Embedding.map_nhds_eq {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Embedding f) (x : X) : Filter.map f (nhds x) = nhdsWithin (f x) (Set.range f)

theorem Embedding.map_nhds_of_mem {X : Type u_1} {Y : Type u_2} {f : X → Y} [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 : Y → Z} [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 : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : Embedding g) : Continuous f ↔ Continuous (g ∘ f)

theorem Embedding.continuous {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Embedding f) : Continuous f

theorem Embedding.closure_eq_preimage_closure_image {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Embedding f) (s : Set X) : closure s = f ⁻¹' closure (f '' s)

theorem Embedding.discreteTopology {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] [DiscreteTopology Y] (hf : Embedding f) : DiscreteTopology X

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.

def QuotientMap {X : Type u_5} {Y : Type u_6} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) : Prop

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

Equations

• QuotientMap f = (Function.Surjective f ∧ tY = TopologicalSpace.coinduced f tX)

theorem quotientMap_iff {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] : QuotientMap f ↔ Function.Surjective f ∧ ∀ (s : Set Y), IsOpen s ↔ IsOpen (f ⁻¹' s)

theorem quotientMap_iff_closed {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] : QuotientMap f ↔ Function.Surjective f ∧ ∀ (s : Set Y), IsClosed s ↔ IsClosed (f ⁻¹' s)

theorem QuotientMap.id {X : Type u_1} [TopologicalSpace X] : QuotientMap id

theorem QuotientMap.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : QuotientMap g) (hf : QuotientMap f) : QuotientMap (g ∘ f)

theorem QuotientMap.of_quotientMap_compose {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hf : Continuous f) (hg : Continuous g) (hgf : QuotientMap (g ∘ f)) : QuotientMap g

theorem QuotientMap.of_inverse {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] {g : Y → X} (hf : Continuous f) (hg : Continuous g) (h : Function.LeftInverse g f) : QuotientMap g

theorem QuotientMap.continuous_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hf : QuotientMap f) : Continuous g ↔ Continuous (g ∘ f)

theorem QuotientMap.continuous {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : QuotientMap f) : Continuous f

theorem QuotientMap.surjective {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : QuotientMap f) : Function.Surjective f

theorem QuotientMap.isOpen_preimage {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : QuotientMap f) {s : Set Y} : IsOpen (f ⁻¹' s) ↔ IsOpen s

theorem QuotientMap.isClosed_preimage {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : QuotientMap f) {s : Set Y} : IsClosed (f ⁻¹' s) ↔ IsClosed s

def IsOpenMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : Prop

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

Equations

• IsOpenMap f = ∀ (U : Set X), IsOpen U → IsOpen (f '' U)

theorem IsOpenMap.id {X : Type u_1} [TopologicalSpace X] : IsOpenMap id

theorem IsOpenMap.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : IsOpenMap g) (hf : IsOpenMap f) : IsOpenMap (g ∘ f)

theorem IsOpenMap.isOpen_range {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) : IsOpen (Set.range f)

theorem IsOpenMap.image_mem_nhds {X : Type u_1} {Y : Type u_2} {f : X → Y} [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 : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) (x : X) : Set.range f ∈ nhds (f x)

theorem IsOpenMap.mapsTo_interior {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) {s : Set X} {t : Set Y} (h : Set.MapsTo f s t) : Set.MapsTo f (interior s) (interior t)

theorem IsOpenMap.image_interior_subset {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) (s : Set X) : f '' interior s ⊆ interior (f '' s)

theorem IsOpenMap.nhds_le {X : Type u_1} {Y : Type u_2} {f : X → Y} [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 : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : ∀ (x : X), nhds (f x) ≤ Filter.map f (nhds x)) : IsOpenMap f

theorem IsOpenMap.of_sections {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (h : ∀ (x : X), ∃ (g : Y → X), ContinuousAt g (f x) ∧ g (f x) = x ∧ Function.RightInverse g f) : IsOpenMap f

theorem IsOpenMap.of_inverse {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] {f' : Y → X} (h : Continuous f') (l_inv : Function.LeftInverse f f') (r_inv : Function.RightInverse f f') : IsOpenMap f

theorem IsOpenMap.to_quotientMap {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (open_map : IsOpenMap f) (cont : Continuous f) (surj : Function.Surjective f) : QuotientMap f

A continuous surjective open map is a quotient map.

theorem IsOpenMap.interior_preimage_subset_preimage_interior {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) {s : Set Y} : interior (f ⁻¹' s) ⊆ f ⁻¹' interior s

theorem IsOpenMap.preimage_interior_eq_interior_preimage {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf₁ : IsOpenMap f) (hf₂ : Continuous f) (s : Set Y) : f ⁻¹' interior s = interior (f ⁻¹' s)

theorem IsOpenMap.preimage_closure_subset_closure_preimage {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) {s : Set Y} : f ⁻¹' closure s ⊆ closure (f ⁻¹' s)

theorem IsOpenMap.preimage_closure_eq_closure_preimage {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) (hfc : Continuous f) (s : Set Y) : f ⁻¹' closure s = closure (f ⁻¹' s)

theorem IsOpenMap.preimage_frontier_subset_frontier_preimage {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) {s : Set Y} : f ⁻¹' frontier s ⊆ frontier (f ⁻¹' s)

theorem IsOpenMap.preimage_frontier_eq_frontier_preimage {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) (hfc : Continuous f) (s : Set Y) : f ⁻¹' frontier s = frontier (f ⁻¹' s)

theorem isOpenMap_iff_nhds_le {X : Type u_1} {Y : Type u_2} {f : X → Y} [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 : X → Y} [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 : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hi : Inducing f) (ho : IsOpen (Set.range f)) : IsOpenMap f

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

def IsClosedMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : Prop

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

Equations

• IsClosedMap f = ∀ (U : Set X), IsClosed U → IsClosed (f '' U)

theorem IsClosedMap.id {X : Type u_1} [TopologicalSpace X] : IsClosedMap id

theorem IsClosedMap.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : IsClosedMap g) (hf : IsClosedMap f) : IsClosedMap (g ∘ f)

theorem IsClosedMap.closure_image_subset {X : Type u_1} {Y : Type u_2} {f : X → Y} [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 : X → Y} [TopologicalSpace X] [TopologicalSpace Y] {f' : Y → X} (h : Continuous f') (l_inv : Function.LeftInverse f f') (r_inv : Function.RightInverse f f') : IsClosedMap f

theorem IsClosedMap.of_nonempty {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (h : ∀ (s : Set X), IsClosed s → Set.Nonempty s → IsClosed (f '' s)) : IsClosedMap f

theorem IsClosedMap.closed_range {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsClosedMap f) : IsClosed (Set.range f)

theorem IsClosedMap.to_quotientMap {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hcl : IsClosedMap f) (hcont : Continuous f) (hsurj : Function.Surjective f) : QuotientMap f

theorem Inducing.isClosedMap {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Inducing f) (h : IsClosed (Set.range f)) : IsClosedMap f

theorem isClosedMap_iff_closure_image {X : Type u_1} {Y : Type u_2} {f : X → Y} [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 : X → Y} [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 : X → Y} [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 : X → Y} [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 : X → Y} [TopologicalSpace X] [TopologicalSpace Y] {F : Filter X} (f_closed : IsClosedMap f) (f_cont : Continuous f) {y : Y} : MapClusterPt y F f ↔ Filter.NeBot (Filter.lift' F closure ⊓ Filter.principal (f ⁻¹' {y}))

theorem openEmbedding_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : OpenEmbedding f ↔ Embedding f ∧ IsOpen (Set.range f)

structure OpenEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) extends Embedding : Prop

An open embedding is an embedding with open image.

• induced : inst✝¹ = TopologicalSpace.induced f inst✝
• inj : Function.Injective f
• open_range : IsOpen (Set.range f)

  The range of an open embedding is an open set.

theorem OpenEmbedding.isOpenMap {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : OpenEmbedding f) : IsOpenMap f

theorem OpenEmbedding.map_nhds_eq {X : Type u_1} {Y : Type u_2} {f : X → Y} [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 : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : OpenEmbedding f) {s : Set X} : IsOpen s ↔ IsOpen (f '' s)

theorem OpenEmbedding.tendsto_nhds_iff {Y : Type u_2} {Z : Type u_3} {ι : Type u_4} {g : Y → Z} [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 : X → Y} {g : Y → Z} [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 : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hf : OpenEmbedding f) {x : X} : ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)

theorem OpenEmbedding.continuous {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : OpenEmbedding f) : Continuous f

theorem OpenEmbedding.open_iff_preimage_open {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : OpenEmbedding f) {s : Set Y} (hs : s ⊆ Set.range f) : IsOpen s ↔ IsOpen (f ⁻¹' s)

theorem openEmbedding_of_embedding_open {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (h₁ : Embedding f) (h₂ : IsOpenMap f) : OpenEmbedding f

theorem Embedding.toOpenEmbedding_of_surjective {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Embedding f) (hsurj : Function.Surjective f) : OpenEmbedding f

A surjective embedding is an OpenEmbedding.

theorem openEmbedding_iff_embedding_open {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] : OpenEmbedding f ↔ Embedding f ∧ IsOpenMap f

theorem openEmbedding_of_continuous_injective_open {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (h₁ : Continuous f) (h₂ : Function.Injective f) (h₃ : IsOpenMap f) : OpenEmbedding f

theorem openEmbedding_iff_continuous_injective_open {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] : OpenEmbedding f ↔ Continuous f ∧ Function.Injective f ∧ IsOpenMap f

theorem openEmbedding_id {X : Type u_1} [TopologicalSpace X] : OpenEmbedding id

theorem OpenEmbedding.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : OpenEmbedding g) (hf : OpenEmbedding f) : OpenEmbedding (g ∘ f)

theorem OpenEmbedding.isOpenMap_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : OpenEmbedding g) : IsOpenMap f ↔ IsOpenMap (g ∘ f)

theorem OpenEmbedding.of_comp_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : X → Y) (hg : OpenEmbedding g) : OpenEmbedding (g ∘ f) ↔ OpenEmbedding f

theorem OpenEmbedding.of_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : X → Y) (hg : OpenEmbedding g) (h : OpenEmbedding (g ∘ f)) : OpenEmbedding f

theorem closedEmbedding_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : ClosedEmbedding f ↔ Embedding f ∧ IsClosed (Set.range f)

structure ClosedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) extends Embedding : Prop

A closed embedding is an embedding with closed image.

• induced : inst✝¹ = TopologicalSpace.induced f inst✝
• inj : Function.Injective f
• closed_range : IsClosed (Set.range f)

  The range of a closed embedding is a closed set.

theorem ClosedEmbedding.tendsto_nhds_iff {X : Type u_1} {Y : Type u_2} {ι : Type u_4} {f : X → Y} [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 : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : ClosedEmbedding f) : Continuous f

theorem ClosedEmbedding.isClosedMap {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : ClosedEmbedding f) : IsClosedMap f

theorem ClosedEmbedding.closed_iff_image_closed {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : ClosedEmbedding f) {s : Set X} : IsClosed s ↔ IsClosed (f '' s)

theorem ClosedEmbedding.closed_iff_preimage_closed {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : ClosedEmbedding f) {s : Set Y} (hs : s ⊆ Set.range f) : IsClosed s ↔ IsClosed (f ⁻¹' s)

theorem closedEmbedding_of_embedding_closed {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (h₁ : Embedding f) (h₂ : IsClosedMap f) : ClosedEmbedding f

theorem closedEmbedding_of_continuous_injective_closed {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (h₁ : Continuous f) (h₂ : Function.Injective f) (h₃ : IsClosedMap f) : ClosedEmbedding f

theorem closedEmbedding_id {X : Type u_1} [TopologicalSpace X] : ClosedEmbedding id

theorem ClosedEmbedding.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : ClosedEmbedding g) (hf : ClosedEmbedding f) : ClosedEmbedding (g ∘ f)

theorem ClosedEmbedding.closure_image_eq {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : ClosedEmbedding f) (s : Set X) : closure (f '' s) = f '' closure s