Theorems · Theorem · general topology

isEmbedding_of_iSup_eq_top_of_preimage_subset_range

∀ {X : Type u_6} {Y : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
  Continuous f →
    ∀ {ι : Type u_4} (U : ι → TopologicalSpace.Opens Y),
      Set.range f ⊆ ↑(iSup U) →
        ∀ (V : ι → Type u_5) [inst_2 : (i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X),
          (∀ (i : ι), Continuous (iV i)) →
            (∀ (i : ι), f ⁻¹' ↑(U i) ⊆ Set.range (iV i)) →
              (∀ (i : ι), Topology.IsEmbedding (f ∘ iV i)) → Topology.IsEmbedding f

Given a continuous map f : X → Y between topological spaces. Suppose we have an open cover U i of the range of f, and a family of continuous maps V i → X whose images are a cover of X that is coarser than the pullback of U under f. To check that f is an embedding it suffices to check that V i → Y is an embedding for all i.

Defined in

Mathlib.Topology.LocalAtTarget

Cited by

1 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpace