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_isInducing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (s : Set β) (h : IsInducing f) :

IsInducing (s.restrictPreimage f)

source

@[deprecated Set.restrictPreimage_isInducing]

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

IsInducing (s.restrictPreimage f)

Alias of Set.restrictPreimage_isInducing.

source

theorem 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.

source

@[deprecated IsInducing.restrictPreimage]

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

IsInducing (s.restrictPreimage f)

Alias of Set.restrictPreimage_isInducing.

source

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

IsEmbedding (s.restrictPreimage f)

source

@[deprecated Set.restrictPreimage_isEmbedding]

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

IsEmbedding (s.restrictPreimage f)

Alias of Set.restrictPreimage_isEmbedding.

source

theorem 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.

source

@[deprecated IsEmbedding.restrictPreimage]

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

IsEmbedding (s.restrictPreimage f)

Alias of Set.restrictPreimage_isEmbedding.

source

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

IsOpenEmbedding (s.restrictPreimage f)

source

@[deprecated Set.restrictPreimage_isOpenEmbedding]

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

IsOpenEmbedding (s.restrictPreimage f)

Alias of Set.restrictPreimage_isOpenEmbedding.

source

theorem 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.

source

@[deprecated IsOpenEmbedding.restrictPreimage]

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

IsOpenEmbedding (s.restrictPreimage f)

Alias of Set.restrictPreimage_isOpenEmbedding.

source

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

IsClosedEmbedding (s.restrictPreimage f)

source

@[deprecated Set.restrictPreimage_isClosedEmbedding]

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

IsClosedEmbedding (s.restrictPreimage f)

Alias of Set.restrictPreimage_isClosedEmbedding.

source

theorem 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.

source

@[deprecated IsClosedEmbedding.restrictPreimage]

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

IsClosedEmbedding (s.restrictPreimage f)

Alias of Set.restrictPreimage_isClosedEmbedding.

source

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

IsClosedMap (s.restrictPreimage f)

source

@[deprecated]

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

IsClosedMap (s.restrictPreimage f)

source

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

IsOpenMap (s.restrictPreimage f)

source

@[deprecated]

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

IsOpenMap (s.restrictPreimage f)

source

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))

source

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)

source

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)

source

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)

source

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)

source

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)

source

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) :

IsInducing f ↔ ∀ (i : ι), IsInducing ((U i).carrier.restrictPreimage f)

source

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) :

IsEmbedding f ↔ ∀ (i : ι), IsEmbedding ((U i).carrier.restrictPreimage f)

source

@[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) :

IsEmbedding f ↔ ∀ (i : ι), IsEmbedding ((U i).carrier.restrictPreimage f)

Alias of isEmbedding_iff_of_iSup_eq_top.

source

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) :

IsOpenEmbedding f ↔ ∀ (i : ι), IsOpenEmbedding ((U i).carrier.restrictPreimage f)

source

@[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) :

IsOpenEmbedding f ↔ ∀ (i : ι), IsOpenEmbedding ((U i).carrier.restrictPreimage f)

Alias of isOpenEmbedding_iff_isOpenEmbedding_of_iSup_eq_top.

source

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) :

IsClosedEmbedding f ↔ ∀ (i : ι), IsClosedEmbedding ((U i).carrier.restrictPreimage f)

source

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)

source

@[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) :

IsClosedEmbedding f ↔ ∀ (i : ι), IsClosedEmbedding ((U i).carrier.restrictPreimage f)

Alias of isClosedEmbedding_iff_isClosedEmbedding_of_iSup_eq_top.

Documentation

Mathlib.Topology.LocalAtTarget

Properties of maps that are local at the target. #