restricting an open embedding to a preimage?

Stream: Is there code for X?

[Kim Morrison]

import Mathlib

theorem IsOpenEmbedding.foo
    {Y X : Type*} [TopologicalSpace Y] [TopologicalSpace X]
    {e : Y → X} (he : IsOpenEmbedding e) {s : Set X} (hs : s ⊆ range e) :
    Nonempty ((e ⁻¹' s) ≃ₜ s) := sorry

Do we have this? (Presumably an actual construction, not the NonEmpty itself.)

[Aaron Liu]

I don't think you need an open embedding I think it works with just an embedding

[Aaron Liu]

well I found docs#Topology.IsEmbedding.homeomorphImage

[Aaron Liu]

You can can compose it with docs#Homeomorph.setCongr

[Aaron Liu]

here we go

import Mathlib

open Topology Set

theorem IsOpenEmbedding.foo
    {Y X : Type*} [TopologicalSpace Y] [TopologicalSpace X]
    {e : Y → X} (he : IsOpenEmbedding e) {s : Set X} (hs : s ⊆ range e) :
    Nonempty ((e ⁻¹' s) ≃ₜ s) :=
  ⟨(he.isEmbedding.homeomorphImage (e ⁻¹' s)).trans (.setCongr (image_preimage_eq_iff.2 hs))⟩

[Kim Morrison]

Thanks!