Properties of maps that are local at the target or at the source. #
We show that the following properties of continuous maps are local at the target :
IsInducingIsOpenMapIsClosedMapIsEmbeddingIsOpenEmbeddingIsClosedEmbeddingGeneralizingMap
We show that the following properties of continuous maps are local at the source:
theorem
Set.restrictPreimage_isInducing
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : Topology.IsInducing f)
:
theorem
Topology.IsInducing.restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : IsInducing f)
:
IsInducing (s.restrictPreimage f)
Alias of Set.restrictPreimage_isInducing.
theorem
Set.restrictPreimage_isEmbedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : Topology.IsEmbedding f)
:
theorem
Topology.IsEmbedding.restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : IsEmbedding f)
:
IsEmbedding (s.restrictPreimage f)
Alias of Set.restrictPreimage_isEmbedding.
theorem
Set.restrictPreimage_isOpenEmbedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : Topology.IsOpenEmbedding f)
:
theorem
Topology.IsOpenEmbedding.restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : IsOpenEmbedding f)
:
Alias of Set.restrictPreimage_isOpenEmbedding.
theorem
Set.restrictPreimage_isClosedEmbedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : Topology.IsClosedEmbedding f)
:
theorem
Topology.IsClosedEmbedding.restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : IsClosedEmbedding f)
:
Alias of Set.restrictPreimage_isClosedEmbedding.
theorem
IsClosedMap.restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(H : IsClosedMap f)
(s : Set β)
:
IsClosedMap (s.restrictPreimage f)
theorem
IsOpenMap.restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(H : IsOpenMap f)
(s : Set β)
:
IsOpenMap (s.restrictPreimage f)
theorem
GeneralizingMap.restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(H : GeneralizingMap f)
(s : Set β)
:
theorem
TopologicalSpace.IsOpenCover.isOpen_iff_inter
{β : Type u_2}
[TopologicalSpace β]
{ι : Type u_3}
{U : ι → Opens β}
{s : Set β}
(hU : IsOpenCover U)
:
theorem
TopologicalSpace.IsOpenCover.isOpen_iff_coe_preimage
{β : Type u_2}
[TopologicalSpace β]
{ι : Type u_3}
{U : ι → Opens β}
{s : Set β}
(hU : IsOpenCover U)
:
theorem
TopologicalSpace.IsOpenCover.isClosed_iff_coe_preimage
{β : Type u_2}
[TopologicalSpace β]
{ι : Type u_3}
{U : ι → Opens β}
(hU : IsOpenCover U)
{s : Set β}
:
theorem
TopologicalSpace.IsOpenCover.isLocallyClosed_iff_coe_preimage
{β : Type u_2}
[TopologicalSpace β]
{ι : Type u_3}
{U : ι → Opens β}
(hU : IsOpenCover U)
{s : Set β}
:
theorem
TopologicalSpace.IsOpenCover.isOpenMap_iff_restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{ι : Type u_3}
{U : ι → Opens β}
(hU : IsOpenCover U)
:
theorem
TopologicalSpace.IsOpenCover.isClosedMap_iff_restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{ι : Type u_3}
{U : ι → Opens β}
(hU : IsOpenCover U)
:
theorem
TopologicalSpace.IsOpenCover.isInducing_iff_restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{ι : Type u_3}
{U : ι → Opens β}
(hU : IsOpenCover U)
(h : Continuous f)
:
theorem
TopologicalSpace.IsOpenCover.isEmbedding_iff_restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{ι : Type u_3}
{U : ι → Opens β}
(hU : IsOpenCover U)
(h : Continuous f)
:
theorem
TopologicalSpace.IsOpenCover.isOpenEmbedding_iff_restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{ι : Type u_3}
{U : ι → Opens β}
(hU : IsOpenCover U)
(h : Continuous f)
:
theorem
TopologicalSpace.IsOpenCover.isClosedEmbedding_iff_restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{ι : Type u_3}
{U : ι → Opens β}
(hU : IsOpenCover U)
(h : Continuous f)
:
Topology.IsClosedEmbedding f ↔ ∀ (i : ι), Topology.IsClosedEmbedding ((U i).carrier.restrictPreimage f)
theorem
TopologicalSpace.IsOpenCover.denseRange_iff_restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{f : α → β}
{ι : Type u_3}
{U : ι → Opens β}
(hU : IsOpenCover U)
:
theorem
TopologicalSpace.IsOpenCover.generalizingMap_iff_restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{ι : Type u_3}
{U : ι → Opens β}
(hU : IsOpenCover U)
:
theorem
TopologicalSpace.IsOpenCover.isOpenMap_iff_comp
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{ι : Type u_3}
{U : ι → Opens α}
(hU : IsOpenCover U)
:
theorem
TopologicalSpace.IsOpenCover.generalizingMap_iff_comp
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{ι : Type u_3}
{U : ι → Opens α}
(hU : IsOpenCover U)
:
@[deprecated TopologicalSpace.IsOpenCover.isOpen_iff_inter (since := "2025-02-10")]
theorem
isOpen_iff_inter_of_iSup_eq_top
{β : Type u_2}
[TopologicalSpace β]
{ι : Type u_3}
{U : ι → TopologicalSpace.Opens β}
(hU : iSup U = ⊤)
(s : Set β)
:
@[deprecated TopologicalSpace.IsOpenCover.isOpen_iff_coe_preimage (since := "2025-02-10")]
theorem
isOpen_iff_coe_preimage_of_iSup_eq_top
{β : Type u_2}
[TopologicalSpace β]
{ι : Type u_3}
{U : ι → TopologicalSpace.Opens β}
(hU : iSup U = ⊤)
(s : Set β)
:
@[deprecated TopologicalSpace.IsOpenCover.isClosed_iff_coe_preimage (since := "2025-02-10")]
theorem
isClosed_iff_coe_preimage_of_iSup_eq_top
{β : Type u_2}
[TopologicalSpace β]
{ι : Type u_3}
{U : ι → TopologicalSpace.Opens β}
(hU : iSup U = ⊤)
(s : Set β)
:
@[deprecated TopologicalSpace.IsOpenCover.isLocallyClosed_iff_coe_preimage (since := "2025-02-10")]
theorem
isLocallyClosed_iff_coe_preimage_of_iSup_eq_top
{β : Type u_2}
[TopologicalSpace β]
{ι : Type u_3}
{U : ι → TopologicalSpace.Opens β}
(hU : iSup U = ⊤)
(s : Set β)
:
@[deprecated TopologicalSpace.IsOpenCover.isOpenMap_iff_restrictPreimage (since := "2025-02-10")]
theorem
isOpenMap_iff_isOpenMap_of_iSup_eq_top
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{ι : Type u_3}
{U : ι → TopologicalSpace.Opens β}
(hU : iSup U = ⊤)
:
@[deprecated TopologicalSpace.IsOpenCover.isClosedMap_iff_restrictPreimage (since := "2025-02-10")]
theorem
isClosedMap_iff_isClosedMap_of_iSup_eq_top
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{ι : Type u_3}
{U : ι → TopologicalSpace.Opens β}
(hU : iSup U = ⊤)
:
@[deprecated TopologicalSpace.IsOpenCover.isInducing_iff_restrictPreimage (since := "2025-02-10")]
theorem
inducing_iff_inducing_of_iSup_eq_top
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{ι : Type u_3}
{U : ι → TopologicalSpace.Opens β}
(hU : iSup U = ⊤)
(h : Continuous f)
:
@[deprecated TopologicalSpace.IsOpenCover.isEmbedding_iff_restrictPreimage (since := "2025-02-10")]
theorem
isEmbedding_iff_of_iSup_eq_top
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{ι : Type u_3}
{U : ι → TopologicalSpace.Opens β}
(hU : iSup U = ⊤)
(h : Continuous f)
:
@[deprecated TopologicalSpace.IsOpenCover.isOpenEmbedding_iff_restrictPreimage (since := "2025-02-10")]
theorem
isOpenEmbedding_iff_isOpenEmbedding_of_iSup_eq_top
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{ι : Type u_3}
{U : ι → TopologicalSpace.Opens β}
(hU : iSup U = ⊤)
(h : Continuous f)
:
@[deprecated TopologicalSpace.IsOpenCover.isClosedEmbedding_iff_restrictPreimage (since := "2025-02-10")]
theorem
isClosedEmbedding_iff_isClosedEmbedding_of_iSup_eq_top
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{ι : Type u_3}
{U : ι → TopologicalSpace.Opens β}
(hU : iSup U = ⊤)
(h : Continuous f)
:
Topology.IsClosedEmbedding f ↔ ∀ (i : ι), Topology.IsClosedEmbedding ((U i).carrier.restrictPreimage f)
@[deprecated TopologicalSpace.IsOpenCover.denseRange_iff_restrictPreimage (since := "2025-02-10")]
theorem
denseRange_iff_denseRange_of_iSup_eq_top
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{f : α → β}
{ι : Type u_3}
{U : ι → TopologicalSpace.Opens β}
(hU : iSup U = ⊤)
:
theorem
isEmbedding_of_iSup_eq_top_of_preimage_subset_range
{X : Type u_6}
{Y : Type u_7}
[TopologicalSpace X]
[TopologicalSpace Y]
(f : X → Y)
(h : Continuous f)
{ι : Type u_4}
(U : ι → TopologicalSpace.Opens Y)
(hU : Set.range f ⊆ ↑(iSup U))
(V : ι → Type u_5)
[(i : ι) → TopologicalSpace (V i)]
(iV : (i : ι) → V i → X)
(hiV : ∀ (i : ι), Continuous (iV i))
(hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ Set.range (iV i))
(hV' : ∀ (i : ι), Topology.IsEmbedding (f ∘ iV i))
:
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.