mathlib3 documentation

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 :

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 set.restrict_preimage_is_closed_map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} (s : set β) (H : is_closed_map f) :
theorem is_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 is_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 is_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 β) :
theorem is_closed_map_iff_is_closed_map_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 = ) :
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) :
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) :
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) :