Properties of maps that are local at the target. #
We show that the following properties of continuous maps are local at the target :
theorem
Set.restrictPreimage_inducing
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : Inducing f)
:
Inducing (Set.restrictPreimage s f)
theorem
Inducing.restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : Inducing f)
:
Inducing (Set.restrictPreimage s f)
Alias of Set.restrictPreimage_inducing.
theorem
Set.restrictPreimage_embedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : Embedding f)
:
theorem
Embedding.restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : Embedding f)
:
Alias of Set.restrictPreimage_embedding.
theorem
Set.restrictPreimage_openEmbedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : OpenEmbedding f)
:
theorem
OpenEmbedding.restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : OpenEmbedding f)
:
Alias of Set.restrictPreimage_openEmbedding.
theorem
Set.restrictPreimage_closedEmbedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : ClosedEmbedding f)
:
theorem
ClosedEmbedding.restrictPreimage
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(h : ClosedEmbedding f)
:
Alias of Set.restrictPreimage_closedEmbedding.
theorem
Set.restrictPreimage_isClosedMap
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(s : Set β)
(H : IsClosedMap 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
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 = ⊤)
:
IsClosedMap f ↔ ∀ (i : ι), IsClosedMap (Set.restrictPreimage (U i).carrier f)
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)
:
Inducing f ↔ ∀ (i : ι), Inducing (Set.restrictPreimage (U i).carrier f)
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)
:
Embedding f ↔ ∀ (i : ι), Embedding (Set.restrictPreimage (U i).carrier f)
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)
:
OpenEmbedding f ↔ ∀ (i : ι), OpenEmbedding (Set.restrictPreimage (U i).carrier f)
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)
:
ClosedEmbedding f ↔ ∀ (i : ι), ClosedEmbedding (Set.restrictPreimage (U i).carrier f)