Documentation

Mathlib.Topology.Maps

Specific classes of maps between topological spaces #

This file introduces the following properties of a map f : X → Y→ 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_iff {α : Type u_1} {β : Type u_2} [tα : TopologicalSpace α] [tβ : TopologicalSpace β] (f : αβ) :
structure Inducing {α : Type u_1} {β : Type u_2} [tα : TopologicalSpace α] [tβ : TopologicalSpace β] (f : αβ) :

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} [inst : TopologicalSpace β] (f : αβ) :
    theorem inducing_id {α : Type u_1} [inst : TopologicalSpace α] :
    theorem Inducing.comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] [inst : TopologicalSpace γ] {g : βγ} {f : αβ} (hg : Inducing g) (hf : Inducing f) :
    theorem inducing_of_inducing_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst : TopologicalSpace β] [inst : TopologicalSpace γ] {f : αβ} {g : βγ} (hf : Continuous f) (hg : Continuous g) (hgf : Inducing (g f)) :
    theorem inducing_iff_nhds {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} :
    Inducing f ∀ (a : α), nhds a = Filter.comap f (nhds (f a))
    theorem Inducing.nhds_eq_comap {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : Inducing f) (a : α) :
    nhds a = Filter.comap f (nhds (f a))
    theorem Inducing.nhdsSet_eq_comap {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : Inducing f) (s : Set α) :
    theorem Inducing.map_nhds_eq {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : Inducing f) (a : α) :
    theorem Inducing.map_nhds_of_mem {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : Inducing f) (a : α) (h : Set.range f nhds (f a)) :
    Filter.map f (nhds a) = nhds (f a)
    theorem Inducing.mapClusterPt_iff {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : Inducing f) {a : α} {l : Filter α} :
    MapClusterPt (f a) l f ClusterPt a l
    theorem Inducing.image_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : Inducing f) {a : α} {s : Set α} (hs : s nhds a) :
    f '' s nhdsWithin (f a) (Set.range f)
    theorem Inducing.tendsto_nhds_iff {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace β] [inst : TopologicalSpace γ] {ι : Type u_1} {f : ιβ} {g : βγ} {a : Filter ι} {b : β} (hg : Inducing g) :
    Filter.Tendsto f a (nhds b) Filter.Tendsto (g f) a (nhds (g b))
    theorem Inducing.continuousAt_iff {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] [inst : TopologicalSpace γ] {f : αβ} {g : βγ} (hg : Inducing g) {x : α} :
    theorem Inducing.continuous_iff {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] [inst : TopologicalSpace γ] {f : αβ} {g : βγ} (hg : Inducing g) :
    theorem Inducing.continuousAt_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst : TopologicalSpace β] [inst : TopologicalSpace γ] {f : αβ} {g : βγ} (hf : Inducing f) {x : α} (h : Set.range f nhds (f x)) :
    theorem Inducing.continuous {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : Inducing f) :
    theorem Inducing.inducing_iff {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] [inst : TopologicalSpace γ] {f : αβ} {g : βγ} (hg : Inducing g) :
    theorem Inducing.closure_eq_preimage_closure_image {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : Inducing f) (s : Set α) :
    theorem Inducing.isClosed_iff {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : Inducing f) {s : Set α} :
    IsClosed s t, IsClosed t f ⁻¹' t = s
    theorem Inducing.isClosed_iff' {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : Inducing f) {s : Set α} :
    IsClosed s ∀ (x : α), f x closure (f '' s)x s
    theorem Inducing.isClosed_preimage {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (h : Inducing f) (s : Set β) (hs : IsClosed s) :
    theorem Inducing.isOpen_iff {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : Inducing f) {s : Set α} :
    IsOpen s t, IsOpen t f ⁻¹' t = s
    theorem Inducing.dense_iff {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : Inducing f) {s : Set α} :
    Dense s ∀ (x : α), f x closure (f '' s)
    theorem embedding_iff {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] (f : αβ) :
    structure Embedding {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] (f : αβ) extends Inducing :

    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_2} {β : Type u_1} [t : TopologicalSpace β] {f : αβ} (hf : Function.Injective f) :
      theorem Embedding.mk' {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] (f : αβ) (inj : Function.Injective f) (induced : ∀ (a : α), Filter.comap f (nhds (f a)) = nhds a) :
      theorem embedding_id {α : Type u_1} [inst : TopologicalSpace α] :
      theorem Embedding.comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] [inst : TopologicalSpace γ] {g : βγ} {f : αβ} (hg : Embedding g) (hf : Embedding f) :
      theorem embedding_of_embedding_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst : TopologicalSpace β] [inst : TopologicalSpace γ] {f : αβ} {g : βγ} (hf : Continuous f) (hg : Continuous g) (hgf : Embedding (g f)) :
      theorem Function.LeftInverse.embedding {α : Type u_2} {β : Type u_1} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} {g : βα} (h : Function.LeftInverse f g) (hf : Continuous f) (hg : Continuous g) :
      theorem Embedding.map_nhds_eq {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : Embedding f) (a : α) :
      theorem Embedding.map_nhds_of_mem {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : Embedding f) (a : α) (h : Set.range f nhds (f a)) :
      Filter.map f (nhds a) = nhds (f a)
      theorem Embedding.tendsto_nhds_iff {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace β] [inst : TopologicalSpace γ] {ι : Type u_1} {f : ιβ} {g : βγ} {a : Filter ι} {b : β} (hg : Embedding g) :
      Filter.Tendsto f a (nhds b) Filter.Tendsto (g f) a (nhds (g b))
      theorem Embedding.continuous_iff {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] [inst : TopologicalSpace γ] {f : αβ} {g : βγ} (hg : Embedding g) :
      theorem Embedding.continuous {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : Embedding f) :
      theorem Embedding.closure_eq_preimage_closure_image {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {e : αβ} (he : Embedding e) (s : Set α) :
      theorem Embedding.discreteTopology {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [tY : TopologicalSpace Y] [inst : DiscreteTopology Y] {f : XY} (hf : Embedding f) :

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

      def QuotientMap {α : Type u_1} {β : Type u_2} [tα : TopologicalSpace α] [tβ : TopologicalSpace β] (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.

      Equations
      theorem quotientMap_iff {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} :
      theorem QuotientMap.id {α : Type u_1} [inst : TopologicalSpace α] :
      theorem QuotientMap.comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] [inst : TopologicalSpace γ] {g : βγ} {f : αβ} (hg : QuotientMap g) (hf : QuotientMap f) :
      theorem QuotientMap.of_quotientMap_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst : TopologicalSpace β] [inst : TopologicalSpace γ] {g : βγ} {f : αβ} (hf : Continuous f) (hg : Continuous g) (hgf : QuotientMap (g f)) :
      theorem QuotientMap.of_inverse {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} {g : βα} (hf : Continuous f) (hg : Continuous g) (h : Function.LeftInverse g f) :
      theorem QuotientMap.continuous_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst : TopologicalSpace β] [inst : TopologicalSpace γ] {g : βγ} {f : αβ} (hf : QuotientMap f) :
      theorem QuotientMap.continuous {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : QuotientMap f) :
      theorem QuotientMap.surjective {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : QuotientMap f) :
      theorem QuotientMap.isOpen_preimage {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : QuotientMap f) {s : Set β} :
      theorem QuotientMap.isClosed_preimage {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : QuotientMap f) {s : Set β} :
      def IsOpenMap {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] (f : αβ) :

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

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

      A continuous surjective open map is a quotient map.

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

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

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

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

      Equations
      theorem IsClosedMap.id {α : Type u_1} [inst : TopologicalSpace α] :
      theorem IsClosedMap.comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] [inst : TopologicalSpace γ] {g : βγ} {f : αβ} (hg : IsClosedMap g) (hf : IsClosedMap f) :
      theorem IsClosedMap.closure_image_subset {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : IsClosedMap f) (s : Set α) :
      closure (f '' s) f '' closure s
      theorem IsClosedMap.of_inverse {α : Type u_2} {β : Type u_1} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} {f' : βα} (h : Continuous f') (l_inv : Function.LeftInverse f f') (r_inv : Function.RightInverse f f') :
      theorem IsClosedMap.of_nonempty {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (h : ∀ (s : Set α), IsClosed sSet.Nonempty sIsClosed (f '' s)) :
      theorem IsClosedMap.closed_range {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : IsClosedMap f) :
      theorem Inducing.isClosedMap {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : Inducing f) (h : IsClosed (Set.range f)) :
      theorem isClosedMap_iff_closure_image {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} :
      IsClosedMap f ∀ (s : Set α), closure (f '' s) f '' closure s
      theorem openEmbedding_iff {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] (f : αβ) :
      structure OpenEmbedding {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] (f : αβ) extends Embedding :
      • The range of an open embedding is an open set.

        open_range : IsOpen (Set.range f)

      An open embedding is an embedding with open image.

      Instances For
        theorem OpenEmbedding.isOpenMap {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : OpenEmbedding f) :
        theorem OpenEmbedding.map_nhds_eq {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : OpenEmbedding f) (a : α) :
        Filter.map f (nhds a) = nhds (f a)
        theorem OpenEmbedding.open_iff_image_open {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : OpenEmbedding f) {s : Set α} :
        theorem OpenEmbedding.tendsto_nhds_iff {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace β] [inst : TopologicalSpace γ] {ι : Type u_1} {f : ιβ} {g : βγ} {a : Filter ι} {b : β} (hg : OpenEmbedding g) :
        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} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : OpenEmbedding f) {g : βγ} {l : Filter γ} {a : α} :
        Filter.Tendsto (g f) (nhds a) l Filter.Tendsto g (nhds (f a)) l
        theorem OpenEmbedding.continuous {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : OpenEmbedding f) :
        theorem OpenEmbedding.open_iff_preimage_open {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : OpenEmbedding f) {s : Set β} (hs : s Set.range f) :
        theorem openEmbedding_of_embedding_open {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (h₁ : Embedding f) (h₂ : IsOpenMap f) :
        theorem openEmbedding_iff_embedding_open {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} :
        theorem openEmbedding_of_continuous_injective_open {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (h₁ : Continuous f) (h₂ : Function.Injective f) (h₃ : IsOpenMap f) :
        theorem OpenEmbedding.comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] [inst : TopologicalSpace γ] {g : βγ} {f : αβ} (hg : OpenEmbedding g) (hf : OpenEmbedding f) :
        theorem OpenEmbedding.isOpenMap_iff {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] [inst : TopologicalSpace γ] {g : βγ} {f : αβ} (hg : OpenEmbedding g) :
        theorem OpenEmbedding.of_comp_iff {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] [inst : TopologicalSpace γ] (f : αβ) {g : βγ} (hg : OpenEmbedding g) :
        theorem OpenEmbedding.of_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] [inst : TopologicalSpace γ] (f : αβ) {g : βγ} (hg : OpenEmbedding g) (h : OpenEmbedding (g f)) :
        theorem closedEmbedding_iff {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] (f : αβ) :
        structure ClosedEmbedding {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] (f : αβ) extends Embedding :
        • The range of a closed embedding is a closed set.

          closed_range : IsClosed (Set.range f)

        A closed embedding is an embedding with closed image.

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