# mathlibdocumentation

topology.local_at_target

# 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
• open_embedding
• closed_embedding
theorem set.restrict_preimage_inducing {α : Type u_1} {β : Type u_2} {f : α → β} (s : set β) (h : inducing f) :
theorem inducing.restrict_preimage {α : Type u_1} {β : Type u_2} {f : α → β} (s : set β) (h : inducing f) :

Alias of set.restrict_preimage_inducing.

theorem set.restrict_preimage_embedding {α : Type u_1} {β : Type u_2} {f : α → β} (s : set β) (h : embedding f) :
theorem embedding.restrict_preimage {α : Type u_1} {β : Type u_2} {f : α → β} (s : set β) (h : embedding f) :

Alias of set.restrict_preimage_embedding.

theorem set.restrict_preimage_open_embedding {α : Type u_1} {β : Type u_2} {f : α → β} (s : set β) (h : open_embedding f) :
theorem open_embedding.restrict_preimage {α : Type u_1} {β : Type u_2} {f : α → β} (s : set β) (h : open_embedding f) :

Alias of set.restrict_preimage_open_embedding.

theorem set.restrict_preimage_closed_embedding {α : Type u_1} {β : Type u_2} {f : α → β} (s : set β) (h : closed_embedding f) :
theorem closed_embedding.restrict_preimage {α : Type u_1} {β : Type u_2} {f : α → β} (s : set β) (h : closed_embedding f) :

Alias of set.restrict_preimage_closed_embedding.

theorem open_iff_inter_of_supr_eq_top {β : Type u_2} {ι : Type u_3} {U : ι → } (hU : supr U = ) (s : set β) :
∀ (i : ι), is_open (s (U i))
theorem open_iff_coe_preimage_of_supr_eq_top {β : Type u_2} {ι : Type u_3} {U : ι → } (hU : supr U = ) (s : set β) :
∀ (i : ι), is_open (coe ⁻¹' s)
theorem closed_iff_coe_preimage_of_supr_eq_top {β : Type u_2} {ι : Type u_3} {U : ι → } (hU : supr U = ) (s : set β) :
∀ (i : ι), is_closed (coe ⁻¹' s)
theorem inducing_iff_inducing_of_supr_eq_top {α : Type u_1} {β : Type u_2} {f : α → β} {ι : Type u_3} {U : ι → } (hU : supr U = ) (h : continuous f) :
∀ (i : ι), inducing ((U i).val.restrict_preimage f)
theorem embedding_iff_embedding_of_supr_eq_top {α : Type u_1} {β : Type u_2} {f : α → β} {ι : Type u_3} {U : ι → } (hU : supr U = ) (h : continuous f) :
∀ (i : ι), embedding ((U i).val.restrict_preimage f)
theorem open_embedding_iff_open_embedding_of_supr_eq_top {α : Type u_1} {β : Type u_2} {f : α → β} {ι : Type u_3} {U : ι → } (hU : supr U = ) (h : continuous f) :
∀ (i : ι), open_embedding ((U i).val.restrict_preimage f)
theorem closed_embedding_iff_closed_embedding_of_supr_eq_top {α : Type u_1} {β : Type u_2} {f : α → β} {ι : Type u_3} {U : ι → } (hU : supr U = ) (h : continuous f) :
∀ (i : ι), closed_embedding ((U i).val.restrict_preimage f)