mathlib documentation

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 :

theorem set.restrict_preimage_inducing {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (s : set β) (h : inducing f) :
theorem inducing.restrict_preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (s : set β) (h : inducing f) :

Alias of set.restrict_preimage_inducing.

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

Alias of set.restrict_preimage_embedding.

theorem set.restrict_preimage_open_embedding {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (s : set β) (h : open_embedding f) :
theorem open_embedding.restrict_preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {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} [topological_space α] [topological_space β] {f : α → β} (s : set β) (h : closed_embedding f) :
theorem closed_embedding.restrict_preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {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} [topological_space β] {ι : Type u_3} {U : ι → topological_space.opens β} (hU : supr U = ) (s : set β) :
is_open s ∀ (i : ι), is_open (s (U i))
theorem open_iff_coe_preimage_of_supr_eq_top {β : Type u_2} [topological_space β] {ι : Type u_3} {U : ι → topological_space.opens β} (hU : supr U = ) (s : set β) :
is_open s ∀ (i : ι), is_open (coe ⁻¹' s)
theorem closed_iff_coe_preimage_of_supr_eq_top {β : Type u_2} [topological_space β] {ι : Type u_3} {U : ι → topological_space.opens β} (hU : supr U = ) (s : set β) :
is_closed s ∀ (i : ι), is_closed (coe ⁻¹' s)
theorem inducing_iff_inducing_of_supr_eq_top {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {ι : Type u_3} {U : ι → topological_space.opens β} (hU : supr U = ) (h : continuous f) :
inducing f ∀ (i : ι), inducing ((U i).val.restrict_preimage f)
theorem embedding_iff_embedding_of_supr_eq_top {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {ι : Type u_3} {U : ι → topological_space.opens β} (hU : supr U = ) (h : continuous f) :
embedding 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} [topological_space α] [topological_space β] {f : α → β} {ι : Type u_3} {U : ι → topological_space.opens β} (hU : supr U = ) (h : continuous f) :
theorem closed_embedding_iff_closed_embedding_of_supr_eq_top {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {ι : Type u_3} {U : ι → topological_space.opens β} (hU : supr U = ) (h : continuous f) :