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) :
inducing (s.restrict_preimage f)
theorem
inducing.restrict_preimage
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
(s : set β)
(h : inducing f) :
inducing (s.restrict_preimage 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) :
embedding (s.restrict_preimage f)
theorem
embedding.restrict_preimage
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
(s : set β)
(h : embedding f) :
embedding (s.restrict_preimage 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
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_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 = ⊤) :
is_closed_map f ↔ ∀ (i : ι), is_closed_map ((U i).carrier.restrict_preimage f)
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) :
open_embedding f ↔ ∀ (i : ι), open_embedding ((U i).carrier.restrict_preimage 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) :
closed_embedding f ↔ ∀ (i : ι), closed_embedding ((U i).carrier.restrict_preimage f)