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

Alias of Set.restrictPreimage_inducing.

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

Alias of Set.restrictPreimage_embedding.

theorem Set.restrictPreimage_openEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (s : Set β) (h : OpenEmbedding f) :
theorem Set.restrictPreimage_isClosedMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (s : Set β) (H : IsClosedMap 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 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 (Set.restrictPreimage (U i).carrier 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 (Set.restrictPreimage (U i).carrier 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 (Set.restrictPreimage (U i).carrier 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 (Set.restrictPreimage (U i).carrier 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 (Set.restrictPreimage (U i).carrier f)