Properties of maps that are local at the target.

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

• IsInducing
• IsEmbedding
• IsOpenEmbedding
• IsClosedEmbedding

theorem Set.restrictPreimage_isInducing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (s : Set β) (h : Topology.IsInducing f) : Topology.IsInducing (s.restrictPreimage f)

@[deprecated Set.restrictPreimage_isInducing]

theorem Set.restrictPreimage_inducing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (s : Set β) (h : Topology.IsInducing f) : Topology.IsInducing (s.restrictPreimage f)

Alias of Set.restrictPreimage_isInducing.

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

Alias of Set.restrictPreimage_isInducing.

@[deprecated Topology.IsInducing.restrictPreimage]

theorem Inducing.restrictPreimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (s : Set β) (h : Topology.IsInducing f) : Topology.IsInducing (s.restrictPreimage f)

Alias of Set.restrictPreimage_isInducing.

---

Alias of Set.restrictPreimage_isInducing.

theorem Set.restrictPreimage_isEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (s : Set β) (h : Topology.IsEmbedding f) : Topology.IsEmbedding (s.restrictPreimage f)

@[deprecated Set.restrictPreimage_isEmbedding]

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

Alias of Set.restrictPreimage_isEmbedding.

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

Alias of Set.restrictPreimage_isEmbedding.

@[deprecated Topology.IsEmbedding.restrictPreimage]

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

Alias of Set.restrictPreimage_isEmbedding.

---

Alias of Set.restrictPreimage_isEmbedding.

theorem Set.restrictPreimage_isOpenEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (s : Set β) (h : Topology.IsOpenEmbedding f) : Topology.IsOpenEmbedding (s.restrictPreimage f)

@[deprecated Set.restrictPreimage_isOpenEmbedding]

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

Alias of Set.restrictPreimage_isOpenEmbedding.

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

Alias of Set.restrictPreimage_isOpenEmbedding.

@[deprecated Topology.IsOpenEmbedding.restrictPreimage]

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

Alias of Set.restrictPreimage_isOpenEmbedding.

---

Alias of Set.restrictPreimage_isOpenEmbedding.

theorem Set.restrictPreimage_isClosedEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (s : Set β) (h : Topology.IsClosedEmbedding f) : Topology.IsClosedEmbedding (s.restrictPreimage f)

@[deprecated Set.restrictPreimage_isClosedEmbedding]

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

Alias of Set.restrictPreimage_isClosedEmbedding.

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

Alias of Set.restrictPreimage_isClosedEmbedding.

@[deprecated Topology.IsClosedEmbedding.restrictPreimage]

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

Alias of Set.restrictPreimage_isClosedEmbedding.

---

Alias of Set.restrictPreimage_isClosedEmbedding.

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 isLocallyClosed_iff_coe_preimage_of_iSup_eq_top {β : Type u_2} [TopologicalSpace β] {ι : Type u_3} {U : ι → TopologicalSpace.Opens β} (hU : iSup U = ⊤) (s : Set β) : IsLocallyClosed s ↔ ∀ (i : ι), IsLocallyClosed (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) : Topology.IsInducing f ↔ ∀ (i : ι), Topology.IsInducing ((U i).carrier.restrictPreimage f)

theorem isEmbedding_iff_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) : Topology.IsEmbedding f ↔ ∀ (i : ι), Topology.IsEmbedding ((U i).carrier.restrictPreimage f)

@[deprecated isEmbedding_iff_of_iSup_eq_top]

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) : Topology.IsEmbedding f ↔ ∀ (i : ι), Topology.IsEmbedding ((U i).carrier.restrictPreimage f)

Alias of isEmbedding_iff_of_iSup_eq_top.

theorem isOpenEmbedding_iff_isOpenEmbedding_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) : Topology.IsOpenEmbedding f ↔ ∀ (i : ι), Topology.IsOpenEmbedding ((U i).carrier.restrictPreimage f)

@[deprecated isOpenEmbedding_iff_isOpenEmbedding_of_iSup_eq_top]

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) : Topology.IsOpenEmbedding f ↔ ∀ (i : ι), Topology.IsOpenEmbedding ((U i).carrier.restrictPreimage f)

Alias of isOpenEmbedding_iff_isOpenEmbedding_of_iSup_eq_top.

theorem isClosedEmbedding_iff_isClosedEmbedding_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) : Topology.IsClosedEmbedding f ↔ ∀ (i : ι), Topology.IsClosedEmbedding ((U i).carrier.restrictPreimage f)

theorem denseRange_iff_denseRange_of_iSup_eq_top {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {f : α → β} {ι : Type u_3} {U : ι → TopologicalSpace.Opens β} (hU : iSup U = ⊤) : DenseRange f ↔ ∀ (i : ι), DenseRange ((U i).carrier.restrictPreimage f)

@[deprecated isClosedEmbedding_iff_isClosedEmbedding_of_iSup_eq_top]

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) : Topology.IsClosedEmbedding f ↔ ∀ (i : ι), Topology.IsClosedEmbedding ((U i).carrier.restrictPreimage f)

Alias of isClosedEmbedding_iff_isClosedEmbedding_of_iSup_eq_top.