# Properties of maps that are local at the target. #

We show that the following properties of continuous maps are local at the target :

• Inducing
• Embedding
• OpenEmbedding
• ClosedEmbedding
theorem Set.restrictPreimage_inducing {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (s : Set β) (h : ) :
Inducing (s.restrictPreimage f)
theorem Inducing.restrictPreimage {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (s : Set β) (h : ) :
Inducing (s.restrictPreimage f)

Alias of Set.restrictPreimage_inducing.

theorem Set.restrictPreimage_embedding {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (s : Set β) (h : ) :
Embedding (s.restrictPreimage f)
theorem Embedding.restrictPreimage {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (s : Set β) (h : ) :
Embedding (s.restrictPreimage f)

Alias of Set.restrictPreimage_embedding.

theorem Set.restrictPreimage_openEmbedding {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (s : Set β) (h : ) :
OpenEmbedding (s.restrictPreimage f)
theorem OpenEmbedding.restrictPreimage {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (s : Set β) (h : ) :
OpenEmbedding (s.restrictPreimage f)

Alias of Set.restrictPreimage_openEmbedding.

theorem Set.restrictPreimage_closedEmbedding {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (s : Set β) (h : ) :
ClosedEmbedding (s.restrictPreimage f)
theorem ClosedEmbedding.restrictPreimage {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (s : Set β) (h : ) :
ClosedEmbedding (s.restrictPreimage f)

Alias of Set.restrictPreimage_closedEmbedding.

theorem IsClosedMap.restrictPreimage {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (H : ) (s : Set β) :
IsClosedMap (s.restrictPreimage f)
@[deprecated]
theorem Set.restrictPreimage_isClosedMap {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (s : Set β) (H : ) :
IsClosedMap (s.restrictPreimage f)
theorem IsOpenMap.restrictPreimage {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (H : ) (s : Set β) :
IsOpenMap (s.restrictPreimage f)
@[deprecated]
theorem Set.restrictPreimage_isOpenMap {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (s : Set β) (H : ) :
IsOpenMap (s.restrictPreimage f)
theorem isOpen_iff_inter_of_iSup_eq_top {β : Type u_2} [] {ι : Type u_3} {U : } (hU : iSup U = ) (s : Set β) :
∀ (i : ι), IsOpen (s (U i))
theorem isOpen_iff_coe_preimage_of_iSup_eq_top {β : Type u_2} [] {ι : Type u_3} {U : } (hU : iSup U = ) (s : Set β) :
∀ (i : ι), IsOpen (Subtype.val ⁻¹' s)
theorem isClosed_iff_coe_preimage_of_iSup_eq_top {β : Type u_2} [] {ι : Type u_3} {U : } (hU : iSup U = ) (s : Set β) :
∀ (i : ι), IsClosed (Subtype.val ⁻¹' s)
theorem isClosedMap_iff_isClosedMap_of_iSup_eq_top {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {ι : Type u_3} {U : } (hU : iSup U = ) :
∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)
theorem inducing_iff_inducing_of_iSup_eq_top {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {ι : Type u_3} {U : } (hU : iSup U = ) (h : ) :
∀ (i : ι), Inducing ((U i).carrier.restrictPreimage f)
theorem embedding_iff_embedding_of_iSup_eq_top {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {ι : Type u_3} {U : } (hU : iSup U = ) (h : ) :
∀ (i : ι), Embedding ((U i).carrier.restrictPreimage f)
theorem openEmbedding_iff_openEmbedding_of_iSup_eq_top {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {ι : Type u_3} {U : } (hU : iSup U = ) (h : ) :
∀ (i : ι), OpenEmbedding ((U i).carrier.restrictPreimage f)
theorem closedEmbedding_iff_closedEmbedding_of_iSup_eq_top {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {ι : Type u_3} {U : } (hU : iSup U = ) (h : ) :
∀ (i : ι), ClosedEmbedding ((U i).carrier.restrictPreimage f)