Properties of maps that are local at the target or at the source.

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

• Topology.IsInducing
• IsOpenMap
• IsClosedMap
• Topology.IsEmbedding
• Topology.IsOpenEmbedding
• Topology.IsClosedEmbedding
• GeneralizingMap

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

• IsOpenMap
• GeneralizingMap

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

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

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)

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

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)

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

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)

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

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)

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

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

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

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

theorem TopologicalSpace.IsOpenCover.isOpen_iff_inter {β : Type u_2} [TopologicalSpace β] {ι : Type u_3} {U : ι → Opens β} {s : Set β} (hU : IsOpenCover U) : IsOpen s ↔ ∀ (i : ι), IsOpen (s ∩ ↑(U i))

theorem TopologicalSpace.IsOpenCover.isOpen_iff_coe_preimage {β : Type u_2} [TopologicalSpace β] {ι : Type u_3} {U : ι → Opens β} {s : Set β} (hU : IsOpenCover U) : IsOpen s ↔ ∀ (i : ι), IsOpen (Subtype.val ⁻¹' s)

theorem TopologicalSpace.IsOpenCover.isClosed_iff_coe_preimage {β : Type u_2} [TopologicalSpace β] {ι : Type u_3} {U : ι → Opens β} (hU : IsOpenCover U) {s : Set β} : IsClosed s ↔ ∀ (i : ι), IsClosed (Subtype.val ⁻¹' s)

theorem TopologicalSpace.IsOpenCover.isLocallyClosed_iff_coe_preimage {β : Type u_2} [TopologicalSpace β] {ι : Type u_3} {U : ι → Opens β} (hU : IsOpenCover U) {s : Set β} : IsLocallyClosed s ↔ ∀ (i : ι), IsLocallyClosed (Subtype.val ⁻¹' s)

theorem TopologicalSpace.IsOpenCover.isOpenMap_iff_restrictPreimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {ι : Type u_3} {U : ι → Opens β} (hU : IsOpenCover U) : IsOpenMap f ↔ ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)

theorem TopologicalSpace.IsOpenCover.isClosedMap_iff_restrictPreimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {ι : Type u_3} {U : ι → Opens β} (hU : IsOpenCover U) : IsClosedMap f ↔ ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)

theorem TopologicalSpace.IsOpenCover.isInducing_iff_restrictPreimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {ι : Type u_3} {U : ι → Opens β} (hU : IsOpenCover U) (h : Continuous f) : Topology.IsInducing f ↔ ∀ (i : ι), Topology.IsInducing ((U i).carrier.restrictPreimage f)

theorem TopologicalSpace.IsOpenCover.isEmbedding_iff_restrictPreimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {ι : Type u_3} {U : ι → Opens β} (hU : IsOpenCover U) (h : Continuous f) : Topology.IsEmbedding f ↔ ∀ (i : ι), Topology.IsEmbedding ((U i).carrier.restrictPreimage f)

theorem TopologicalSpace.IsOpenCover.isOpenEmbedding_iff_restrictPreimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {ι : Type u_3} {U : ι → Opens β} (hU : IsOpenCover U) (h : Continuous f) : Topology.IsOpenEmbedding f ↔ ∀ (i : ι), Topology.IsOpenEmbedding ((U i).carrier.restrictPreimage f)

theorem TopologicalSpace.IsOpenCover.isClosedEmbedding_iff_restrictPreimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {ι : Type u_3} {U : ι → Opens β} (hU : IsOpenCover U) (h : Continuous f) : Topology.IsClosedEmbedding f ↔ ∀ (i : ι), Topology.IsClosedEmbedding ((U i).carrier.restrictPreimage f)

theorem TopologicalSpace.IsOpenCover.isHomeomorph_iff_restrictPreimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {ι : Type u_3} {U : ι → Opens β} (hU : IsOpenCover U) (h : Continuous f) : IsHomeomorph f ↔ ∀ (i : ι), IsHomeomorph ((U i).carrier.restrictPreimage f)

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

theorem TopologicalSpace.IsOpenCover.generalizingMap_iff_restrictPreimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {ι : Type u_3} {U : ι → Opens β} (hU : IsOpenCover U) : GeneralizingMap f ↔ ∀ (i : ι), GeneralizingMap ((U i).carrier.restrictPreimage f)

theorem TopologicalSpace.IsOpenCover.isOpenMap_iff_comp {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {ι : Type u_3} {U : ι → Opens α} (hU : IsOpenCover U) : IsOpenMap f ↔ ∀ (i : ι), IsOpenMap (f ∘ Subtype.val)

theorem TopologicalSpace.IsOpenCover.generalizingMap_iff_comp {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {ι : Type u_3} {U : ι → Opens α} (hU : IsOpenCover U) : GeneralizingMap f ↔ ∀ (i : ι), GeneralizingMap (f ∘ Subtype.val)

theorem isEmbedding_of_iSup_eq_top_of_preimage_subset_range {X : Type u_6} {Y : Type u_7} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : Continuous f) {ι : Type u_4} (U : ι → TopologicalSpace.Opens Y) (hU : Set.range f ⊆ ↑(iSup U)) (V : ι → Type u_5) [(i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X) (hiV : ∀ (i : ι), Continuous (iV i)) (hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ Set.range (iV i)) (hV' : ∀ (i : ι), Topology.IsEmbedding (f ∘ iV i)) : Topology.IsEmbedding f

Given a continuous map f : X → Y between topological spaces. Suppose we have an open cover U i of the range of f, and a family of continuous maps V i → X whose images are a cover of X that is coarser than the pullback of U under f. To check that f is an embedding it suffices to check that V i → Y is an embedding for all i.