Mathlib.Topology.Maps.Basic

Topology.IsInducing.induced theorem

(f : X → Y) : @IsInducing X Y (induced f ‹_›) _ f

Full source

protected lemma IsInducing.induced (f : X → Y) : @IsInducing X Y (induced f ‹_›) _ f :=
  @IsInducing.mk _ _ (TopologicalSpace.induced f ‹_›) _ _ rfl

Inducing Property of the Induced Topology

Informal description

For any function $f: X \to Y$ between topological spaces, the topology on $X$ induced by $f$ from the topology on $Y$ makes $f$ an inducing map.

Topology.IsInducing.id theorem

: IsInducing (@id X)

Full source

protected lemma IsInducing.id : IsInducing (@id X) := ⟨induced_id.symm⟩

Identity Map is Inducing

Informal description

The identity map $\mathrm{id} \colon X \to X$ on a topological space $X$ is inducing, meaning the topology on $X$ is the same as the topology induced by $\mathrm{id}$ from the topology on $X$.

Topology.IsInducing.comp theorem

(hg : IsInducing g) (hf : IsInducing f) : IsInducing (g ∘ f)

Full source

protected lemma IsInducing.comp (hg : IsInducing g) (hf : IsInducing f) :
    IsInducing (g ∘ f) :=
  ⟨by rw [hf.eq_induced, hg.eq_induced, induced_compose]⟩

Composition of Inducing Maps is Inducing

Informal description

Let $f \colon X \to Y$ and $g \colon Y \to Z$ be maps between topological spaces. If $f$ and $g$ are both inducing maps, then their composition $g \circ f \colon X \to Z$ is also an inducing map.

Topology.IsInducing.of_comp_iff theorem

(hg : IsInducing g) : IsInducing (g ∘ f) ↔ IsInducing f

Full source

lemma IsInducing.of_comp_iff (hg : IsInducing g) : IsInducingIsInducing (g ∘ f) ↔ IsInducing f := by
  refine ⟨fun h ↦ ?_, hg.comp⟩
  rw [isInducing_iff, hg.eq_induced, induced_compose, h.eq_induced]

Inducing Property of Composition via Inducing Second Map

Informal description

Let $f \colon X \to Y$ and $g \colon Y \to Z$ be maps between topological spaces, with $g$ being an inducing map. Then the composition $g \circ f \colon X \to Z$ is an inducing map if and only if $f$ is an inducing map.

Topology.IsInducing.of_comp theorem

(hf : Continuous f) (hg : Continuous g) (hgf : IsInducing (g ∘ f)) : IsInducing f

Full source

lemma IsInducing.of_comp (hf : Continuous f) (hg : Continuous g) (hgf : IsInducing (g ∘ f)) :
    IsInducing f :=
  ⟨le_antisymm (by rwa [← continuous_iff_le_induced])
      (by
        rw [hgf.eq_induced, ← induced_compose]
        exact induced_mono hg.le_induced)⟩

Inducing Property via Composition of Continuous Maps

Informal description

Let $f \colon X \to Y$ and $g \colon Y \to Z$ be continuous maps between topological spaces. If the composition $g \circ f \colon X \to Z$ is inducing, then $f$ is inducing.

Topology.isInducing_iff_nhds theorem

: IsInducing f ↔ ∀ x, 𝓝 x = comap f (𝓝 (f x))

Full source

lemma isInducing_iff_nhds : IsInducingIsInducing f ↔ ∀ x, 𝓝 x = comap f (𝓝 (f x)) :=
  (isInducing_iff _).trans (induced_iff_nhds_eq f)

Characterization of Inducing Maps via Neighborhood Filters

Informal description

A map $f \colon X \to Y$ between topological spaces is inducing if and only if for every point $x \in X$, the neighborhood filter $\mathcal{N}_x$ of $x$ in $X$ is equal to the preimage under $f$ of the neighborhood filter $\mathcal{N}_{f(x)}$ of $f(x)$ in $Y$, i.e., $\mathcal{N}_x = f^{-1}(\mathcal{N}_{f(x)})$.

Topology.IsInducing.nhds_eq_comap theorem

(hf : IsInducing f) : ∀ x : X, 𝓝 x = comap f (𝓝 <| f x)

Full source

lemma nhds_eq_comap (hf : IsInducing f) : ∀ x : X, 𝓝 x = comap f (𝓝 <| f x) :=
  isInducing_iff_nhds.1 hf

Neighborhood Filter Characterization for Inducing Maps

Informal description

If a map $f \colon X \to Y$ between topological spaces is inducing, then for every point $x \in X$, the neighborhood filter $\mathcal{N}_x$ of $x$ in $X$ is equal to the preimage under $f$ of the neighborhood filter $\mathcal{N}_{f(x)}$ of $f(x)$ in $Y$, i.e., $\mathcal{N}_x = f^{-1}(\mathcal{N}_{f(x)})$.

Topology.IsInducing.basis_nhds theorem

 {p : ι → Prop} {s : ι → Set Y} (hf : IsInducing f) {x : X} (h_basis : (𝓝 (f x)).HasBasis p s) :
  (𝓝 x).HasBasis p (preimage f ∘ s)

Full source

lemma basis_nhds {p : ι → Prop} {s : ι → Set Y} (hf : IsInducing f) {x : X}
    (h_basis : (𝓝 (f x)).HasBasis p s) : (𝓝 x).HasBasis p (preimagepreimage f ∘ s) :=
  hf.nhds_eq_comap x ▸ h_basis.comap f

Basis Characterization of Neighborhood Filters under Inducing Maps

Informal description

Let $f \colon X \to Y$ be an inducing map between topological spaces. Suppose that for a point $x \in X$, the neighborhood filter $\mathcal{N}_{f(x)}$ of $f(x)$ in $Y$ has a basis consisting of sets $\{s_i\}_{i \in I}$ indexed by some type $I$, where each $s_i$ is a subset of $Y$ and $p(i)$ is a predicate on $I$ determining whether $s_i$ is included in the basis. Then, the neighborhood filter $\mathcal{N}_x$ of $x$ in $X$ has a basis consisting of the preimages $f^{-1}(s_i)$ for those $i \in I$ satisfying $p(i)$. In other words, if $\{s_i\}_{p(i)}$ forms a basis for $\mathcal{N}_{f(x)}$, then $\{f^{-1}(s_i)\}_{p(i)}$ forms a basis for $\mathcal{N}_x$.

Topology.IsInducing.nhdsSet_eq_comap theorem

(hf : IsInducing f) (s : Set X) : 𝓝ˢ s = comap f (𝓝ˢ (f '' s))

Full source

lemma nhdsSet_eq_comap (hf : IsInducing f) (s : Set X) :
    𝓝ˢ s = comap f (𝓝ˢ (f '' s)) := by
  simp only [nhdsSet, sSup_image, comap_iSup, hf.nhds_eq_comap, iSup_image]

Neighborhood Filter of Subset under Inducing Map Equals Preimage of Neighborhood Filter of Image

Informal description

Let $f \colon X \to Y$ be an inducing map between topological spaces. For any subset $s \subseteq X$, the neighborhood filter $\mathcal{N}_s$ of $s$ in $X$ is equal to the preimage under $f$ of the neighborhood filter $\mathcal{N}_{f(s)}$ of the image $f(s)$ in $Y$, i.e., $$\mathcal{N}_s = f^{-1}(\mathcal{N}_{f(s)}).$$

Topology.IsInducing.map_nhds_eq theorem

(hf : IsInducing f) (x : X) : (𝓝 x).map f = 𝓝[range f] f x

Full source

lemma map_nhds_eq (hf : IsInducing f) (x : X) : (𝓝 x).map f = 𝓝[range f] f x :=
  hf.eq_induced ▸ map_nhds_induced_eq x

Pushforward of Neighborhood Filter under Inducing Map Equals Restricted Neighborhood Filter

Informal description

Let $f : X \to Y$ be an inducing map between topological spaces. For any point $x \in X$, the pushforward of the neighborhood filter of $x$ under $f$ equals the neighborhood filter of $f(x)$ restricted to the range of $f$. In other words: $$\text{map}_f(\mathcal{N}_x) = \mathcal{N}_{f(x)}|_{\text{range}(f)}$$ where $\mathcal{N}_x$ denotes the neighborhood filter at $x$ and $\text{map}_f$ denotes the pushforward filter.

Topology.IsInducing.map_nhds_of_mem theorem

(hf : IsInducing f) (x : X) (h : range f ∈ 𝓝 (f x)) : (𝓝 x).map f = 𝓝 (f x)

Full source

lemma map_nhds_of_mem (hf : IsInducing f) (x : X) (h : rangerange f ∈ 𝓝 (f x)) :
    (𝓝 x).map f = 𝓝 (f x) := hf.eq_induced ▸ map_nhds_induced_of_mem h

Neighborhood Filter Preservation for Inducing Maps

Informal description

Let $f : X \to Y$ be an inducing map between topological spaces, and let $x \in X$. If the range of $f$ is a neighborhood of $f(x)$ in $Y$, then the pushforward of the neighborhood filter at $x$ under $f$ equals the neighborhood filter at $f(x)$. In other words, $\text{map}\, f\, (\mathcal{N}_x) = \mathcal{N}_{f(x)}$.

Topology.IsInducing.mapClusterPt_iff theorem

(hf : IsInducing f) {x : X} {l : Filter X} : MapClusterPt (f x) l f ↔ ClusterPt x l

Full source

lemma mapClusterPt_iff (hf : IsInducing f) {x : X} {l : Filter X} :
    MapClusterPtMapClusterPt (f x) l f ↔ ClusterPt x l := by
  delta MapClusterPt ClusterPt
  rw [← Filter.push_pull', ← hf.nhds_eq_comap, map_neBot_iff]

Cluster Point Characterization for Inducing Maps

Informal description

Let $f \colon X \to Y$ be an inducing map between topological spaces. For any point $x \in X$ and any filter $l$ on $X$, the point $f(x)$ is a cluster point of $l$ under $f$ if and only if $x$ is a cluster point of $l$. In other words, $f(x)$ is a cluster point of the pushforward filter $f_* l$ if and only if $x$ is a cluster point of $l$.

Topology.IsInducing.image_mem_nhdsWithin theorem

(hf : IsInducing f) {x : X} {s : Set X} (hs : s ∈ 𝓝 x) : f '' s ∈ 𝓝[range f] f x

Full source

lemma image_mem_nhdsWithin (hf : IsInducing f) {x : X} {s : Set X} (hs : s ∈ 𝓝 x) :
    f '' sf '' s ∈ 𝓝[range f] f x :=
  hf.map_nhds_eq x ▸ image_mem_map hs

Image of Neighborhood under Inducing Map is Restricted Neighborhood

Informal description

Let $f : X \to Y$ be an inducing map between topological spaces. For any point $x \in X$ and any set $s \subseteq X$ that is a neighborhood of $x$, the image $f(s)$ is a neighborhood of $f(x)$ in $Y$ restricted to the range of $f$. In other words, $f(s) \in \mathcal{N}_{f(x)}|_{\text{range}(f)}$.

Topology.IsInducing.tendsto_nhds_iff theorem

{f : ι → Y} {l : Filter ι} {y : Y} (hg : IsInducing g) : Tendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y))

Full source

lemma tendsto_nhds_iff {f : ι → Y} {l : Filter ι} {y : Y} (hg : IsInducing g) :
    TendstoTendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y)) := by
  rw [hg.nhds_eq_comap, tendsto_comap_iff]

Characterization of Limits via Inducing Maps

Informal description

Let $g : X \to Y$ be an inducing map between topological spaces. For any function $f : \iota \to Y$, filter $l$ on $\iota$, and point $y \in Y$, the function $f$ tends to $y$ along $l$ if and only if the composition $g \circ f$ tends to $g(y)$ along $l$. In other words, $\lim_{l} f = y$ if and only if $\lim_{l} (g \circ f) = g(y)$.

Topology.IsInducing.continuousAt_iff theorem

(hg : IsInducing g) {x : X} : ContinuousAt f x ↔ ContinuousAt (g ∘ f) x

Full source

lemma continuousAt_iff (hg : IsInducing g) {x : X} :
    ContinuousAtContinuousAt f x ↔ ContinuousAt (g ∘ f) x :=
  hg.tendsto_nhds_iff

Continuity at a Point via Inducing Maps

Informal description

Let $g : X \to Y$ be an inducing map between topological spaces. For any function $f : X \to Z$ and point $x \in X$, $f$ is continuous at $x$ if and only if the composition $g \circ f$ is continuous at $x$.

Topology.IsInducing.continuous_iff theorem

(hg : IsInducing g) : Continuous f ↔ Continuous (g ∘ f)

Full source

lemma continuous_iff (hg : IsInducing g) :
    ContinuousContinuous f ↔ Continuous (g ∘ f) := by
  simp_rw [continuous_iff_continuousAt, hg.continuousAt_iff]

Continuity Characterization via Inducing Maps

Informal description

Let $g : X \to Y$ be an inducing map between topological spaces. A function $f : X \to Z$ is continuous if and only if the composition $g \circ f$ is continuous.

Topology.IsInducing.continuousAt_iff' theorem

(hf : IsInducing f) {x : X} (h : range f ∈ 𝓝 (f x)) : ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)

Full source

lemma continuousAt_iff' (hf : IsInducing f) {x : X} (h : rangerange f ∈ 𝓝 (f x)) :
    ContinuousAtContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x) := by
  simp_rw [ContinuousAt, Filter.Tendsto, ← hf.map_nhds_of_mem _ h, Filter.map_map, comp]

Continuity of Composition via Inducing Map at a Point

Informal description

Let $f : X \to Y$ be an inducing map between topological spaces, and let $x \in X$ such that the range of $f$ is a neighborhood of $f(x)$ in $Y$. Then, for any function $g : Y \to Z$, the composition $g \circ f$ is continuous at $x$ if and only if $g$ is continuous at $f(x)$.

Topology.IsInducing.continuous theorem

(hf : IsInducing f) : Continuous f

Full source

protected lemma continuous (hf : IsInducing f) : Continuous f :=
  hf.continuous_iff.mp continuous_id

Continuity of Inducing Maps

Informal description

If $f : X \to Y$ is an inducing map between topological spaces, then $f$ is continuous.

Topology.IsInducing.closure_eq_preimage_closure_image theorem

(hf : IsInducing f) (s : Set X) : closure s = f ⁻¹' closure (f '' s)

Full source

lemma closure_eq_preimage_closure_image (hf : IsInducing f) (s : Set X) :
    closure s = f ⁻¹' closure (f '' s) := by
  ext x
  rw [Set.mem_preimage, ← closure_induced, hf.eq_induced]

Closure of Subset under Inducing Map Equals Preimage of Closure of Image

Informal description

Let $f : X \to Y$ be an inducing map between topological spaces. For any subset $s \subseteq X$, the closure of $s$ in $X$ equals the preimage under $f$ of the closure of $f(s)$ in $Y$, i.e., $$\overline{s} = f^{-1}(\overline{f(s)}).$$

Topology.IsInducing.isClosed_iff theorem

(hf : IsInducing f) {s : Set X} : IsClosed s ↔ ∃ t, IsClosed t ∧ f ⁻¹' t = s

Full source

theorem isClosed_iff (hf : IsInducing f) {s : Set X} :
    IsClosedIsClosed s ↔ ∃ t, IsClosed t ∧ f ⁻¹' t = s := by rw [hf.eq_induced, isClosed_induced_iff]

Characterization of Closed Sets via Inducing Maps

Informal description

Let $f : X \to Y$ be a map between topological spaces that is inducing (i.e., the topology on $X$ is induced by $f$ from the topology on $Y$). Then a subset $s \subseteq X$ is closed if and only if there exists a closed subset $t \subseteq Y$ such that $s$ is the preimage of $t$ under $f$, i.e., $s = f^{-1}(t)$.

Topology.IsInducing.isClosed_iff' theorem

(hf : IsInducing f) {s : Set X} : IsClosed s ↔ ∀ x, f x ∈ closure (f '' s) → x ∈ s

Full source

theorem isClosed_iff' (hf : IsInducing f) {s : Set X} :
    IsClosedIsClosed s ↔ ∀ x, f x ∈ closure (f '' s) → x ∈ s := by rw [hf.eq_induced, isClosed_induced_iff']

Characterization of Closed Sets via Inducing Maps

Informal description

Let $f : X \to Y$ be an inducing map between topological spaces. A subset $s \subseteq X$ is closed if and only if for every $x \in X$, if $f(x)$ belongs to the closure of the image $f(s)$, then $x$ belongs to $s$.

Topology.IsInducing.isClosed_preimage theorem

(h : IsInducing f) (s : Set Y) (hs : IsClosed s) : IsClosed (f ⁻¹' s)

Full source

theorem isClosed_preimage (h : IsInducing f) (s : Set Y) (hs : IsClosed s) :
    IsClosed (f ⁻¹' s) :=
  (isClosed_iff h).mpr ⟨s, hs, rfl⟩

Preimage of Closed Set under Inducing Map is Closed

Informal description

Let $f : X \to Y$ be an inducing map between topological spaces. For any closed subset $s \subseteq Y$, the preimage $f^{-1}(s)$ is closed in $X$.

Topology.IsInducing.isOpen_iff theorem

(hf : IsInducing f) {s : Set X} : IsOpen s ↔ ∃ t, IsOpen t ∧ f ⁻¹' t = s

Full source

theorem isOpen_iff (hf : IsInducing f) {s : Set X} :
    IsOpenIsOpen s ↔ ∃ t, IsOpen t ∧ f ⁻¹' t = s := by rw [hf.eq_induced, isOpen_induced_iff]

Characterization of Open Sets via Inducing Maps

Informal description

Let $f : X \to Y$ be a map between topological spaces that is inducing. Then a subset $s \subseteq X$ is open if and only if there exists an open subset $t \subseteq Y$ such that the preimage $f^{-1}(t)$ equals $s$.

Topology.IsInducing.setOf_isOpen theorem

(hf : IsInducing f) : {s : Set X | IsOpen s} = preimage f '' {t | IsOpen t}

Full source

theorem setOf_isOpen (hf : IsInducing f) :
    {s : Set X | IsOpen s} = preimagepreimage f '' {t | IsOpen t} :=
  Set.ext fun _ ↦ hf.isOpen_iff

Open Sets as Preimages of Open Sets under Inducing Maps

Informal description

Let $f \colon X \to Y$ be an inducing map between topological spaces. Then the collection of open sets in $X$ is precisely the preimage under $f$ of the collection of open sets in $Y$, i.e., \[ \{s \subseteq X \mid s \text{ is open}\} = f^{-1}''\{t \subseteq Y \mid t \text{ is open}\}. \]

Topology.IsInducing.dense_iff theorem

(hf : IsInducing f) {s : Set X} : Dense s ↔ ∀ x, f x ∈ closure (f '' s)

Full source

theorem dense_iff (hf : IsInducing f) {s : Set X} :
    DenseDense s ↔ ∀ x, f x ∈ closure (f '' s) := by
  simp only [Dense, hf.closure_eq_preimage_closure_image, mem_preimage]

Density Characterization via Inducing Maps

Informal description

Let $f \colon X \to Y$ be an inducing map between topological spaces. A subset $s \subseteq X$ is dense in $X$ if and only if for every $x \in X$, the image $f(x)$ belongs to the closure of $f(s)$ in $Y$.

Topology.IsInducing.of_subsingleton theorem

[Subsingleton X] (f : X → Y) : IsInducing f

Full source

theorem of_subsingleton [Subsingleton X] (f : X → Y) : IsInducing f :=
  ⟨Subsingleton.elim _ _⟩

Inducing Topology for Maps from Subsingleton Spaces

Informal description

If $X$ is a subsingleton topological space (i.e., has at most one point), then any map $f \colon X \to Y$ to another topological space $Y$ is inducing. That is, the topology on $X$ is the one induced via $f$ from the topology on $Y$.

Topology.IsEmbedding.induced theorem

[t : TopologicalSpace Y] (hf : Injective f) : @IsEmbedding X Y (t.induced f) t f

Full source

lemma induced [t : TopologicalSpace Y] (hf : Injective f) :
    @IsEmbedding X Y (t.induced f) t f :=
  @IsEmbedding.mk X Y (t.induced f) t _ (.induced f) hf

Induced Topology Makes Injective Map an Embedding

Informal description

Let $X$ and $Y$ be topological spaces, with $Y$ equipped with topology $t$. For any injective function $f : X \to Y$, the topology induced on $X$ by $f$ from $t$ makes $f$ an embedding. That is, $f$ becomes a homeomorphism onto its image when $X$ is given the induced topology.

Topology.IsEmbedding.isInducing theorem

(hf : IsEmbedding f) : IsInducing f

Full source

lemma isInducing (hf : IsEmbedding f) : IsInducing f := hf.toIsInducing

Embedding Implies Inducing Topology

Informal description

If a map $f \colon X \to Y$ between topological spaces is an embedding, then it is also inducing. That is, the topology on $X$ is the one induced via $f$ from the topology on $Y$.

Topology.IsEmbedding.mk' theorem

(f : X → Y) (inj : Injective f) (induced : ∀ x, comap f (𝓝 (f x)) = 𝓝 x) : IsEmbedding f

Full source

lemma mk' (f : X → Y) (inj : Injective f) (induced : ∀ x, comap f (𝓝 (f x)) = 𝓝 x) :
    IsEmbedding f :=
  ⟨isInducing_iff_nhds.2 fun x => (induced x).symm, inj⟩

Characterization of Topological Embeddings via Injectivity and Neighborhood Filters

Informal description

A map $f \colon X \to Y$ between topological spaces is an embedding if and only if it is injective and for every point $x \in X$, the neighborhood filter $\mathcal{N}_x$ of $x$ in $X$ is equal to the preimage under $f$ of the neighborhood filter $\mathcal{N}_{f(x)}$ of $f(x)$ in $Y$, i.e., $\mathcal{N}_x = f^{-1}(\mathcal{N}_{f(x)})$.

Topology.IsEmbedding.id theorem

: IsEmbedding (@id X)

Full source

protected lemma id : IsEmbedding (@id X) := ⟨.id, fun _ _ h => h⟩

Identity Map is an Embedding

Informal description

The identity map $\mathrm{id} \colon X \to X$ on a topological space $X$ is an embedding. That is, it is injective and the topology on $X$ is the one induced via $\mathrm{id}$ from the topology on $X$.

Topology.IsEmbedding.comp theorem

(hg : IsEmbedding g) (hf : IsEmbedding f) : IsEmbedding (g ∘ f)

Full source

protected lemma comp (hg : IsEmbedding g) (hf : IsEmbedding f) : IsEmbedding (g ∘ f) :=
  { hg.isInducing.comp hf.isInducing with injective := fun _ _ h => hf.injective <| hg.injective h }

Composition of Topological Embeddings is an Embedding

Informal description

If $f \colon X \to Y$ and $g \colon Y \to Z$ are topological embeddings, then their composition $g \circ f \colon X \to Z$ is also a topological embedding.

Topology.IsEmbedding.of_comp_iff theorem

(hg : IsEmbedding g) : IsEmbedding (g ∘ f) ↔ IsEmbedding f

Full source

lemma of_comp_iff (hg : IsEmbedding g) : IsEmbeddingIsEmbedding (g ∘ f) ↔ IsEmbedding f := by
  simp_rw [isEmbedding_iff, hg.isInducing.of_comp_iff, hg.injective.of_comp_iff f]

Embedding Property of Composition via Embedding Second Map

Informal description

Let $f \colon X \to Y$ and $g \colon Y \to Z$ be maps between topological spaces, with $g$ being an embedding. Then the composition $g \circ f \colon X \to Z$ is an embedding if and only if $f$ is an embedding.

Topology.IsEmbedding.of_comp theorem

(hf : Continuous f) (hg : Continuous g) (hgf : IsEmbedding (g ∘ f)) : IsEmbedding f

Full source

protected lemma of_comp (hf : Continuous f) (hg : Continuous g) (hgf : IsEmbedding (g ∘ f)) :
    IsEmbedding f where
  toIsInducing := hgf.isInducing.of_comp hf hg
  injective := hgf.injective.of_comp

Embedding Property via Composition of Continuous Maps

Informal description

Let $f \colon X \to Y$ and $g \colon Y \to Z$ be continuous maps between topological spaces. If the composition $g \circ f \colon X \to Z$ is an embedding, then $f$ is an embedding.

Topology.IsEmbedding.of_leftInverse theorem

{f : X → Y} {g : Y → X} (h : LeftInverse f g) (hf : Continuous f) (hg : Continuous g) : IsEmbedding g

Full source

lemma of_leftInverse {f : X → Y} {g : Y → X} (h : LeftInverse f g) (hf : Continuous f)
    (hg : Continuous g) : IsEmbedding g := .of_comp hg hf <| h.comp_eq_id.symm ▸ .id

Left Inverse of Continuous Map is Embedding

Informal description

Let $f \colon X \to Y$ and $g \colon Y \to X$ be continuous maps between topological spaces. If $f$ is a left inverse of $g$ (i.e., $f \circ g = \text{id}_Y$), then $g$ is an embedding.

Topology.IsEmbedding.map_nhds_eq theorem

(hf : IsEmbedding f) (x : X) : (𝓝 x).map f = 𝓝[range f] f x

Full source

lemma map_nhds_eq (hf : IsEmbedding f) (x : X) :     (𝓝 x).map f = 𝓝[range f] f x :=
  hf.1.map_nhds_eq x

Pushforward of Neighborhood Filter under Embedding Equals Restricted Neighborhood Filter

Informal description

Let $f : X \to Y$ be an embedding between topological spaces. For any point $x \in X$, the pushforward of the neighborhood filter of $x$ under $f$ equals the neighborhood filter of $f(x)$ restricted to the range of $f$. In other words: $$\text{map}_f(\mathcal{N}_x) = \mathcal{N}_{f(x)}|_{\text{range}(f)}$$ where $\mathcal{N}_x$ denotes the neighborhood filter at $x$ and $\text{map}_f$ denotes the pushforward filter.

Topology.IsEmbedding.map_nhds_of_mem theorem

(hf : IsEmbedding f) (x : X) (h : range f ∈ 𝓝 (f x)) : (𝓝 x).map f = 𝓝 (f x)

Full source

lemma map_nhds_of_mem (hf : IsEmbedding f) (x : X) (h : rangerange f ∈ 𝓝 (f x)) :
    (𝓝 x).map f = 𝓝 (f x) :=
  hf.1.map_nhds_of_mem x h

Neighborhood Filter Preservation for Embeddings with Local Range Condition

Informal description

Let $f : X \to Y$ be an embedding between topological spaces, and let $x \in X$. If the range of $f$ is a neighborhood of $f(x)$ in $Y$, then the pushforward of the neighborhood filter at $x$ under $f$ equals the neighborhood filter at $f(x)$. In other words, $\text{map}\, f\, (\mathcal{N}_x) = \mathcal{N}_{f(x)}$.

Topology.IsEmbedding.tendsto_nhds_iff theorem

{f : ι → Y} {l : Filter ι} {y : Y} (hg : IsEmbedding g) : Tendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y))

Full source

lemma tendsto_nhds_iff {f : ι → Y} {l : Filter ι} {y : Y} (hg : IsEmbedding g) :
    TendstoTendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y)) := hg.isInducing.tendsto_nhds_iff

Limit Characterization via Embeddings

Informal description

Let $g : X \to Y$ be an embedding between topological spaces. For any function $f : \iota \to Y$, filter $l$ on $\iota$, and point $y \in Y$, the function $f$ tends to $y$ along $l$ if and only if the composition $g \circ f$ tends to $g(y)$ along $l$. In other words: $$\lim_{l} f = y \iff \lim_{l} (g \circ f) = g(y).$$

Topology.IsEmbedding.continuous_iff theorem

(hg : IsEmbedding g) : Continuous f ↔ Continuous (g ∘ f)

Full source

lemma continuous_iff (hg : IsEmbedding g) : ContinuousContinuous f ↔ Continuous (g ∘ f) :=
  hg.isInducing.continuous_iff

Continuity Characterization via Embeddings

Informal description

Let $g \colon X \to Y$ be an embedding between topological spaces. A function $f \colon Z \to X$ is continuous if and only if the composition $g \circ f \colon Z \to Y$ is continuous.

Topology.IsEmbedding.continuous theorem

(hf : IsEmbedding f) : Continuous f

Full source

lemma continuous (hf : IsEmbedding f) : Continuous f := hf.isInducing.continuous

Continuity of Topological Embeddings

Informal description

If $f \colon X \to Y$ is an embedding between topological spaces, then $f$ is continuous.

Topology.IsEmbedding.closure_eq_preimage_closure_image theorem

(hf : IsEmbedding f) (s : Set X) : closure s = f ⁻¹' closure (f '' s)

Full source

lemma closure_eq_preimage_closure_image (hf : IsEmbedding f) (s : Set X) :
    closure s = f ⁻¹' closure (f '' s) :=
  hf.1.closure_eq_preimage_closure_image s

Closure Preservation under Topological Embedding

Informal description

Let $f : X \to Y$ be an embedding between topological spaces. For any subset $s \subseteq X$, the closure of $s$ in $X$ equals the preimage under $f$ of the closure of $f(s)$ in $Y$, i.e., $$\overline{s} = f^{-1}(\overline{f(s)}).$$

Topology.IsEmbedding.discreteTopology theorem

[DiscreteTopology Y] (hf : IsEmbedding f) : DiscreteTopology X

Full source

/-- 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`. -/
lemma discreteTopology [DiscreteTopology Y] (hf : IsEmbedding f) : DiscreteTopology X :=
  .of_continuous_injective hf.continuous hf.injective

Discrete Topology Induced by Embedding into Discrete Space

Informal description

Let $X$ and $Y$ be topological spaces with $Y$ discrete. If $f \colon X \to Y$ is an embedding, then $X$ is also discrete.

Topology.IsEmbedding.of_subsingleton theorem

[Subsingleton X] (f : X → Y) : IsEmbedding f

Full source

lemma of_subsingleton [Subsingleton X] (f : X → Y) : IsEmbedding f :=
  ⟨.of_subsingleton f, f.injective_of_subsingleton⟩

Embedding Property of Maps from Subsingleton Spaces

Informal description

For any subsingleton topological space $X$ (i.e., a space with at most one point) and any continuous map $f \colon X \to Y$ to another topological space $Y$, the map $f$ is an embedding. That is, $f$ is both injective and induces the topology on $X$ from $Y$.

Topology.isQuotientMap_iff theorem

: IsQuotientMap f ↔ Surjective f ∧ ∀ s, IsOpen s ↔ IsOpen (f ⁻¹' s)

Full source

lemma isQuotientMap_iff : IsQuotientMapIsQuotientMap f ↔ Surjective f ∧ ∀ s, IsOpen s ↔ IsOpen (f ⁻¹' s) :=
  (isQuotientMap_iff' _).trans <| and_congr Iff.rfl TopologicalSpace.ext_iff

Characterization of Quotient Maps via Open Sets

Informal description

A function $f \colon X \to Y$ between topological spaces is a quotient map if and only if $f$ is surjective and for every subset $s \subseteq Y$, $s$ is open in $Y$ if and only if its preimage $f^{-1}(s)$ is open in $X$.

Topology.isQuotientMap_iff_isClosed theorem

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

Full source

theorem isQuotientMap_iff_isClosed :
    IsQuotientMapIsQuotientMap f ↔ Surjective f ∧ ∀ s : Set Y, IsClosed s ↔ IsClosed (f ⁻¹' s) :=
  isQuotientMap_iff.trans <| Iff.rfl.and <| compl_surjective.forall.trans <| by
    simp only [isOpen_compl_iff, preimage_compl]

Characterization of Quotient Maps via Closed Sets

Informal description

A function $f \colon X \to Y$ between topological spaces is a quotient map if and only if $f$ is surjective and for every subset $s \subseteq Y$, $s$ is closed in $Y$ if and only if its preimage $f^{-1}(s)$ is closed in $X$.

Topology.IsQuotientMap.id theorem

: IsQuotientMap (@id X)

Full source

protected theorem id : IsQuotientMap (@id X) :=
  ⟨fun x => ⟨x, rfl⟩, coinduced_id.symm⟩

Identity Map is a Quotient Map

Informal description

The identity map $\mathrm{id} \colon X \to X$ on a topological space $X$ is a quotient map.

Topology.IsQuotientMap.comp theorem

(hg : IsQuotientMap g) (hf : IsQuotientMap f) : IsQuotientMap (g ∘ f)

Full source

protected theorem comp (hg : IsQuotientMap g) (hf : IsQuotientMap f) : IsQuotientMap (g ∘ f) :=
  ⟨hg.surjective.comp hf.surjective, by rw [hg.eq_coinduced, hf.eq_coinduced, coinduced_compose]⟩

Composition of Quotient Maps is a Quotient Map

Informal description

Let $f \colon X \to Y$ and $g \colon Y \to Z$ be quotient maps between topological spaces. Then the composition $g \circ f \colon X \to Z$ is also a quotient map.

Topology.IsQuotientMap.of_comp theorem

(hf : Continuous f) (hg : Continuous g) (hgf : IsQuotientMap (g ∘ f)) : IsQuotientMap g

Full source

protected theorem of_comp (hf : Continuous f) (hg : Continuous g)
    (hgf : IsQuotientMap (g ∘ f)) : IsQuotientMap g :=
  ⟨hgf.1.of_comp,
    le_antisymm
      (by rw [hgf.eq_coinduced, ← coinduced_compose]; exact coinduced_mono hf.coinduced_le)
      hg.coinduced_le⟩

Quotient Map Property via Composition

Informal description

Let $f \colon X \to Y$ and $g \colon Y \to Z$ be continuous maps between topological spaces. If the composition $g \circ f \colon X \to Z$ is a quotient map, then $g$ is a quotient map.

Topology.IsQuotientMap.of_inverse theorem

{g : Y → X} (hf : Continuous f) (hg : Continuous g) (h : LeftInverse g f) : IsQuotientMap g

Full source

theorem of_inverse {g : Y → X} (hf : Continuous f) (hg : Continuous g) (h : LeftInverse g f) :
    IsQuotientMap g := .of_comp hf hg <| h.comp_eq_id.symm ▸ IsQuotientMap.id

Quotient Map Property via Left Inverse

Informal description

Let $f \colon X \to Y$ and $g \colon Y \to X$ be continuous maps between topological spaces. If $g$ is a left inverse of $f$ (i.e., $g \circ f = \text{id}_X$), then $g$ is a quotient map.

Topology.IsQuotientMap.continuous_iff theorem

(hf : IsQuotientMap f) : Continuous g ↔ Continuous (g ∘ f)

Full source

protected theorem continuous_iff (hf : IsQuotientMap f) : ContinuousContinuous g ↔ Continuous (g ∘ f) := by
  rw [continuous_iff_coinduced_le, continuous_iff_coinduced_le, hf.eq_coinduced, coinduced_compose]

Continuity Criterion via Quotient Maps

Informal description

Let $f \colon X \to Y$ be a quotient map between topological spaces. Then a function $g \colon Y \to Z$ is continuous if and only if the composition $g \circ f \colon X \to Z$ is continuous.

Topology.IsQuotientMap.continuous theorem

(hf : IsQuotientMap f) : Continuous f

Full source

protected theorem continuous (hf : IsQuotientMap f) : Continuous f :=
  hf.continuous_iff.mp continuous_id

Quotient Maps are Continuous

Informal description

If $f \colon X \to Y$ is a quotient map between topological spaces, then $f$ is continuous.

Topology.IsQuotientMap.isOpen_preimage theorem

(hf : IsQuotientMap f) {s : Set Y} : IsOpen (f ⁻¹' s) ↔ IsOpen s

Full source

protected lemma isOpen_preimage (hf : IsQuotientMap f) {s : Set Y} : IsOpenIsOpen (f ⁻¹' s) ↔ IsOpen s :=
  ((isQuotientMap_iff.1 hf).2 s).symm

Openness Criterion for Preimages under Quotient Maps

Informal description

Let $f \colon X \to Y$ be a quotient map between topological spaces. For any subset $s \subseteq Y$, the preimage $f^{-1}(s)$ is open in $X$ if and only if $s$ is open in $Y$.

Topology.IsQuotientMap.isClosed_preimage theorem

(hf : IsQuotientMap f) {s : Set Y} : IsClosed (f ⁻¹' s) ↔ IsClosed s

Full source

protected theorem isClosed_preimage (hf : IsQuotientMap f) {s : Set Y} :
    IsClosedIsClosed (f ⁻¹' s) ↔ IsClosed s :=
  ((isQuotientMap_iff_isClosed.1 hf).2 s).symm

Closedness Criterion for Preimages under Quotient Maps

Informal description

Let $f \colon X \to Y$ be a quotient map between topological spaces. For any subset $s \subseteq Y$, the preimage $f^{-1}(s)$ is closed in $X$ if and only if $s$ is closed in $Y$.

IsOpenMap.id theorem

: IsOpenMap (@id X)

Full source

protected theorem id : IsOpenMap (@id X) := fun s hs => by rwa [image_id]

Identity Map is Open

Informal description

The identity map $\text{id} : X \to X$ on a topological space $X$ is an open map, meaning that for every open set $U \subseteq X$, the image $\text{id}(U) = U$ is open in $X$.

IsOpenMap.comp theorem

(hg : IsOpenMap g) (hf : IsOpenMap f) : IsOpenMap (g ∘ f)

Full source

protected theorem comp (hg : IsOpenMap g) (hf : IsOpenMap f) :
    IsOpenMap (g ∘ f) := fun s hs => by rw [image_comp]; exact hg _ (hf _ hs)

Composition of Open Maps is Open

Informal description

Let $f \colon X \to Y$ and $g \colon Y \to Z$ be maps between topological spaces. If $f$ and $g$ are open maps, then their composition $g \circ f \colon X \to Z$ is also an open map.

IsOpenMap.isOpen_range theorem

(hf : IsOpenMap f) : IsOpen (range f)

Full source

theorem isOpen_range (hf : IsOpenMap f) : IsOpen (range f) := by
  rw [← image_univ]
  exact hf _ isOpen_univ

Range of an Open Map is Open

Informal description

If $f \colon X \to Y$ is an open map between topological spaces, then the range of $f$ is an open subset of $Y$.

IsOpenMap.image_mem_nhds theorem

(hf : IsOpenMap f) {x : X} {s : Set X} (hx : s ∈ 𝓝 x) : f '' s ∈ 𝓝 (f x)

Full source

theorem image_mem_nhds (hf : IsOpenMap f) {x : X} {s : Set X} (hx : s ∈ 𝓝 x) : f '' sf '' s ∈ 𝓝 (f x) :=
  let ⟨t, hts, ht, hxt⟩ := mem_nhds_iff.1 hx
  mem_of_superset (IsOpen.mem_nhds (hf t ht) (mem_image_of_mem _ hxt)) (image_subset _ hts)

Open Maps Preserve Neighborhoods

Informal description

Let $f : X \to Y$ be an open map between topological spaces. For any point $x \in X$ and any neighborhood $s$ of $x$ (i.e., $s \in \mathcal{N}(x)$), the image $f(s)$ is a neighborhood of $f(x)$ in $Y$ (i.e., $f(s) \in \mathcal{N}(f(x))$).

IsOpenMap.range_mem_nhds theorem

(hf : IsOpenMap f) (x : X) : range f ∈ 𝓝 (f x)

Full source

theorem range_mem_nhds (hf : IsOpenMap f) (x : X) : rangerange f ∈ 𝓝 (f x) :=
  hf.isOpen_range.mem_nhds <| mem_range_self _

Range of Open Map is Neighborhood of Image Point

Informal description

For any open map $f \colon X \to Y$ between topological spaces and any point $x \in X$, the range of $f$ is a neighborhood of $f(x)$ in $Y$.

IsOpenMap.mapsTo_interior theorem

(hf : IsOpenMap f) {s : Set X} {t : Set Y} (h : MapsTo f s t) : MapsTo f (interior s) (interior t)

Full source

theorem mapsTo_interior (hf : IsOpenMap f) {s : Set X} {t : Set Y} (h : MapsTo f s t) :
    MapsTo f (interior s) (interior t) :=
  mapsTo'.2 <|
    interior_maximal (h.mono interior_subset Subset.rfl).image_subset (hf _ isOpen_interior)

Open Maps Preserve Interior Inclusion

Informal description

Let $f : X \to Y$ be an open map between topological spaces. If $f$ maps a subset $s \subseteq X$ into a subset $t \subseteq Y$, then $f$ also maps the interior of $s$ into the interior of $t$. In other words, if $f(s) \subseteq t$, then $f(\text{int}(s)) \subseteq \text{int}(t)$.

IsOpenMap.image_interior_subset theorem

(hf : IsOpenMap f) (s : Set X) : f '' interior s ⊆ interior (f '' s)

Full source

theorem image_interior_subset (hf : IsOpenMap f) (s : Set X) :
    f '' interior sf '' interior s ⊆ interior (f '' s) :=
  (hf.mapsTo_interior (mapsTo_image f s)).image_subset

Open Maps Preserve Interior Containment

Informal description

Let $f \colon X \to Y$ be an open map between topological spaces. For any subset $s \subseteq X$, the image of the interior of $s$ under $f$ is contained in the interior of the image of $s$ under $f$, i.e., $f(\text{int}(s)) \subseteq \text{int}(f(s))$.

IsOpenMap.nhds_le theorem

(hf : IsOpenMap f) (x : X) : 𝓝 (f x) ≤ (𝓝 x).map f

Full source

theorem nhds_le (hf : IsOpenMap f) (x : X) : 𝓝 (f x) ≤ (𝓝 x).map f :=
  le_map fun _ => hf.image_mem_nhds

Neighborhood Filter Comparison for Open Maps

Informal description

Let $f \colon X \to Y$ be an open map between topological spaces. For any point $x \in X$, the neighborhood filter $\mathcal{N}(f(x))$ at $f(x)$ is contained in the image under $f$ of the neighborhood filter $\mathcal{N}(x)$ at $x$, i.e., $\mathcal{N}(f(x)) \leq f_*(\mathcal{N}(x))$.

IsOpenMap.of_nhds_le theorem

(hf : ∀ x, 𝓝 (f x) ≤ map f (𝓝 x)) : IsOpenMap f

Full source

theorem of_nhds_le (hf : ∀ x, 𝓝 (f x) ≤ map f (𝓝 x)) : IsOpenMap f := fun _s hs =>
  isOpen_iff_mem_nhds.2 fun _y ⟨_x, hxs, hxy⟩ => hxy ▸ hf _ (image_mem_map <| hs.mem_nhds hxs)

Open Map Criterion via Neighborhood Filters

Informal description

A function $f \colon X \to Y$ between topological spaces is an open map if for every point $x \in X$, the neighborhood filter $\mathcal{N}(f(x))$ at $f(x)$ is contained in the image under $f$ of the neighborhood filter $\mathcal{N}(x)$ at $x$.

IsOpenMap.of_sections theorem

(h : ∀ x, ∃ g : Y → X, ContinuousAt g (f x) ∧ g (f x) = x ∧ RightInverse g f) : IsOpenMap f

Full source

theorem of_sections
    (h : ∀ x, ∃ g : Y → X, ContinuousAt g (f x) ∧ g (f x) = x ∧ RightInverse g f) : IsOpenMap f :=
  of_nhds_le fun x =>
    let ⟨g, hgc, hgx, hgf⟩ := h x
    calc
      𝓝 (f x) = map f (map g (𝓝 (f x))) := by rw [map_map, hgf.comp_eq_id, map_id]
      _ ≤ map f (𝓝 (g (f x))) := map_mono hgc
      _ = map f (𝓝 x) := by rw [hgx]

Open Map Criterion via Local Right Inverses

Informal description

A function $f \colon X \to Y$ between topological spaces is an open map if for every point $x \in X$, there exists a function $g \colon Y \to X$ such that: 1. $g$ is continuous at $f(x)$, 2. $g(f(x)) = x$, and 3. $g$ is a right inverse of $f$ (i.e., $f \circ g = \text{id}_Y$).

IsOpenMap.of_inverse theorem

{f' : Y → X} (h : Continuous f') (l_inv : LeftInverse f f') (r_inv : RightInverse f f') : IsOpenMap f

Full source

theorem of_inverse {f' : Y → X} (h : Continuous f') (l_inv : LeftInverse f f')
    (r_inv : RightInverse f f') : IsOpenMap f :=
  of_sections fun _ => ⟨f', h.continuousAt, r_inv _, l_inv⟩

Continuous Two-Sided Inverse Implies Open Map

Informal description

Let $f \colon X \to Y$ be a map between topological spaces. If there exists a continuous map $f' \colon Y \to X$ such that $f'$ is both a left inverse (i.e., $f'(f(x)) = x$ for all $x \in X$) and a right inverse (i.e., $f(f'(y)) = y$ for all $y \in Y$) of $f$, then $f$ is an open map.

IsOpenMap.isQuotientMap theorem

(open_map : IsOpenMap f) (cont : Continuous f) (surj : Surjective f) : IsQuotientMap f

Full source

/-- A continuous surjective open map is a quotient map. -/
theorem isQuotientMap (open_map : IsOpenMap f) (cont : Continuous f) (surj : Surjective f) :
    IsQuotientMap f :=
  isQuotientMap_iff.2
    ⟨surj, fun s => ⟨fun h => h.preimage cont, fun h => surj.image_preimage s ▸ open_map _ h⟩⟩

Continuous Open Surjective Maps are Quotient Maps

Informal description

Let $f \colon X \to Y$ be a continuous, surjective, open map between topological spaces. Then $f$ is a quotient map.

IsOpenMap.interior_preimage_subset_preimage_interior theorem

(hf : IsOpenMap f) {s : Set Y} : interior (f ⁻¹' s) ⊆ f ⁻¹' interior s

Full source

theorem interior_preimage_subset_preimage_interior (hf : IsOpenMap f) {s : Set Y} :
    interiorinterior (f ⁻¹' s) ⊆ f ⁻¹' interior s :=
  hf.mapsTo_interior (mapsTo_preimage _ _)

Open Maps Shrink Interior of Preimages

Informal description

Let $f : X \to Y$ be an open map between topological spaces. For any subset $s \subseteq Y$, the interior of the preimage $f^{-1}(s)$ is contained in the preimage of the interior of $s$, i.e., \[ \text{int}(f^{-1}(s)) \subseteq f^{-1}(\text{int}(s)). \]

IsOpenMap.preimage_interior_eq_interior_preimage theorem

(hf₁ : IsOpenMap f) (hf₂ : Continuous f) (s : Set Y) : f ⁻¹' interior s = interior (f ⁻¹' s)

Full source

theorem preimage_interior_eq_interior_preimage (hf₁ : IsOpenMap f) (hf₂ : Continuous f)
    (s : Set Y) : f ⁻¹' interior s = interior (f ⁻¹' s) :=
  Subset.antisymm (preimage_interior_subset_interior_preimage hf₂)
    (interior_preimage_subset_preimage_interior hf₁)

Equality of Preimage Interior and Interior Preimage for Continuous Open Maps

Informal description

Let $f : X \to Y$ be a continuous open map between topological spaces. For any subset $s \subseteq Y$, the preimage of the interior of $s$ under $f$ equals the interior of the preimage of $s$, i.e., \[ f^{-1}(\text{int}(s)) = \text{int}(f^{-1}(s)). \]

IsOpenMap.preimage_closure_subset_closure_preimage theorem

(hf : IsOpenMap f) {s : Set Y} : f ⁻¹' closure s ⊆ closure (f ⁻¹' s)

Full source

theorem preimage_closure_subset_closure_preimage (hf : IsOpenMap f) {s : Set Y} :
    f ⁻¹' closure sf ⁻¹' closure s ⊆ closure (f ⁻¹' s) := by
  rw [← compl_subset_compl]
  simp only [← interior_compl, ← preimage_compl, hf.interior_preimage_subset_preimage_interior]

Open Maps Contract Preimage of Closure to Closure of Preimage

Informal description

Let $f : X \to Y$ be an open map between topological spaces. For any subset $s \subseteq Y$, the preimage of the closure of $s$ under $f$ is contained in the closure of the preimage of $s$, i.e., \[ f^{-1}(\overline{s}) \subseteq \overline{f^{-1}(s)}. \]

IsOpenMap.preimage_closure_eq_closure_preimage theorem

(hf : IsOpenMap f) (hfc : Continuous f) (s : Set Y) : f ⁻¹' closure s = closure (f ⁻¹' s)

Full source

theorem preimage_closure_eq_closure_preimage (hf : IsOpenMap f) (hfc : Continuous f) (s : Set Y) :
    f ⁻¹' closure s = closure (f ⁻¹' s) :=
  hf.preimage_closure_subset_closure_preimage.antisymm (hfc.closure_preimage_subset s)

Equality of Preimage Closure and Closure Preimage for Continuous Open Maps

Informal description

Let $f : X \to Y$ be a continuous open map between topological spaces. For any subset $s \subseteq Y$, the preimage of the closure of $s$ under $f$ equals the closure of the preimage of $s$, i.e., \[ f^{-1}(\overline{s}) = \overline{f^{-1}(s)}. \]

IsOpenMap.preimage_frontier_subset_frontier_preimage theorem

(hf : IsOpenMap f) {s : Set Y} : f ⁻¹' frontier s ⊆ frontier (f ⁻¹' s)

Full source

theorem preimage_frontier_subset_frontier_preimage (hf : IsOpenMap f) {s : Set Y} :
    f ⁻¹' frontier sf ⁻¹' frontier s ⊆ frontier (f ⁻¹' s) := by
  simpa only [frontier_eq_closure_inter_closure, preimage_inter] using
    inter_subset_inter hf.preimage_closure_subset_closure_preimage
      hf.preimage_closure_subset_closure_preimage

Open Maps Contract Preimage of Frontier to Frontier of Preimage

Informal description

Let $f \colon X \to Y$ be an open map between topological spaces. For any subset $s \subseteq Y$, the preimage of the frontier of $s$ under $f$ is contained in the frontier of the preimage of $s$, i.e., \[ f^{-1}(\partial s) \subseteq \partial f^{-1}(s). \]

IsOpenMap.preimage_frontier_eq_frontier_preimage theorem

(hf : IsOpenMap f) (hfc : Continuous f) (s : Set Y) : f ⁻¹' frontier s = frontier (f ⁻¹' s)

Full source

theorem preimage_frontier_eq_frontier_preimage (hf : IsOpenMap f) (hfc : Continuous f) (s : Set Y) :
    f ⁻¹' frontier s = frontier (f ⁻¹' s) := by
  simp only [frontier_eq_closure_inter_closure, preimage_inter, preimage_compl,
    hf.preimage_closure_eq_closure_preimage hfc]

Equality of Preimage Frontier and Frontier Preimage for Continuous Open Maps

Informal description

Let $f \colon X \to Y$ be a continuous open map between topological spaces. For any subset $s \subseteq Y$, the preimage of the frontier of $s$ under $f$ equals the frontier of the preimage of $s$, i.e., \[ f^{-1}(\partial s) = \partial f^{-1}(s). \]

IsOpenMap.of_isEmpty theorem

[h : IsEmpty X] (f : X → Y) : IsOpenMap f

Full source

theorem of_isEmpty [h : IsEmpty X] (f : X → Y) : IsOpenMap f := of_nhds_le h.elim

Open Map Property for Functions from Empty Spaces

Informal description

For any empty topological space $X$ and any function $f \colon X \to Y$ to a topological space $Y$, the function $f$ is an open map.

isOpenMap_iff_nhds_le theorem

: IsOpenMap f ↔ ∀ x : X, 𝓝 (f x) ≤ (𝓝 x).map f

Full source

theorem isOpenMap_iff_nhds_le : IsOpenMapIsOpenMap f ↔ ∀ x : X, 𝓝 (f x) ≤ (𝓝 x).map f :=
  ⟨fun hf => hf.nhds_le, IsOpenMap.of_nhds_le⟩

Open Map Characterization via Neighborhood Filters

Informal description

A function $f \colon X \to Y$ between topological spaces is an open map if and only if for every point $x \in X$, the neighborhood filter $\mathcal{N}(f(x))$ at $f(x)$ is contained in the image under $f$ of the neighborhood filter $\mathcal{N}(x)$ at $x$.

isOpenMap_iff_interior theorem

: IsOpenMap f ↔ ∀ s, f '' interior s ⊆ interior (f '' s)

Full source

theorem isOpenMap_iff_interior : IsOpenMapIsOpenMap f ↔ ∀ s, f '' interior s ⊆ interior (f '' s) :=
  ⟨IsOpenMap.image_interior_subset, fun hs u hu =>
    subset_interior_iff_isOpen.mp <|
      calc
        f '' u = f '' interior u := by rw [hu.interior_eq]
        _ ⊆ interior (f '' u) := hs u⟩

Characterization of Open Maps via Interior Preservation

Informal description

A function $f \colon X \to Y$ between topological spaces is an open map if and only if for every subset $s \subseteq X$, the image of the interior of $s$ under $f$ is contained in the interior of the image of $s$ under $f$, i.e., $f(\text{int}(s)) \subseteq \text{int}(f(s))$.

Topology.IsInducing.isOpenMap theorem

(hi : IsInducing f) (ho : IsOpen (range f)) : IsOpenMap f

Full source

/-- An inducing map with an open range is an open map. -/
protected lemma Topology.IsInducing.isOpenMap (hi : IsInducing f) (ho : IsOpen (range f)) :
    IsOpenMap f :=
  IsOpenMap.of_nhds_le fun _ => (hi.map_nhds_of_mem _ <| IsOpen.mem_nhds ho <| mem_range_self _).ge

Inducing Maps with Open Range are Open Maps

Informal description

Let $f \colon X \to Y$ be an inducing map between topological spaces. If the range of $f$ is open in $Y$, then $f$ is an open map.

Dense.preimage theorem

{s : Set Y} (hs : Dense s) (hf : IsOpenMap f) : Dense (f ⁻¹' s)

Full source

/-- Preimage of a dense set under an open map is dense. -/
protected theorem Dense.preimage {s : Set Y} (hs : Dense s) (hf : IsOpenMap f) :
    Dense (f ⁻¹' s) := fun x ↦
  hf.preimage_closure_subset_closure_preimage <| hs (f x)

Density Preservation under Open Maps

Informal description

Let $f \colon X \to Y$ be an open map between topological spaces. If $s \subseteq Y$ is a dense subset of $Y$, then the preimage $f^{-1}(s)$ is a dense subset of $X$.

IsClosedMap.id theorem

: IsClosedMap (@id X)

Full source

protected theorem id : IsClosedMap (@id X) := fun s hs => by rwa [image_id]

Identity Map is Closed

Informal description

The identity map $\mathrm{id} \colon X \to X$ on a topological space $X$ is a closed map, meaning that the image of any closed subset of $X$ under $\mathrm{id}$ is closed in $X$.

IsClosedMap.comp theorem

(hg : IsClosedMap g) (hf : IsClosedMap f) : IsClosedMap (g ∘ f)

Full source

protected theorem comp (hg : IsClosedMap g) (hf : IsClosedMap f) : IsClosedMap (g ∘ f) := by
  intro s hs
  rw [image_comp]
  exact hg _ (hf _ hs)

Composition of Closed Maps is Closed

Informal description

Let $f \colon X \to Y$ and $g \colon Y \to Z$ be maps between topological spaces. If both $f$ and $g$ are closed maps (i.e., they map closed sets to closed sets), then their composition $g \circ f \colon X \to Z$ is also a closed map.

IsClosedMap.of_comp_surjective theorem

(hf : Surjective f) (hf' : Continuous f) (hfg : IsClosedMap (g ∘ f)) : IsClosedMap g

Full source

protected theorem of_comp_surjective (hf : Surjective f) (hf' : Continuous f)
    (hfg : IsClosedMap (g ∘ f)) : IsClosedMap g := by
  intro K hK
  rw [← image_preimage_eq K hf, ← image_comp]
  exact hfg _ (hK.preimage hf')

Surjective Continuous Map with Closed Composition Implies Closed Map

Informal description

Let $f \colon X \to Y$ be a continuous surjective map between topological spaces, and let $g \colon Y \to Z$ be another map. If the composition $g \circ f \colon X \to Z$ is a closed map, then $g$ is also a closed map.

IsClosedMap.closure_image_subset theorem

(hf : IsClosedMap f) (s : Set X) : closure (f '' s) ⊆ f '' closure s

Full source

theorem closure_image_subset (hf : IsClosedMap f) (s : Set X) :
    closureclosure (f '' s) ⊆ f '' closure s :=
  closure_minimal (image_subset _ subset_closure) (hf _ isClosed_closure)

Closure of Image under Closed Map is Contained in Image of Closure

Informal description

Let $f : X \to Y$ be a closed map between topological spaces. For any subset $s \subseteq X$, the closure of the image $f(s)$ in $Y$ is contained in the image of the closure of $s$ under $f$, i.e., $\overline{f(s)} \subseteq f(\overline{s})$.

IsClosedMap.of_inverse theorem

{f' : Y → X} (h : Continuous f') (l_inv : LeftInverse f f') (r_inv : RightInverse f f') : IsClosedMap f

Full source

theorem of_inverse {f' : Y → X} (h : Continuous f') (l_inv : LeftInverse f f')
    (r_inv : RightInverse f f') : IsClosedMap f := fun s hs => by
  rw [image_eq_preimage_of_inverse r_inv l_inv]
  exact hs.preimage h

Closed Map Criterion via Continuous Two-Sided Inverse

Informal description

Let $f \colon X \to Y$ be a map between topological spaces. If there exists a continuous map $f' \colon Y \to X$ such that $f'$ is both a left inverse and a right inverse of $f$ (i.e., $f' \circ f = \text{id}_X$ and $f \circ f' = \text{id}_Y$), then $f$ is a closed map.

IsClosedMap.of_nonempty theorem

(h : ∀ s, IsClosed s → s.Nonempty → IsClosed (f '' s)) : IsClosedMap f

Full source

theorem of_nonempty (h : ∀ s, IsClosed s → s.Nonempty → IsClosed (f '' s)) :
    IsClosedMap f := by
  intro s hs; rcases eq_empty_or_nonempty s with h2s | h2s
  · simp_rw [h2s, image_empty, isClosed_empty]
  · exact h s hs h2s

Characterization of Closed Maps via Nonempty Closed Sets

Informal description

A map $f \colon X \to Y$ between topological spaces is a closed map if for every nonempty closed subset $s \subseteq X$, the image $f(s)$ is closed in $Y$.

IsClosedMap.isClosed_range theorem

(hf : IsClosedMap f) : IsClosed (range f)

Full source

theorem isClosed_range (hf : IsClosedMap f) : IsClosed (range f) :=
  @image_univ _ _ f ▸ hf _ isClosed_univ

Range of a Closed Map is Closed

Informal description

If $f \colon X \to Y$ is a closed map between topological spaces, then the range of $f$ is a closed subset of $Y$.

IsClosedMap.isQuotientMap theorem

(hcl : IsClosedMap f) (hcont : Continuous f) (hsurj : Surjective f) : IsQuotientMap f

Full source

theorem isQuotientMap (hcl : IsClosedMap f) (hcont : Continuous f)
    (hsurj : Surjective f) : IsQuotientMap f :=
  isQuotientMap_iff_isClosed.2 ⟨hsurj, fun s =>
    ⟨fun hs => hs.preimage hcont, fun hs => hsurj.image_preimage s ▸ hcl _ hs⟩⟩

Continuous Surjective Closed Maps are Quotient Maps

Informal description

Let $f \colon X \to Y$ be a continuous, surjective, closed map between topological spaces. Then $f$ is a quotient map, meaning the topology on $Y$ is the quotient topology induced by $f$.

Topology.IsInducing.isClosedMap theorem

(hf : IsInducing f) (h : IsClosed (range f)) : IsClosedMap f

Full source

lemma Topology.IsInducing.isClosedMap (hf : IsInducing f) (h : IsClosed (range f)) :
    IsClosedMap f := by
  intro s hs
  rcases hf.isClosed_iff.1 hs with ⟨t, ht, rfl⟩
  rw [image_preimage_eq_inter_range]
  exact ht.inter h

Inducing Map with Closed Range is a Closed Map

Informal description

Let $f \colon X \to Y$ be an inducing map between topological spaces (i.e., the topology on $X$ is induced by $f$ from the topology on $Y$). If the range of $f$ is closed in $Y$, then $f$ is a closed map (i.e., the image of any closed set in $X$ is closed in $Y$).

isClosedMap_iff_closure_image theorem

: IsClosedMap f ↔ ∀ s, closure (f '' s) ⊆ f '' closure s

Full source

theorem isClosedMap_iff_closure_image :
    IsClosedMapIsClosedMap f ↔ ∀ s, closure (f '' s) ⊆ f '' closure s :=
  ⟨IsClosedMap.closure_image_subset, fun hs c hc =>
    isClosed_of_closure_subset <|
      calc
        closure (f '' c) ⊆ f '' closure c := hs c
        _ = f '' c := by rw [hc.closure_eq]⟩

Characterization of Closed Maps via Closure of Images

Informal description

A map $f \colon X \to Y$ between topological spaces is closed if and only if for every subset $s \subseteq X$, the closure of the image $f(s)$ in $Y$ is contained in the image of the closure of $s$ under $f$, i.e., $\overline{f(s)} \subseteq f(\overline{s})$.

isClosedMap_iff_clusterPt theorem

: IsClosedMap f ↔ ∀ s y, MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)

Full source

/-- 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_iff_clusterPt :
    IsClosedMapIsClosedMap f ↔ ∀ s y, MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s) := by
  simp [MapClusterPt, isClosedMap_iff_closure_image, subset_def, mem_closure_iff_clusterPt,
    and_comm]

Characterization of Closed Maps via Cluster Points

Informal description

A map $f \colon X \to Y$ between topological spaces is closed if and only if for every subset $s \subseteq X$ and every cluster point $y$ of $f(s)$, there exists a cluster point $x$ of $s$ such that $f(x) = y$.

IsClosedMap.closure_image_eq_of_continuous theorem

(f_closed : IsClosedMap f) (f_cont : Continuous f) (s : Set X) : closure (f '' s) = f '' closure s

Full source

theorem IsClosedMap.closure_image_eq_of_continuous
    (f_closed : IsClosedMap f) (f_cont : Continuous f) (s : Set X) :
    closure (f '' s) = f '' closure s :=
  subset_antisymm (f_closed.closure_image_subset s) (image_closure_subset_closure_image f_cont)

Equality of Closure and Image of Closure for Continuous Closed Maps

Informal description

Let $f \colon X \to Y$ be a continuous closed map between topological spaces. For any subset $s \subseteq X$, the closure of the image $f(s)$ in $Y$ equals the image of the closure of $s$ under $f$, i.e., $\overline{f(s)} = f(\overline{s})$.

IsClosedMap.lift'_closure_map_eq theorem

(f_closed : IsClosedMap f) (f_cont : Continuous f) (F : Filter X) : (map f F).lift' closure = map f (F.lift' closure)

Full source

theorem IsClosedMap.lift'_closure_map_eq
    (f_closed : IsClosedMap f) (f_cont : Continuous f) (F : Filter X) :
    (map f F).lift' closure = map f (F.lift' closure) := by
  rw [map_lift'_eq2 (monotone_closure Y), map_lift'_eq (monotone_closure X)]
  congr
  ext s : 1
  exact f_closed.closure_image_eq_of_continuous f_cont s

Equality of Filter Lifts for Continuous Closed Maps

Informal description

Let $f \colon X \to Y$ be a continuous closed map between topological spaces. For any filter $F$ on $X$, the lift of the closure operation applied to the image filter $\text{map}\,f\,F$ equals the image under $f$ of the lift of the closure operation applied to $F$. In symbols: $$(\text{map}\,f\,F).\text{lift}'\,\text{closure} = \text{map}\,f\,(F.\text{lift}'\,\text{closure}).$$

IsClosedMap.mapClusterPt_iff_lift'_closure theorem

 {F : Filter X} (f_closed : IsClosedMap f) (f_cont : Continuous f) {y : Y} :
  MapClusterPt y F f ↔ ((F.lift' closure) ⊓ 𝓟 (f ⁻¹' { y })).NeBot

Full source

theorem IsClosedMap.mapClusterPt_iff_lift'_closure
    {F : Filter X} (f_closed : IsClosedMap f) (f_cont : Continuous f) {y : Y} :
    MapClusterPtMapClusterPt y F f ↔ ((F.lift' closure) ⊓ 𝓟 (f ⁻¹' {y})).NeBot := by
  rw [MapClusterPt, clusterPt_iff_lift'_closure', f_closed.lift'_closure_map_eq f_cont,
      ← comap_principal, ← map_neBot_iff f, Filter.push_pull, principal_singleton]

Characterization of Cluster Points for Continuous Closed Maps via Filter Lifts

Informal description

Let $f \colon X \to Y$ be a continuous closed map between topological spaces, and let $F$ be a filter on $X$. For a point $y \in Y$, $y$ is a cluster point of the image filter $\text{map}\,f\,F$ if and only if the filter generated by the closure of sets in $F$ intersected with the principal filter on the preimage $f^{-1}(\{y\})$ is non-trivial. In symbols: $$y \text{ is a cluster point of } \text{map}\,f\,F \iff \left(F.\text{lift}'\,\text{closure} \sqcap \mathcal{P}(f^{-1}(\{y\}))\right) \text{ is non-trivial}.$$

Topology.IsOpenEmbedding.isEmbedding theorem

(hf : IsOpenEmbedding f) : IsEmbedding f

Full source

lemma IsOpenEmbedding.isEmbedding (hf : IsOpenEmbedding f) : IsEmbedding f := hf.toIsEmbedding

Open embeddings are embeddings

Informal description

If a continuous map $f \colon X \to Y$ between topological spaces is an open embedding, then it is also an embedding.

Topology.IsOpenEmbedding.isInducing theorem

(hf : IsOpenEmbedding f) : IsInducing f

Full source

lemma IsOpenEmbedding.isInducing (hf : IsOpenEmbedding f) : IsInducing f :=
  hf.isEmbedding.isInducing

Open embeddings induce subspace topology

Informal description

If a continuous map $f \colon X \to Y$ between topological spaces is an open embedding, then it is inducing. That is, the topology on $X$ is the one induced via $f$ from the topology on $Y$.

Topology.IsOpenEmbedding.isOpenMap theorem

(hf : IsOpenEmbedding f) : IsOpenMap f

Full source

lemma IsOpenEmbedding.isOpenMap (hf : IsOpenEmbedding f) : IsOpenMap f :=
  hf.isEmbedding.isInducing.isOpenMap hf.isOpen_range

Open Embeddings are Open Maps

Informal description

If a continuous map $f \colon X \to Y$ between topological spaces is an open embedding, then $f$ is an open map. That is, the image of any open set in $X$ under $f$ is open in $Y$.

Topology.IsOpenEmbedding.map_nhds_eq theorem

(hf : IsOpenEmbedding f) (x : X) : map f (𝓝 x) = 𝓝 (f x)

Full source

theorem IsOpenEmbedding.map_nhds_eq (hf : IsOpenEmbedding f) (x : X) :
    map f (𝓝 x) = 𝓝 (f x) :=
  hf.isEmbedding.map_nhds_of_mem _ <| hf.isOpen_range.mem_nhds <| mem_range_self _

Neighborhood Filter Preservation for Open Embeddings

Informal description

Let $f \colon X \to Y$ be an open embedding between topological spaces. For any point $x \in X$, the pushforward of the neighborhood filter at $x$ under $f$ equals the neighborhood filter at $f(x)$. In other words, $\text{map}\, f\, (\mathcal{N}_x) = \mathcal{N}_{f(x)}$.

Topology.IsOpenEmbedding.isOpen_iff_image_isOpen theorem

(hf : IsOpenEmbedding f) {s : Set X} : IsOpen s ↔ IsOpen (f '' s)

Full source

lemma IsOpenEmbedding.isOpen_iff_image_isOpen (hf : IsOpenEmbedding f) {s : Set X} :
    IsOpenIsOpen s ↔ IsOpen (f '' s) where
  mp := hf.isOpenMap s
  mpr h := by convert ← h.preimage hf.isEmbedding.continuous; apply preimage_image_eq _ hf.injective

Openness Characterization via Open Embeddings

Informal description

Let $f \colon X \to Y$ be an open embedding between topological spaces. For any subset $s \subseteq X$, $s$ is open in $X$ if and only if its image $f(s)$ is open in $Y$.

Topology.IsOpenEmbedding.tendsto_nhds_iff theorem

 [TopologicalSpace Z] {f : ι → Y} {l : Filter ι} {y : Y} (hg : IsOpenEmbedding g) :
  Tendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y))

Full source

theorem IsOpenEmbedding.tendsto_nhds_iff [TopologicalSpace Z] {f : ι → Y} {l : Filter ι} {y : Y}
    (hg : IsOpenEmbedding g) : TendstoTendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y)) :=
  hg.isEmbedding.tendsto_nhds_iff

Limit Characterization via Open Embeddings

Informal description

Let $g : X \to Y$ be an open embedding between topological spaces. For any function $f : \iota \to Y$, filter $l$ on $\iota$, and point $y \in Y$, the function $f$ tends to $y$ along $l$ if and only if the composition $g \circ f$ tends to $g(y)$ along $l$. In other words: $$\lim_{l} f = y \iff \lim_{l} (g \circ f) = g(y).$$

Topology.IsOpenEmbedding.tendsto_nhds_iff' theorem

(hf : IsOpenEmbedding f) {l : Filter Z} {x : X} : Tendsto (g ∘ f) (𝓝 x) l ↔ Tendsto g (𝓝 (f x)) l

Full source

theorem IsOpenEmbedding.tendsto_nhds_iff' (hf : IsOpenEmbedding f) {l : Filter Z} {x : X} :
    TendstoTendsto (g ∘ f) (𝓝 x) l ↔ Tendsto g (𝓝 (f x)) l := by
  rw [Tendsto, ← map_map, hf.map_nhds_eq]; rfl

Limit Characterization for Compositions with Open Embeddings

Informal description

Let $f \colon X \to Y$ be an open embedding between topological spaces, and let $g \colon Y \to Z$ be a map to another topological space $Z$. For any point $x \in X$ and any filter $l$ on $Z$, the composition $g \circ f$ tends to $l$ as $x'$ approaches $x$ if and only if $g$ tends to $l$ as $y$ approaches $f(x)$. In other words, \[ \lim_{x' \to x} g(f(x')) = l \quad \Leftrightarrow \quad \lim_{y \to f(x)} g(y) = l. \]

Topology.IsOpenEmbedding.continuousAt_iff theorem

[TopologicalSpace Z] (hf : IsOpenEmbedding f) {x : X} : ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)

Full source

theorem IsOpenEmbedding.continuousAt_iff [TopologicalSpace Z] (hf : IsOpenEmbedding f) {x : X} :
    ContinuousAtContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x) :=
  hf.tendsto_nhds_iff'

Continuity Characterization for Compositions with Open Embeddings

Informal description

Let $f \colon X \to Y$ be an open embedding between topological spaces, and let $g \colon Y \to Z$ be a map to another topological space $Z$. For any point $x \in X$, the composition $g \circ f$ is continuous at $x$ if and only if $g$ is continuous at $f(x)$. In other words, \[ g \circ f \text{ is continuous at } x \quad \Leftrightarrow \quad g \text{ is continuous at } f(x). \]

Topology.IsOpenEmbedding.continuous theorem

(hf : IsOpenEmbedding f) : Continuous f

Full source

theorem IsOpenEmbedding.continuous (hf : IsOpenEmbedding f) : Continuous f :=
  hf.isEmbedding.continuous

Continuity of Open Embeddings

Informal description

If $f \colon X \to Y$ is an open embedding between topological spaces, then $f$ is continuous.

Topology.IsOpenEmbedding.isOpen_iff_preimage_isOpen theorem

(hf : IsOpenEmbedding f) {s : Set Y} (hs : s ⊆ range f) : IsOpen s ↔ IsOpen (f ⁻¹' s)

Full source

lemma IsOpenEmbedding.isOpen_iff_preimage_isOpen (hf : IsOpenEmbedding f) {s : Set Y}
    (hs : s ⊆ range f) : IsOpenIsOpen s ↔ IsOpen (f ⁻¹' s) := by
  rw [hf.isOpen_iff_image_isOpen, image_preimage_eq_inter_range, inter_eq_self_of_subset_left hs]

Openness Criterion via Preimage Under Open Embedding

Informal description

Let $f \colon X \to Y$ be an open embedding between topological spaces. For any subset $s \subseteq Y$ that is contained in the range of $f$, $s$ is open in $Y$ if and only if its preimage $f^{-1}(s)$ is open in $X$.

Topology.IsOpenEmbedding.of_isEmbedding_isOpenMap theorem

(h₁ : IsEmbedding f) (h₂ : IsOpenMap f) : IsOpenEmbedding f

Full source

lemma IsOpenEmbedding.of_isEmbedding_isOpenMap (h₁ : IsEmbedding f) (h₂ : IsOpenMap f) :
    IsOpenEmbedding f :=
  ⟨h₁, h₂.isOpen_range⟩

Open Embedding Characterization via Embedding and Open Map

Informal description

If a map $f \colon X \to Y$ between topological spaces is both an embedding and an open map, then it is an open embedding.

Topology.IsEmbedding.isOpenEmbedding_of_surjective theorem

(hf : IsEmbedding f) (hsurj : f.Surjective) : IsOpenEmbedding f

Full source

/-- A surjective embedding is an `IsOpenEmbedding`. -/
lemma IsEmbedding.isOpenEmbedding_of_surjective (hf : IsEmbedding f) (hsurj : f.Surjective) :
    IsOpenEmbedding f :=
  ⟨hf, hsurj.range_eq ▸ isOpen_univ⟩

Surjective Embeddings are Open Embeddings

Informal description

If a continuous map $f \colon X \to Y$ between topological spaces is an embedding and surjective, then it is an open embedding.

Topology.isOpenEmbedding_iff_isEmbedding_isOpenMap theorem

: IsOpenEmbedding f ↔ IsEmbedding f ∧ IsOpenMap f

Full source

lemma isOpenEmbedding_iff_isEmbedding_isOpenMap : IsOpenEmbeddingIsOpenEmbedding f ↔ IsEmbedding f ∧ IsOpenMap f :=
  ⟨fun h => ⟨h.1, h.isOpenMap⟩, fun h => .of_isEmbedding_isOpenMap h.1 h.2⟩

Characterization of Open Embeddings via Embedding and Open Map Properties

Informal description

A map $f \colon X \to Y$ between topological spaces is an open embedding if and only if it is both an embedding and an open map.

Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap theorem

(h₁ : Continuous f) (h₂ : Injective f) (h₃ : IsOpenMap f) : IsOpenEmbedding f

Full source

theorem IsOpenEmbedding.of_continuous_injective_isOpenMap
    (h₁ : Continuous f) (h₂ : Injective f) (h₃ : IsOpenMap f) : IsOpenEmbedding f := by
  simp only [isOpenEmbedding_iff_isEmbedding_isOpenMap, isEmbedding_iff, isInducing_iff_nhds, *,
    and_true]
  exact fun x =>
    le_antisymm (h₁.tendsto _).le_comap (@comap_map _ _ (𝓝 x) _ h₂ ▸ comap_mono (h₃.nhds_le _))

Continuous Injective Open Maps are Open Embeddings

Informal description

Let $f \colon X \to Y$ be a continuous, injective map between topological spaces. If $f$ is also an open map, then $f$ is an open embedding.

Topology.isOpenEmbedding_iff_continuous_injective_isOpenMap theorem

: IsOpenEmbedding f ↔ Continuous f ∧ Injective f ∧ IsOpenMap f

Full source

lemma isOpenEmbedding_iff_continuous_injective_isOpenMap :
    IsOpenEmbeddingIsOpenEmbedding f ↔ Continuous f ∧ Injective f ∧ IsOpenMap f :=
  ⟨fun h => ⟨h.continuous, h.injective, h.isOpenMap⟩, fun h =>
    .of_continuous_injective_isOpenMap h.1 h.2.1 h.2.2⟩

Characterization of Open Embeddings via Continuity, Injectivity, and Open Map Property

Informal description

A map $f \colon X \to Y$ between topological spaces is an open embedding if and only if it is continuous, injective, and an open map (i.e., it maps open sets in $X$ to open sets in $Y$).

Topology.IsOpenEmbedding.id theorem

: IsOpenEmbedding (@id X)

Full source

protected lemma id : IsOpenEmbedding (@id X) := ⟨.id, IsOpenMap.id.isOpen_range⟩

Identity Map is an Open Embedding

Informal description

The identity map $\mathrm{id} \colon X \to X$ on a topological space $X$ is an open embedding. That is, it is injective, continuous, and maps open sets to open sets, thereby identifying $X$ with an open subspace of itself.

Topology.IsOpenEmbedding.comp theorem

(hg : IsOpenEmbedding g) (hf : IsOpenEmbedding f) : IsOpenEmbedding (g ∘ f)

Full source

protected lemma comp (hg : IsOpenEmbedding g)
    (hf : IsOpenEmbedding f) : IsOpenEmbedding (g ∘ f) :=
  ⟨hg.1.comp hf.1, (hg.isOpenMap.comp hf.isOpenMap).isOpen_range⟩

Composition of Open Embeddings is an Open Embedding

Informal description

Let $f \colon X \to Y$ and $g \colon Y \to Z$ be continuous maps between topological spaces. If both $f$ and $g$ are open embeddings, then their composition $g \circ f \colon X \to Z$ is also an open embedding.

Topology.IsOpenEmbedding.isOpenMap_iff theorem

(hg : IsOpenEmbedding g) : IsOpenMap f ↔ IsOpenMap (g ∘ f)

Full source

theorem isOpenMap_iff (hg : IsOpenEmbedding g) :
    IsOpenMapIsOpenMap f ↔ IsOpenMap (g ∘ f) := by
  simp_rw [isOpenMap_iff_nhds_le, ← map_map, comp, ← hg.map_nhds_eq, map_le_map_iff hg.injective]

Open Map Characterization via Open Embedding Composition

Informal description

Let $g \colon Y \to Z$ be an open embedding between topological spaces. For any map $f \colon X \to Y$, $f$ is an open map if and only if the composition $g \circ f \colon X \to Z$ is an open map.

Topology.IsOpenEmbedding.of_comp_iff theorem

(f : X → Y) (hg : IsOpenEmbedding g) : IsOpenEmbedding (g ∘ f) ↔ IsOpenEmbedding f

Full source

theorem of_comp_iff (f : X → Y) (hg : IsOpenEmbedding g) :
    IsOpenEmbeddingIsOpenEmbedding (g ∘ f) ↔ IsOpenEmbedding f := by
  simp only [isOpenEmbedding_iff_continuous_injective_isOpenMap, ← hg.isOpenMap_iff, ←
    hg.1.continuous_iff, hg.injective.of_comp_iff]

Open Embedding Characterization via Composition with Open Embedding

Informal description

Let $f \colon X \to Y$ be a map between topological spaces and $g \colon Y \to Z$ be an open embedding. Then the composition $g \circ f \colon X \to Z$ is an open embedding if and only if $f$ is an open embedding.

Topology.IsOpenEmbedding.of_comp theorem

(f : X → Y) (hg : IsOpenEmbedding g) (h : IsOpenEmbedding (g ∘ f)) : IsOpenEmbedding f

Full source

lemma of_comp (f : X → Y) (hg : IsOpenEmbedding g) (h : IsOpenEmbedding (g ∘ f)) :
    IsOpenEmbedding f := (IsOpenEmbedding.of_comp_iff f hg).1 h

Open Embedding Property via Composition with Open Embedding

Informal description

Let $f \colon X \to Y$ be a map between topological spaces and $g \colon Y \to Z$ be an open embedding. If the composition $g \circ f \colon X \to Z$ is an open embedding, then $f$ is also an open embedding.

Topology.IsOpenEmbedding.of_isEmpty theorem

[IsEmpty X] (f : X → Y) : IsOpenEmbedding f

Full source

theorem of_isEmpty [IsEmpty X] (f : X → Y) : IsOpenEmbedding f :=
  of_isEmbedding_isOpenMap (.of_subsingleton f) (.of_isEmpty f)

Open Embedding Property for Functions from Empty Spaces

Informal description

For any empty topological space $X$ and any function $f \colon X \to Y$ to a topological space $Y$, the function $f$ is an open embedding.

Topology.IsOpenEmbedding.image_mem_nhds theorem

{f : X → Y} (hf : IsOpenEmbedding f) {s : Set X} {x : X} : f '' s ∈ 𝓝 (f x) ↔ s ∈ 𝓝 x

Full source

theorem image_mem_nhds {f : X → Y} (hf : IsOpenEmbedding f) {s : Set X} {x : X} :
    f '' sf '' s ∈ 𝓝 (f x)f '' s ∈ 𝓝 (f x) ↔ s ∈ 𝓝 x := by
  rw [← hf.map_nhds_eq, mem_map, preimage_image_eq _ hf.injective]

Neighborhood Characterization for Open Embeddings

Informal description

Let $f \colon X \to Y$ be an open embedding between topological spaces. For any subset $s \subseteq X$ and any point $x \in X$, the image $f(s)$ is a neighborhood of $f(x)$ in $Y$ if and only if $s$ is a neighborhood of $x$ in $X$. In other words, $f(s) \in \mathcal{N}(f(x)) \leftrightarrow s \in \mathcal{N}(x)$.

Topology.IsClosedEmbedding.isEmbedding theorem

(hf : IsClosedEmbedding f) : IsEmbedding f

Full source

lemma isEmbedding (hf : IsClosedEmbedding f) : IsEmbedding f := hf.toIsEmbedding

Closed Embedding Implies Embedding

Informal description

If a map $f \colon X \to Y$ between topological spaces is a closed embedding, then it is an embedding. That is, $f$ is injective and the topology on $X$ is induced by $f$ from the topology on $Y$.

Topology.IsClosedEmbedding.isInducing theorem

(hf : IsClosedEmbedding f) : IsInducing f

Full source

lemma isInducing (hf : IsClosedEmbedding f) : IsInducing f := hf.isEmbedding.isInducing

Closed Embedding Induces Topology

Informal description

If a continuous map $f \colon X \to Y$ between topological spaces is a closed embedding (i.e., $f$ is injective, has closed image, and induces the topology on $X$ from $Y$), then $f$ is inducing. That is, the topology on $X$ is the one induced via $f$ from the topology on $Y$.

Topology.IsClosedEmbedding.continuous theorem

(hf : IsClosedEmbedding f) : Continuous f

Full source

lemma continuous (hf : IsClosedEmbedding f) : Continuous f := hf.isEmbedding.continuous

Continuity of Closed Embeddings

Informal description

If a map $f \colon X \to Y$ between topological spaces is a closed embedding, then $f$ is continuous.

Topology.IsClosedEmbedding.tendsto_nhds_iff theorem

 {g : ι → X} {l : Filter ι} {x : X} (hf : IsClosedEmbedding f) : Tendsto g l (𝓝 x) ↔ Tendsto (f ∘ g) l (𝓝 (f x))

Full source

lemma tendsto_nhds_iff {g : ι → X} {l : Filter ι} {x : X} (hf : IsClosedEmbedding f) :
    TendstoTendsto g l (𝓝 x) ↔ Tendsto (f ∘ g) l (𝓝 (f x)) := hf.isEmbedding.tendsto_nhds_iff

Limit Characterization via Closed Embeddings

Informal description

Let $f \colon X \to Y$ be a closed embedding between topological spaces. For any function $g \colon \iota \to X$, filter $l$ on $\iota$, and point $x \in X$, the function $g$ tends to $x$ along $l$ if and only if the composition $f \circ g$ tends to $f(x)$ along $l$. In other words: $$\lim_{l} g = x \iff \lim_{l} (f \circ g) = f(x).$$

Topology.IsClosedEmbedding.isClosedMap theorem

(hf : IsClosedEmbedding f) : IsClosedMap f

Full source

lemma isClosedMap (hf : IsClosedEmbedding f) : IsClosedMap f :=
  hf.isEmbedding.isInducing.isClosedMap hf.isClosed_range

Closed Embedding Implies Closed Map

Informal description

If a map $f \colon X \to Y$ between topological spaces is a closed embedding, then $f$ is a closed map. That is, the image of any closed set in $X$ under $f$ is closed in $Y$.

Topology.IsClosedEmbedding.isClosed_iff_image_isClosed theorem

(hf : IsClosedEmbedding f) {s : Set X} : IsClosed s ↔ IsClosed (f '' s)

Full source

lemma isClosed_iff_image_isClosed (hf : IsClosedEmbedding f) {s : Set X} :
    IsClosedIsClosed s ↔ IsClosed (f '' s) :=
  ⟨hf.isClosedMap s, fun h => by
    rw [← preimage_image_eq s hf.injective]
    exact h.preimage hf.continuous⟩

Characterization of Closed Sets via Closed Embedding Images

Informal description

Let $f \colon X \to Y$ be a closed embedding between topological spaces. For any subset $s \subseteq X$, $s$ is closed in $X$ if and only if its image $f(s)$ is closed in $Y$.

Topology.IsClosedEmbedding.isClosed_iff_preimage_isClosed theorem

(hf : IsClosedEmbedding f) {s : Set Y} (hs : s ⊆ range f) : IsClosed s ↔ IsClosed (f ⁻¹' s)

Full source

lemma isClosed_iff_preimage_isClosed (hf : IsClosedEmbedding f) {s : Set Y}
    (hs : s ⊆ range f) : IsClosedIsClosed s ↔ IsClosed (f ⁻¹' s) := by
  rw [hf.isClosed_iff_image_isClosed, image_preimage_eq_of_subset hs]

Closedness Criterion via Preimage under Closed Embedding

Informal description

Let $f \colon X \to Y$ be a closed embedding between topological spaces. For any subset $s \subseteq Y$ that is contained in the range of $f$, $s$ is closed in $Y$ if and only if its preimage $f^{-1}(s)$ is closed in $X$.

Topology.IsClosedEmbedding.of_isEmbedding_isClosedMap theorem

(h₁ : IsEmbedding f) (h₂ : IsClosedMap f) : IsClosedEmbedding f

Full source

lemma of_isEmbedding_isClosedMap (h₁ : IsEmbedding f) (h₂ : IsClosedMap f) :
    IsClosedEmbedding f :=
  ⟨h₁, image_univ (f := f) ▸ h₂ univ isClosed_univ⟩

Closed Embedding from Embedding and Closed Map

Informal description

Let $f : X \to Y$ be a map between topological spaces. If $f$ is an embedding and a closed map, then $f$ is a closed embedding.

Topology.IsClosedEmbedding.of_continuous_injective_isClosedMap theorem

(h₁ : Continuous f) (h₂ : Injective f) (h₃ : IsClosedMap f) : IsClosedEmbedding f

Full source

lemma of_continuous_injective_isClosedMap (h₁ : Continuous f) (h₂ : Injective f)
    (h₃ : IsClosedMap f) : IsClosedEmbedding f := by
  refine .of_isEmbedding_isClosedMap ⟨⟨?_⟩, h₂⟩ h₃
  refine h₁.le_induced.antisymm fun s hs => ?_
  refine ⟨(f '' sᶜ)ᶜ, (h₃ _ hs.isClosed_compl).isOpen_compl, ?_⟩
  rw [preimage_compl, preimage_image_eq _ h₂, compl_compl]

Closed Embedding from Continuous Injective Closed Map

Informal description

Let $f \colon X \to Y$ be a continuous, injective map between topological spaces. If $f$ is also a closed map (i.e., the image of every closed set in $X$ is closed in $Y$), then $f$ is a closed embedding.

Topology.IsClosedEmbedding.isClosedEmbedding_iff_continuous_injective_isClosedMap theorem

{f : X → Y} : IsClosedEmbedding f ↔ Continuous f ∧ Injective f ∧ IsClosedMap f

Full source

lemma isClosedEmbedding_iff_continuous_injective_isClosedMap {f : X → Y} :
    IsClosedEmbeddingIsClosedEmbedding f ↔ Continuous f ∧ Injective f ∧ IsClosedMap f where
  mp h := ⟨h.continuous, h.injective, h.isClosedMap⟩
  mpr h := .of_continuous_injective_isClosedMap h.1 h.2.1 h.2.2

Characterization of Closed Embeddings: $f$ is a closed embedding $\iff$ $f$ is continuous, injective, and a closed map

Informal description

A map $f \colon X \to Y$ between topological spaces is a closed embedding if and only if it is continuous, injective, and a closed map (i.e., the image of every closed set in $X$ under $f$ is closed in $Y$).

Topology.IsClosedEmbedding.id theorem

: IsClosedEmbedding (@id X)

Full source

protected theorem id : IsClosedEmbedding (@id X) := ⟨.id, IsClosedMap.id.isClosed_range⟩

Identity Map is a Closed Embedding

Informal description

The identity map $\mathrm{id} \colon X \to X$ on a topological space $X$ is a closed embedding, meaning it is continuous, injective, and maps closed subsets of $X$ to closed subsets of $X$.

Topology.IsClosedEmbedding.comp theorem

(hg : IsClosedEmbedding g) (hf : IsClosedEmbedding f) : IsClosedEmbedding (g ∘ f)

Full source

theorem comp (hg : IsClosedEmbedding g) (hf : IsClosedEmbedding f) :
    IsClosedEmbedding (g ∘ f) :=
  ⟨hg.isEmbedding.comp hf.isEmbedding, (hg.isClosedMap.comp hf.isClosedMap).isClosed_range⟩

Composition of Closed Embeddings is a Closed Embedding

Informal description

Let $f \colon X \to Y$ and $g \colon Y \to Z$ be continuous maps between topological spaces. If both $f$ and $g$ are closed embeddings (i.e., they are injective, continuous, and map closed sets to closed sets), then their composition $g \circ f \colon X \to Z$ is also a closed embedding.

Topology.IsClosedEmbedding.of_comp_iff theorem

(hg : IsClosedEmbedding g) : IsClosedEmbedding (g ∘ f) ↔ IsClosedEmbedding f

Full source

lemma of_comp_iff (hg : IsClosedEmbedding g) : IsClosedEmbeddingIsClosedEmbedding (g ∘ f) ↔ IsClosedEmbedding f := by
  simp_rw [isClosedEmbedding_iff, hg.isEmbedding.of_comp_iff, Set.range_comp,
    ← hg.isClosed_iff_image_isClosed]

Closed Embedding Property of Composition via Closed Embedding Second Map

Informal description

Let $f \colon X \to Y$ and $g \colon Y \to Z$ be continuous maps between topological spaces, with $g$ being a closed embedding. Then the composition $g \circ f \colon X \to Z$ is a closed embedding if and only if $f$ is a closed embedding.

Topology.IsClosedEmbedding.closure_image_eq theorem

(hf : IsClosedEmbedding f) (s : Set X) : closure (f '' s) = f '' closure s

Full source

theorem closure_image_eq (hf : IsClosedEmbedding f) (s : Set X) :
    closure (f '' s) = f '' closure s :=
  hf.isClosedMap.closure_image_eq_of_continuous hf.continuous s

Closure-Image Equality for Closed Embeddings

Informal description

Let $f \colon X \to Y$ be a closed embedding between topological spaces. For any subset $s \subseteq X$, the closure of the image $f(s)$ in $Y$ equals the image of the closure of $s$ under $f$, i.e., $\overline{f(s)} = f(\overline{s})$.

Mathlib.Topology.Maps.Basic

References

Tags