Properties of maps that are local at the target.

We show that the following properties of continuous maps are local at the target :

• Inducing
• Embedding
• OpenEmbedding
• ClosedEmbedding

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)