Documentation

Mathlib.Topology.LocalAtTarget

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.restrictPreimage_inducing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (s : Set β) (h : Inducing f) :
Inducing (s.restrictPreimage f)
theorem Inducing.restrictPreimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (s : Set β) (h : Inducing f) :
Inducing (s.restrictPreimage f)

Alias of Set.restrictPreimage_inducing.

theorem Set.restrictPreimage_embedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (s : Set β) (h : Embedding f) :
Embedding (s.restrictPreimage f)
theorem Embedding.restrictPreimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (s : Set β) (h : Embedding f) :
Embedding (s.restrictPreimage f)

Alias of Set.restrictPreimage_embedding.

theorem Set.restrictPreimage_openEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (s : Set β) (h : OpenEmbedding f) :
OpenEmbedding (s.restrictPreimage f)
theorem OpenEmbedding.restrictPreimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (s : Set β) (h : OpenEmbedding f) :
OpenEmbedding (s.restrictPreimage f)

Alias of Set.restrictPreimage_openEmbedding.

theorem Set.restrictPreimage_closedEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (s : Set β) (h : ClosedEmbedding f) :
ClosedEmbedding (s.restrictPreimage f)
theorem ClosedEmbedding.restrictPreimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (s : Set β) (h : ClosedEmbedding f) :
ClosedEmbedding (s.restrictPreimage f)

Alias of Set.restrictPreimage_closedEmbedding.

theorem IsClosedMap.restrictPreimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (H : IsClosedMap f) (s : Set β) :
IsClosedMap (s.restrictPreimage f)
@[deprecated]
theorem Set.restrictPreimage_isClosedMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (s : Set β) (H : IsClosedMap f) :
IsClosedMap (s.restrictPreimage f)
theorem IsOpenMap.restrictPreimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (H : IsOpenMap f) (s : Set β) :
IsOpenMap (s.restrictPreimage f)
@[deprecated]
theorem Set.restrictPreimage_isOpenMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (s : Set β) (H : IsOpenMap f) :
IsOpenMap (s.restrictPreimage f)
theorem isOpen_iff_inter_of_iSup_eq_top {β : Type u_2} [TopologicalSpace β] {ι : Type u_3} {U : ιTopologicalSpace.Opens β} (hU : iSup U = ) (s : Set β) :
IsOpen s ∀ (i : ι), IsOpen (s (U i))
theorem isOpen_iff_coe_preimage_of_iSup_eq_top {β : Type u_2} [TopologicalSpace β] {ι : Type u_3} {U : ιTopologicalSpace.Opens β} (hU : iSup U = ) (s : Set β) :
IsOpen s ∀ (i : ι), IsOpen (Subtype.val ⁻¹' s)
theorem isClosed_iff_coe_preimage_of_iSup_eq_top {β : Type u_2} [TopologicalSpace β] {ι : Type u_3} {U : ιTopologicalSpace.Opens β} (hU : iSup U = ) (s : Set β) :
IsClosed s ∀ (i : ι), IsClosed (Subtype.val ⁻¹' s)
theorem isOpenMap_iff_isOpenMap_of_iSup_eq_top {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {ι : Type u_3} {U : ιTopologicalSpace.Opens β} (hU : iSup U = ) :
IsOpenMap f ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
theorem isClosedMap_iff_isClosedMap_of_iSup_eq_top {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {ι : Type u_3} {U : ιTopologicalSpace.Opens β} (hU : iSup U = ) :
IsClosedMap f ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)
theorem inducing_iff_inducing_of_iSup_eq_top {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {ι : Type u_3} {U : ιTopologicalSpace.Opens β} (hU : iSup U = ) (h : Continuous f) :
Inducing f ∀ (i : ι), Inducing ((U i).carrier.restrictPreimage f)
theorem embedding_iff_embedding_of_iSup_eq_top {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {ι : Type u_3} {U : ιTopologicalSpace.Opens β} (hU : iSup U = ) (h : Continuous f) :
Embedding f ∀ (i : ι), Embedding ((U i).carrier.restrictPreimage f)
theorem openEmbedding_iff_openEmbedding_of_iSup_eq_top {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {ι : Type u_3} {U : ιTopologicalSpace.Opens β} (hU : iSup U = ) (h : Continuous f) :
OpenEmbedding f ∀ (i : ι), OpenEmbedding ((U i).carrier.restrictPreimage f)
theorem closedEmbedding_iff_closedEmbedding_of_iSup_eq_top {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {ι : Type u_3} {U : ιTopologicalSpace.Opens β} (hU : iSup U = ) (h : Continuous f) :
ClosedEmbedding f ∀ (i : ι), ClosedEmbedding ((U i).carrier.restrictPreimage f)