Properties of maps that are local at the target. #
We show that the following properties of continuous maps are local at the target :
IsInducingIsEmbeddingIsOpenEmbeddingIsClosedEmbedding
theorem
Set.restrictPreimage_isInducing
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : Topology.IsInducing f)
:
@[deprecated Set.restrictPreimage_isInducing (since := "2024-10-28")]
theorem
Set.restrictPreimage_inducing
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : Topology.IsInducing f)
:
Alias of Set.restrictPreimage_isInducing.
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.
@[deprecated Topology.IsInducing.restrictPreimage (since := "2024-10-28")]
theorem
Inducing.restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : Topology.IsInducing f)
:
Alias of Set.restrictPreimage_isInducing.
Alias of Set.restrictPreimage_isInducing.
theorem
Set.restrictPreimage_isEmbedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : Topology.IsEmbedding f)
:
@[deprecated Set.restrictPreimage_isEmbedding (since := "2024-10-26")]
theorem
Set.restrictPreimage_embedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : Topology.IsEmbedding f)
:
Alias of Set.restrictPreimage_isEmbedding.
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.
@[deprecated Topology.IsEmbedding.restrictPreimage (since := "2024-10-26")]
theorem
Embedding.restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : Topology.IsEmbedding f)
:
Alias of Set.restrictPreimage_isEmbedding.
Alias of Set.restrictPreimage_isEmbedding.
theorem
Set.restrictPreimage_isOpenEmbedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : Topology.IsOpenEmbedding f)
:
@[deprecated Set.restrictPreimage_isOpenEmbedding (since := "2024-10-18")]
theorem
Set.restrictPreimage_openEmbedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : Topology.IsOpenEmbedding f)
:
Alias of Set.restrictPreimage_isOpenEmbedding.
theorem
Topology.IsOpenEmbedding.restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : IsOpenEmbedding f)
:
Alias of Set.restrictPreimage_isOpenEmbedding.
@[deprecated Topology.IsOpenEmbedding.restrictPreimage (since := "2024-10-18")]
theorem
OpenEmbedding.restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : Topology.IsOpenEmbedding f)
:
Alias of Set.restrictPreimage_isOpenEmbedding.
Alias of Set.restrictPreimage_isOpenEmbedding.
theorem
Set.restrictPreimage_isClosedEmbedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : Topology.IsClosedEmbedding f)
:
@[deprecated Set.restrictPreimage_isClosedEmbedding (since := "2024-10-20")]
theorem
Set.restrictPreimage_closedEmbedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : Topology.IsClosedEmbedding f)
:
Alias of Set.restrictPreimage_isClosedEmbedding.
theorem
Topology.IsClosedEmbedding.restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : IsClosedEmbedding f)
:
Alias of Set.restrictPreimage_isClosedEmbedding.
@[deprecated Topology.IsClosedEmbedding.restrictPreimage (since := "2024-10-20")]
theorem
ClosedEmbedding.restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : Topology.IsClosedEmbedding f)
:
Alias of Set.restrictPreimage_isClosedEmbedding.
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
isOpen_iff_inter_of_iSup_eq_top
{β : Type u_2}
[TopologicalSpace β]
{ι : Type u_3}
{U : ι → TopologicalSpace.Opens β}
(hU : iSup U = ⊤)
(s : Set β)
:
theorem
isOpen_iff_coe_preimage_of_iSup_eq_top
{β : Type u_2}
[TopologicalSpace β]
{ι : Type u_3}
{U : ι → TopologicalSpace.Opens β}
(hU : iSup U = ⊤)
(s : Set β)
:
theorem
isClosed_iff_coe_preimage_of_iSup_eq_top
{β : Type u_2}
[TopologicalSpace β]
{ι : Type u_3}
{U : ι → TopologicalSpace.Opens β}
(hU : iSup U = ⊤)
(s : Set β)
:
theorem
isLocallyClosed_iff_coe_preimage_of_iSup_eq_top
{β : Type u_2}
[TopologicalSpace β]
{ι : Type u_3}
{U : ι → TopologicalSpace.Opens β}
(hU : iSup U = ⊤)
(s : Set β)
:
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 = ⊤)
:
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 = ⊤)
:
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)
:
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)
:
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 V i of the range of f, and an open cover U i of X that is
coarser than the pullback of V under f.
To check that f is an embedding it suffices to check that U i → Y is an embedding for all i.
@[deprecated isEmbedding_iff_of_iSup_eq_top (since := "2024-10-26")]
theorem
embedding_iff_embedding_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)
:
Alias of isEmbedding_iff_of_iSup_eq_top.
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 isOpenEmbedding_iff_isOpenEmbedding_of_iSup_eq_top (since := "2024-10-18")]
theorem
openEmbedding_iff_openEmbedding_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)
:
Alias of isOpenEmbedding_iff_isOpenEmbedding_of_iSup_eq_top.
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)
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 = ⊤)
:
@[deprecated isClosedEmbedding_iff_isClosedEmbedding_of_iSup_eq_top (since := "2024-10-20")]
theorem
closedEmbedding_iff_closedEmbedding_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)
Alias of isClosedEmbedding_iff_isClosedEmbedding_of_iSup_eq_top.