# mathlib3documentation

topology.local_at_target

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 set.restrict_preimage_is_closed_map {α : Type u_1} {β : Type u_2} {f : α β} (s : set β) (H : is_closed_map f) :
theorem is_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 is_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 is_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 is_closed_map_iff_is_closed_map_of_supr_eq_top {α : Type u_1} {β : Type u_2} {f : α β} {ι : Type u_3} {U : ι } (hU : supr U = ) :
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) :
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) :
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) :
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) :