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.)

IsInducing 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.
IsEmbedding f means f is inducing and also injective. Equivalently, f identifies X with a subspace of Y.
IsOpenEmbedding 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.
IsClosedEmbedding 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.
IsQuotientMap f is the dual condition to IsEmbedding 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

source

theorem Topology.IsInducing.induced {X : Type u_1} {Y : Type u_2} [TopologicalSpace Y] (f : X → Y) :

IsInducing f

source

@[deprecated Topology.IsInducing.induced (since := "2024-10-28")]

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

IsInducing f

Alias of Topology.IsInducing.induced.

source

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

IsInducing id

source

@[deprecated Topology.IsInducing.id (since := "2024-10-28")]

theorem Topology.inducing_id {X : Type u_1} [TopologicalSpace X] :

IsInducing id

Alias of Topology.IsInducing.id.

source

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

IsInducing (g ∘ f)

source

@[deprecated Topology.IsInducing.comp (since := "2024-10-28")]

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

IsInducing (g ∘ f)

Alias of Topology.IsInducing.comp.

source

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

IsInducing (g ∘ f) ↔ IsInducing f

source

@[deprecated Topology.IsInducing.of_comp_iff (since := "2024-10-28")]

theorem Topology.Inducing.of_comp_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace Y] [TopologicalSpace X] [TopologicalSpace Z] (hg : IsInducing g) :

IsInducing (g ∘ f) ↔ IsInducing f

Alias of Topology.IsInducing.of_comp_iff.

source

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

IsInducing f

source

@[deprecated Topology.IsInducing.of_comp (since := "2024-10-28")]

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

IsInducing f

Alias of Topology.IsInducing.of_comp.

source

theorem Topology.isInducing_iff_nhds {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] :

IsInducing f ↔ ∀ (x : X), nhds x = Filter.comap f (nhds (f x))

source

@[deprecated Topology.isInducing_iff_nhds (since := "2024-10-28")]

theorem Topology.inducing_iff_nhds {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] :

IsInducing f ↔ ∀ (x : X), nhds x = Filter.comap f (nhds (f x))

Alias of Topology.isInducing_iff_nhds.

source

theorem Topology.IsInducing.nhds_eq_comap {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : IsInducing f) (x : X) :

nhds x = Filter.comap f (nhds (f x))

source

theorem Topology.IsInducing.basis_nhds {X : Type u_1} {Y : Type u_2} {ι : Type u_4} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] {p : ι → Prop} {s : ι → Set Y} (hf : IsInducing f) {x : X} (h_basis : (nhds (f x)).HasBasis p s) :

(nhds x).HasBasis p (Set.preimage f ∘ s)

source

theorem Topology.IsInducing.nhdsSet_eq_comap {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : IsInducing f) (s : Set X) :

nhdsSet s = Filter.comap f (nhdsSet (f '' s))

source

theorem Topology.IsInducing.map_nhds_eq {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : IsInducing f) (x : X) :

Filter.map f (nhds x) = nhdsWithin (f x) (Set.range f)

source

theorem Topology.IsInducing.map_nhds_of_mem {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : IsInducing f) (x : X) (h : Set.range f ∈ nhds (f x)) :

Filter.map f (nhds x) = nhds (f x)

source

theorem Topology.IsInducing.mapClusterPt_iff {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : IsInducing f) {x : X} {l : Filter X} :

MapClusterPt (f x) l f ↔ ClusterPt x l

source

theorem Topology.IsInducing.image_mem_nhdsWithin {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : IsInducing f) {x : X} {s : Set X} (hs : s ∈ nhds x) :

f '' s ∈ nhdsWithin (f x) (Set.range f)

source

theorem Topology.IsInducing.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 : IsInducing g) :

Filter.Tendsto f l (nhds y) ↔ Filter.Tendsto (g ∘ f) l (nhds (g y))

source

theorem Topology.IsInducing.continuousAt_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace Y] [TopologicalSpace X] [TopologicalSpace Z] (hg : IsInducing g) {x : X} :

ContinuousAt f x ↔ ContinuousAt (g ∘ f) x

source

theorem Topology.IsInducing.continuous_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace Y] [TopologicalSpace X] [TopologicalSpace Z] (hg : IsInducing g) :

Continuous f ↔ Continuous (g ∘ f)

source

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

ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)

source

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

Continuous f

source

theorem Topology.IsInducing.closure_eq_preimage_closure_image {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : IsInducing f) (s : Set X) :

closure s = f ⁻¹' closure (f '' s)

source

theorem Topology.IsInducing.isClosed_iff {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : IsInducing f) {s : Set X} :

IsClosed s ↔ ∃ (t : Set Y), IsClosed t ∧ f ⁻¹' t = s

source

theorem Topology.IsInducing.isClosed_iff' {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : IsInducing f) {s : Set X} :

IsClosed s ↔ ∀ (x : X), f x ∈ closure (f '' s) → x ∈ s

source

theorem Topology.IsInducing.isClosed_preimage {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (h : IsInducing f) (s : Set Y) (hs : IsClosed s) :

IsClosed (f ⁻¹' s)

source

theorem Topology.IsInducing.isOpen_iff {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : IsInducing f) {s : Set X} :

IsOpen s ↔ ∃ (t : Set Y), IsOpen t ∧ f ⁻¹' t = s

source

theorem Topology.IsInducing.setOf_isOpen {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : IsInducing f) :

{s : Set X | IsOpen s} = Set.preimage f '' {t : Set Y | IsOpen t}

source

theorem Topology.IsInducing.dense_iff {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : IsInducing f) {s : Set X} :

Dense s ↔ ∀ (x : X), f x ∈ closure (f '' s)

source

theorem Topology.IsInducing.of_subsingleton {X : Type u_1} {Y : Type u_2} [TopologicalSpace Y] [TopologicalSpace X] [Subsingleton X] (f : X → Y) :

IsInducing f

source

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

IsEmbedding f

source

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

Topology.IsEmbedding f

Alias of Topology.IsEmbedding.induced.

source

@[deprecated Function.Injective.isEmbedding_induced (since := "2024-10-26")]

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

IsEmbedding f

Alias of Topology.IsEmbedding.induced.

source

theorem Topology.IsEmbedding.isInducing {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsEmbedding f) :

IsInducing f

source

@[deprecated Topology.IsEmbedding.isInducing (since := "2024-10-28")]

theorem Topology.IsEmbedding.inducing {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsEmbedding f) :

IsInducing f

Alias of Topology.IsEmbedding.isInducing.

source

theorem Topology.IsEmbedding.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) :

IsEmbedding f

source

@[deprecated Topology.IsEmbedding.mk' (since := "2024-10-26")]

theorem Topology.IsEmbedding.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) :

IsEmbedding f

Alias of Topology.IsEmbedding.mk'.

source

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

IsEmbedding id

source

@[deprecated Topology.IsEmbedding.id (since := "2024-10-26")]

theorem Topology.IsEmbedding.embedding_id {X : Type u_1} [TopologicalSpace X] :

IsEmbedding id

Alias of Topology.IsEmbedding.id.

source

theorem Topology.IsEmbedding.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 : IsEmbedding g) (hf : IsEmbedding f) :

IsEmbedding (g ∘ f)

source

@[deprecated Topology.IsEmbedding.comp (since := "2024-10-26")]

theorem Topology.IsEmbedding.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 : IsEmbedding g) (hf : IsEmbedding f) :

IsEmbedding (g ∘ f)

Alias of Topology.IsEmbedding.comp.

source

theorem Topology.IsEmbedding.of_comp_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 : IsEmbedding g) :

IsEmbedding (g ∘ f) ↔ IsEmbedding f

source

@[deprecated Topology.IsEmbedding.of_comp_iff (since := "2024-10-26")]

theorem Topology.IsEmbedding.Embedding.of_comp_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 : IsEmbedding g) :

IsEmbedding (g ∘ f) ↔ IsEmbedding f

Alias of Topology.IsEmbedding.of_comp_iff.

source

theorem Topology.IsEmbedding.of_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] (hf : Continuous f) (hg : Continuous g) (hgf : IsEmbedding (g ∘ f)) :

IsEmbedding f

source

@[deprecated Topology.IsEmbedding.of_comp (since := "2024-10-26")]

theorem Topology.IsEmbedding.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 : IsEmbedding (g ∘ f)) :

IsEmbedding f

Alias of Topology.IsEmbedding.of_comp.

source

theorem Topology.IsEmbedding.of_leftInverse {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) :

IsEmbedding g

source

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

Topology.IsEmbedding g

Alias of Topology.IsEmbedding.of_leftInverse.

source

@[deprecated Function.LeftInverse.isEmbedding (since := "2024-10-26")]

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

Topology.IsEmbedding g

Alias of Topology.IsEmbedding.of_leftInverse.

source

theorem Topology.IsEmbedding.map_nhds_eq {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsEmbedding f) (x : X) :

Filter.map f (nhds x) = nhdsWithin (f x) (Set.range f)

source

@[deprecated Topology.IsEmbedding.map_nhds_eq (since := "2024-10-26")]

theorem Topology.IsEmbedding.Embedding.map_nhds_eq {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsEmbedding f) (x : X) :

Filter.map f (nhds x) = nhdsWithin (f x) (Set.range f)

Alias of Topology.IsEmbedding.map_nhds_eq.

source

theorem Topology.IsEmbedding.map_nhds_of_mem {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsEmbedding f) (x : X) (h : Set.range f ∈ nhds (f x)) :

Filter.map f (nhds x) = nhds (f x)

source

@[deprecated Topology.IsEmbedding.map_nhds_of_mem (since := "2024-10-26")]

theorem Topology.IsEmbedding.Embedding.map_nhds_of_mem {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsEmbedding f) (x : X) (h : Set.range f ∈ nhds (f x)) :

Filter.map f (nhds x) = nhds (f x)

Alias of Topology.IsEmbedding.map_nhds_of_mem.

source

theorem Topology.IsEmbedding.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 : IsEmbedding g) :

Filter.Tendsto f l (nhds y) ↔ Filter.Tendsto (g ∘ f) l (nhds (g y))

source

theorem Topology.IsEmbedding.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 : IsEmbedding g) :

Continuous f ↔ Continuous (g ∘ f)

source

@[deprecated Topology.IsEmbedding.continuous_iff (since := "2024-10-26")]

theorem Topology.IsEmbedding.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 : IsEmbedding g) :

Continuous f ↔ Continuous (g ∘ f)

Alias of Topology.IsEmbedding.continuous_iff.

source

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

Continuous f

source

theorem Topology.IsEmbedding.closure_eq_preimage_closure_image {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsEmbedding f) (s : Set X) :

closure s = f ⁻¹' closure (f '' s)

source

@[deprecated Topology.IsEmbedding.closure_eq_preimage_closure_image (since := "2024-10-26")]

theorem Topology.IsEmbedding.Embedding.closure_eq_preimage_closure_image {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsEmbedding f) (s : Set X) :

closure s = f ⁻¹' closure (f '' s)

Alias of Topology.IsEmbedding.closure_eq_preimage_closure_image.

source

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

DiscreteTopology X

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

source

@[deprecated Topology.IsEmbedding.discreteTopology (since := "2024-10-26")]

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

DiscreteTopology X

Alias of Topology.IsEmbedding.discreteTopology.

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

source

theorem Topology.IsEmbedding.of_subsingleton {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [Subsingleton X] (f : X → Y) :

IsEmbedding f

source

@[deprecated Topology.IsEmbedding.of_subsingleton (since := "2024-10-26")]

theorem Topology.IsEmbedding.Embedding.of_subsingleton {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [Subsingleton X] (f : X → Y) :

IsEmbedding f

Alias of Topology.IsEmbedding.of_subsingleton.

source

theorem Topology.isQuotientMap_iff {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] :

IsQuotientMap f ↔ Function.Surjective f ∧ ∀ (s : Set Y), IsOpen s ↔ IsOpen (f ⁻¹' s)

source

@[deprecated Topology.isQuotientMap_iff (since := "2024-10-22")]

theorem Topology.quotientMap_iff {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] :

IsQuotientMap f ↔ Function.Surjective f ∧ ∀ (s : Set Y), IsOpen s ↔ IsOpen (f ⁻¹' s)

Alias of Topology.isQuotientMap_iff.

source

theorem Topology.isQuotientMap_iff_isClosed {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] :

IsQuotientMap f ↔ Function.Surjective f ∧ ∀ (s : Set Y), IsClosed s ↔ IsClosed (f ⁻¹' s)

source

@[deprecated Topology.isQuotientMap_iff_isClosed (since := "2024-10-22")]

theorem Topology.quotientMap_iff_closed {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] :

IsQuotientMap f ↔ Function.Surjective f ∧ ∀ (s : Set Y), IsClosed s ↔ IsClosed (f ⁻¹' s)

Alias of Topology.isQuotientMap_iff_isClosed.

source

@[deprecated Topology.isQuotientMap_iff_isClosed (since := "2024-11-19")]

theorem Topology.isQuotientMap_iff_closed {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] :

IsQuotientMap f ↔ Function.Surjective f ∧ ∀ (s : Set Y), IsClosed s ↔ IsClosed (f ⁻¹' s)

Alias of Topology.isQuotientMap_iff_isClosed.

source

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

IsQuotientMap id

source

theorem Topology.IsQuotientMap.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 : IsQuotientMap g) (hf : IsQuotientMap f) :

IsQuotientMap (g ∘ f)

source

theorem Topology.IsQuotientMap.of_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] (hf : Continuous f) (hg : Continuous g) (hgf : IsQuotientMap (g ∘ f)) :

IsQuotientMap g

source

@[deprecated Topology.IsQuotientMap.of_comp (since := "2024-10-22")]

theorem Topology.IsQuotientMap.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 : IsQuotientMap (g ∘ f)) :

IsQuotientMap g

Alias of Topology.IsQuotientMap.of_comp.

source

theorem Topology.IsQuotientMap.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) :

IsQuotientMap g

source

theorem Topology.IsQuotientMap.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 : IsQuotientMap f) :

Continuous g ↔ Continuous (g ∘ f)

source

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

Continuous f

source

theorem Topology.IsQuotientMap.isOpen_preimage {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsQuotientMap f) {s : Set Y} :

IsOpen (f ⁻¹' s) ↔ IsOpen s

source

theorem Topology.IsQuotientMap.isClosed_preimage {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsQuotientMap f) {s : Set Y} :

IsClosed (f ⁻¹' s) ↔ IsClosed s

source

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

IsOpenMap id

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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

source

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

source

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

source

theorem IsOpenMap.isQuotientMap {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) :

Topology.IsQuotientMap f

A continuous surjective open map is a quotient map.

source

@[deprecated IsOpenMap.isQuotientMap (since := "2024-10-22")]

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

Topology.IsQuotientMap f

Alias of IsOpenMap.isQuotientMap.

A continuous surjective open map is a quotient map.

source

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

source

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)

source

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)

source

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)

source

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)

source

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)

source

theorem IsOpenMap.of_isEmpty {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [h : IsEmpty X] (f : X → Y) :

IsOpenMap f

source

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)

source

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)

source

theorem Topology.IsInducing.isOpenMap {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hi : IsInducing f) (ho : IsOpen (Set.range f)) :

IsOpenMap f

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

source

@[deprecated Topology.IsInducing.isOpenMap (since := "2024-10-28")]

theorem Inducing.isOpenMap {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hi : Topology.IsInducing f) (ho : IsOpen (Set.range f)) :

IsOpenMap f

Alias of Topology.IsInducing.isOpenMap.

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

source

theorem Dense.preimage {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] {s : Set Y} (hs : Dense s) (hf : IsOpenMap f) :

Dense (f ⁻¹' s)

Preimage of a dense set under an open map is dense.

source

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

IsClosedMap id

source

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)

source

theorem IsClosedMap.of_comp_surjective {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 : Function.Surjective f) (hf' : Continuous f) (hfg : IsClosedMap (g ∘ f)) :

IsClosedMap g

source

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

source

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

source

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 → s.Nonempty → IsClosed (f '' s)) :

IsClosedMap f

source

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

IsClosed (Set.range f)

source

theorem IsClosedMap.isQuotientMap {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) :

Topology.IsQuotientMap f

source

@[deprecated IsClosedMap.isQuotientMap (since := "2024-10-22")]

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

Topology.IsQuotientMap f

Alias of IsClosedMap.isQuotientMap.

source

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

IsClosedMap f

source

@[deprecated Topology.IsInducing.isClosedMap (since := "2024-10-28")]

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

IsClosedMap f

Alias of Topology.IsInducing.isClosedMap.

source

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

source

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.

source

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

source

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.map f F).lift' closure = Filter.map f (F.lift' closure)

source

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 ↔ (F.lift' closure ⊓ Filter.principal (f ⁻¹' {y})).NeBot

source

theorem Topology.IsOpenEmbedding.isEmbedding {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenEmbedding f) :

IsEmbedding f

source

theorem Topology.IsOpenEmbedding.isInducing {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenEmbedding f) :

IsInducing f

source

@[deprecated Topology.IsOpenEmbedding.isInducing (since := "2024-10-28")]

theorem Topology.IsOpenEmbedding.inducing {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenEmbedding f) :

IsInducing f

Alias of Topology.IsOpenEmbedding.isInducing.

source

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

IsOpenMap f

source

@[deprecated Topology.IsOpenEmbedding.isOpenMap (since := "2024-10-18")]

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

IsOpenMap f

Alias of Topology.IsOpenEmbedding.isOpenMap.

source

theorem Topology.IsOpenEmbedding.map_nhds_eq {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenEmbedding f) (x : X) :

Filter.map f (nhds x) = nhds (f x)

source

@[deprecated Topology.IsOpenEmbedding.map_nhds_eq (since := "2024-10-18")]

theorem Topology.OpenEmbedding.map_nhds_eq {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenEmbedding f) (x : X) :

Filter.map f (nhds x) = nhds (f x)

Alias of Topology.IsOpenEmbedding.map_nhds_eq.

source

theorem Topology.IsOpenEmbedding.isOpen_iff_image_isOpen {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenEmbedding f) {s : Set X} :

IsOpen s ↔ IsOpen (f '' s)

source

@[deprecated Topology.IsOpenEmbedding.isOpen_iff_image_isOpen (since := "2024-10-30")]

theorem Topology.IsOpenEmbedding.open_iff_image_open {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenEmbedding f) {s : Set X} :

IsOpen s ↔ IsOpen (f '' s)

Alias of Topology.IsOpenEmbedding.isOpen_iff_image_isOpen.

source

@[deprecated Topology.IsOpenEmbedding.isOpen_iff_image_isOpen (since := "2024-10-18")]

theorem Topology.OpenEmbedding.open_iff_image_open {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenEmbedding f) {s : Set X} :

IsOpen s ↔ IsOpen (f '' s)

Alias of Topology.IsOpenEmbedding.isOpen_iff_image_isOpen.

source

theorem Topology.IsOpenEmbedding.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 : IsOpenEmbedding g) :

Filter.Tendsto f l (nhds y) ↔ Filter.Tendsto (g ∘ f) l (nhds (g y))

source

@[deprecated Topology.IsOpenEmbedding.tendsto_nhds_iff (since := "2024-10-18")]

theorem Topology.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 : IsOpenEmbedding g) :

Filter.Tendsto f l (nhds y) ↔ Filter.Tendsto (g ∘ f) l (nhds (g y))

Alias of Topology.IsOpenEmbedding.tendsto_nhds_iff.

source

theorem Topology.IsOpenEmbedding.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 : IsOpenEmbedding f) {l : Filter Z} {x : X} :

Filter.Tendsto (g ∘ f) (nhds x) l ↔ Filter.Tendsto g (nhds (f x)) l

source

@[deprecated Topology.IsOpenEmbedding.tendsto_nhds_iff' (since := "2024-10-18")]

theorem Topology.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 : IsOpenEmbedding f) {l : Filter Z} {x : X} :

Filter.Tendsto (g ∘ f) (nhds x) l ↔ Filter.Tendsto g (nhds (f x)) l

Alias of Topology.IsOpenEmbedding.tendsto_nhds_iff'.

source

theorem Topology.IsOpenEmbedding.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 : IsOpenEmbedding f) {x : X} :

ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)

source

@[deprecated Topology.IsOpenEmbedding.continuousAt_iff (since := "2024-10-18")]

theorem Topology.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 : IsOpenEmbedding f) {x : X} :

ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)

Alias of Topology.IsOpenEmbedding.continuousAt_iff.

source

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

Continuous f

source

@[deprecated Topology.IsOpenEmbedding.continuous (since := "2024-10-18")]

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

Continuous f

Alias of Topology.IsOpenEmbedding.continuous.

source

theorem Topology.IsOpenEmbedding.isOpen_iff_preimage_isOpen {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenEmbedding f) {s : Set Y} (hs : s ⊆ Set.range f) :

IsOpen s ↔ IsOpen (f ⁻¹' s)

source

@[deprecated Topology.IsOpenEmbedding.isOpen_iff_preimage_isOpen (since := "2024-10-30")]

theorem Topology.IsOpenEmbedding.open_iff_preimage_open {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenEmbedding f) {s : Set Y} (hs : s ⊆ Set.range f) :

IsOpen s ↔ IsOpen (f ⁻¹' s)

Alias of Topology.IsOpenEmbedding.isOpen_iff_preimage_isOpen.

source

@[deprecated Topology.IsOpenEmbedding.isOpen_iff_preimage_isOpen (since := "2024-10-18")]

theorem Topology.OpenEmbedding.open_iff_preimage_open {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenEmbedding f) {s : Set Y} (hs : s ⊆ Set.range f) :

IsOpen s ↔ IsOpen (f ⁻¹' s)

Alias of Topology.IsOpenEmbedding.isOpen_iff_preimage_isOpen.

source

theorem Topology.IsOpenEmbedding.of_isEmbedding_isOpenMap {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (h₁ : IsEmbedding f) (h₂ : IsOpenMap f) :

IsOpenEmbedding f

source

@[deprecated Topology.IsOpenEmbedding.of_isEmbedding_isOpenMap (since := "2024-10-26")]

theorem Topology.isOpenEmbedding_of_embedding_open {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (h₁ : IsEmbedding f) (h₂ : IsOpenMap f) :

IsOpenEmbedding f

Alias of Topology.IsOpenEmbedding.of_isEmbedding_isOpenMap.

source

@[deprecated Topology.IsOpenEmbedding.of_isEmbedding_isOpenMap (since := "2024-10-18")]

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

IsOpenEmbedding f

Alias of Topology.IsOpenEmbedding.of_isEmbedding_isOpenMap.

source

theorem Topology.IsEmbedding.isOpenEmbedding_of_surjective {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsEmbedding f) (hsurj : Function.Surjective f) :

IsOpenEmbedding f

A surjective embedding is an IsOpenEmbedding.

source

@[deprecated Topology.IsEmbedding.isOpenEmbedding_of_surjective (since := "2024-10-26")]

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

Topology.IsOpenEmbedding f

Alias of Topology.IsEmbedding.isOpenEmbedding_of_surjective.

A surjective embedding is an IsOpenEmbedding.

source

theorem Topology.IsOpenEmbedding.of_isEmbedding {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsEmbedding f) (hsurj : Function.Surjective f) :

IsOpenEmbedding f

Alias of Topology.IsEmbedding.isOpenEmbedding_of_surjective.

A surjective embedding is an IsOpenEmbedding.

source

@[deprecated Topology.IsEmbedding.isOpenEmbedding_of_surjective (since := "2024-10-18")]

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

Topology.IsOpenEmbedding f

Alias of Topology.IsEmbedding.isOpenEmbedding_of_surjective.

A surjective embedding is an IsOpenEmbedding.

source

theorem Topology.isOpenEmbedding_iff_isEmbedding_isOpenMap {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] :

IsOpenEmbedding f ↔ IsEmbedding f ∧ IsOpenMap f

source

@[deprecated Topology.isOpenEmbedding_iff_isEmbedding_isOpenMap (since := "2024-10-26")]

theorem Topology.isOpenEmbedding_iff_embedding_open {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] :

IsOpenEmbedding f ↔ IsEmbedding f ∧ IsOpenMap f

Alias of Topology.isOpenEmbedding_iff_isEmbedding_isOpenMap.

source

@[deprecated Topology.isOpenEmbedding_iff_isEmbedding_isOpenMap (since := "2024-10-18")]

theorem Topology.openEmbedding_iff_embedding_open {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] :

IsOpenEmbedding f ↔ IsEmbedding f ∧ IsOpenMap f

Alias of Topology.isOpenEmbedding_iff_isEmbedding_isOpenMap.

source

theorem Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap {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) :

IsOpenEmbedding f

source

theorem Topology.isOpenEmbedding_iff_continuous_injective_isOpenMap {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] :

IsOpenEmbedding f ↔ Continuous f ∧ Function.Injective f ∧ IsOpenMap f

source

@[deprecated Topology.isOpenEmbedding_iff_continuous_injective_isOpenMap (since := "2024-10-30")]

theorem Topology.isOpenEmbedding_iff_continuous_injective_open {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] :

IsOpenEmbedding f ↔ Continuous f ∧ Function.Injective f ∧ IsOpenMap f

Alias of Topology.isOpenEmbedding_iff_continuous_injective_isOpenMap.

source

@[deprecated Topology.isOpenEmbedding_iff_continuous_injective_isOpenMap (since := "2024-10-18")]

theorem Topology.openEmbedding_iff_continuous_injective_open {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] :

IsOpenEmbedding f ↔ Continuous f ∧ Function.Injective f ∧ IsOpenMap f

Alias of Topology.isOpenEmbedding_iff_continuous_injective_isOpenMap.

source

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

IsOpenEmbedding id

source

@[deprecated Topology.IsOpenEmbedding.id (since := "2024-10-18")]

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

Topology.IsOpenEmbedding id

Alias of Topology.IsOpenEmbedding.id.

source

theorem Topology.IsOpenEmbedding.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 : IsOpenEmbedding g) (hf : IsOpenEmbedding f) :

IsOpenEmbedding (g ∘ f)

source

theorem Topology.IsOpenEmbedding.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 : IsOpenEmbedding g) :

IsOpenMap f ↔ IsOpenMap (g ∘ f)

source

theorem Topology.IsOpenEmbedding.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 : IsOpenEmbedding g) :

IsOpenEmbedding (g ∘ f) ↔ IsOpenEmbedding f

source

theorem Topology.IsOpenEmbedding.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 : IsOpenEmbedding g) (h : IsOpenEmbedding (g ∘ f)) :

IsOpenEmbedding f

source

theorem Topology.IsOpenEmbedding.of_isEmpty {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [IsEmpty X] (f : X → Y) :

IsOpenEmbedding f

source

theorem Topology.IsOpenEmbedding.image_mem_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsOpenEmbedding f) {s : Set X} {x : X} :

f '' s ∈ nhds (f x) ↔ s ∈ nhds x

source

theorem Topology.IsClosedEmbedding.isEmbedding {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsClosedEmbedding f) :

IsEmbedding f

source

theorem Topology.IsClosedEmbedding.isInducing {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsClosedEmbedding f) :

IsInducing f

source

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

Continuous f

source

@[deprecated Topology.IsClosedEmbedding.isInducing (since := "2024-10-28")]

theorem Topology.IsClosedEmbedding.inducing {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsClosedEmbedding f) :

IsInducing f

Alias of Topology.IsClosedEmbedding.isInducing.

source

theorem Topology.IsClosedEmbedding.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 : IsClosedEmbedding f) :

Filter.Tendsto g l (nhds x) ↔ Filter.Tendsto (f ∘ g) l (nhds (f x))

source

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

IsClosedMap f

source

theorem Topology.IsClosedEmbedding.isClosed_iff_image_isClosed {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsClosedEmbedding f) {s : Set X} :

IsClosed s ↔ IsClosed (f '' s)

source

@[deprecated Topology.IsClosedEmbedding.isClosed_iff_image_isClosed (since := "2024-10-30")]

theorem Topology.IsClosedEmbedding.closed_iff_image_closed {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsClosedEmbedding f) {s : Set X} :

IsClosed s ↔ IsClosed (f '' s)

Alias of Topology.IsClosedEmbedding.isClosed_iff_image_isClosed.

source

theorem Topology.IsClosedEmbedding.isClosed_iff_preimage_isClosed {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsClosedEmbedding f) {s : Set Y} (hs : s ⊆ Set.range f) :

IsClosed s ↔ IsClosed (f ⁻¹' s)

source

@[deprecated Topology.IsClosedEmbedding.isClosed_iff_preimage_isClosed (since := "2024-10-30")]

theorem Topology.IsClosedEmbedding.closed_iff_preimage_closed {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsClosedEmbedding f) {s : Set Y} (hs : s ⊆ Set.range f) :

IsClosed s ↔ IsClosed (f ⁻¹' s)

Alias of Topology.IsClosedEmbedding.isClosed_iff_preimage_isClosed.

source

theorem Topology.IsClosedEmbedding.of_isEmbedding_isClosedMap {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (h₁ : IsEmbedding f) (h₂ : IsClosedMap f) :

IsClosedEmbedding f

source

@[deprecated Topology.IsClosedEmbedding.of_isEmbedding_isClosedMap (since := "2024-10-26")]

theorem IsClosedEmbedding.of_embedding_closed {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (h₁ : Topology.IsEmbedding f) (h₂ : IsClosedMap f) :

Topology.IsClosedEmbedding f

Alias of Topology.IsClosedEmbedding.of_isEmbedding_isClosedMap.

source

@[deprecated Topology.IsClosedEmbedding.of_isEmbedding_isClosedMap (since := "2024-10-20")]

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

Topology.IsClosedEmbedding f

Alias of Topology.IsClosedEmbedding.of_isEmbedding_isClosedMap.

source

theorem Topology.IsClosedEmbedding.of_continuous_injective_isClosedMap {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) :

IsClosedEmbedding f

source

@[deprecated Topology.IsClosedEmbedding.of_continuous_injective_isClosedMap (since := "2024-10-20")]

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

Topology.IsClosedEmbedding f

Alias of Topology.IsClosedEmbedding.of_continuous_injective_isClosedMap.

source

theorem Topology.IsClosedEmbedding.isClosedEmbedding_iff_continuous_injective_isClosedMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} :

IsClosedEmbedding f ↔ Continuous f ∧ Function.Injective f ∧ IsClosedMap f

source

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

IsClosedEmbedding id

source

@[deprecated Topology.IsClosedEmbedding.id (since := "2024-10-20")]

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

Topology.IsClosedEmbedding id

Alias of Topology.IsClosedEmbedding.id.

source

theorem Topology.IsClosedEmbedding.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 : IsClosedEmbedding g) (hf : IsClosedEmbedding f) :

IsClosedEmbedding (g ∘ f)

source

theorem Topology.IsClosedEmbedding.of_comp_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 : IsClosedEmbedding g) :

IsClosedEmbedding (g ∘ f) ↔ IsClosedEmbedding f

source

@[deprecated Topology.IsClosedEmbedding.of_comp_iff (since := "2024-10-26")]

theorem Topology.IsClosedEmbedding.Embedding.of_comp_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 : IsClosedEmbedding g) :

IsClosedEmbedding (g ∘ f) ↔ IsClosedEmbedding f

Alias of Topology.IsClosedEmbedding.of_comp_iff.

source

theorem Topology.IsClosedEmbedding.closure_image_eq {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsClosedEmbedding f) (s : Set X) :

closure (f '' s) = f '' closure s

Documentation

Mathlib.Topology.Maps.Basic

Specific classes of maps between topological spaces #

References #

Tags #