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) :
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
open_iff_inter_of_supr_eq_top
{β : Type u_2}
[topological_space β]
{ι : Type u_3}
{U : ι → topological_space.opens β}
(hU : supr U = ⊤)
(s : set β) :
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 β) :
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 β) :
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) :
open_embedding 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}
[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).val.restrict_preimage f)