isProperMap_id
theorem isProperMap_id : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsProperMap id
This theorem, `isProperMap_id`, states that for any type `X` with a topology (i.e., it is a topological space), the identity map is a proper map. In the context of topology, a proper map is one where the preimage of a compact set is also compact. This theorem says that this property holds when the map in question is the identity map, which maps each element of the set to itself.
More concisely: The identity map is a proper map on any topological space.
|
IsProperMap.prod_map
theorem IsProperMap.prod_map :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {W : Type u_4} [inst : TopologicalSpace X]
[inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] {f : X → Y} {g : Z → W},
IsProperMap f → IsProperMap g → IsProperMap (Prod.map f g)
The theorem `IsProperMap.prod_map` states that for any four types `X`, `Y`, `Z`, and `W`, which each have a topological space structure, if we have two functions `f : X → Y` and `g : Z → W` that are both proper maps, then the function `Prod.map f g`, which creates a pair by mapping `f` on the first component and `g` on the second component, is also a proper map. In mathematical terms, given two proper maps between topological spaces, the product of these maps is also a proper map.
More concisely: If `f : X → Y` and `g : Z → W` are proper maps between topological spaces, then their product `Prod.map f g : X × Z → Y × W` is also a proper map.
|
isProperMap_iff_isClosedMap_and_tendsto_cofinite
theorem isProperMap_iff_isClosedMap_and_tendsto_cofinite :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
[inst_2 : T1Space Y],
IsProperMap f ↔ Continuous f ∧ IsClosedMap f ∧ Filter.Tendsto f (Filter.cocompact X) Filter.cofinite
This theorem, `isProperMap_iff_isClosedMap_and_tendsto_cofinite`, is stating a condition equivalent to a function being a proper map in terms of other topological properties. Specifically, a function `f` from a type `X` with a topological space structure to a type `Y` with a topological space and a `T1` space structure is a proper map if and only if it satisfies three conditions: it is continuous, it is a closed map (i.e., the image of any closed set in `X` is also closed in `Y`), and it has the property that the filter map `f` tends from the cocompact filter on `X` to the cofinite filter (i.e., for every set in the cofinite filter, the preimage of that set under `f` is in the cocompact filter on `X`). The cocompact filter on `X` is defined as the filter generated by complements to compact sets, and the cofinite filter is the filter of subsets whose complements are finite.
More concisely: A continuous function between topological spaces is proper (i.e., its image of every closed set is closed and its preimage of every set in the cocompact filter is in the cocompact filter) if and only if it is both a closed map and its filter map tends to the cofinite filter.
|
Homeomorph.isProperMap
theorem Homeomorph.isProperMap :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y),
IsProperMap ⇑e
This theorem states that for any two types `X` and `Y`, which have topological space structures, if there exists a homeomorphism (a bijective, continuous mapping whose inverse is also continuous) between `X` and `Y`, then the function represented by this homeomorphism is a proper map. A proper map, in this context, means a function that is precompact, i.e., the preimage of a compact set is also compact.
More concisely: If `X` and `Y` are topological spaces with a homeomorphism between them, then the homeomorphism is a proper map.
|
isProperMap_iff_universally_closed
theorem isProperMap_iff_universally_closed :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
IsProperMap f ↔ Continuous f ∧ ∀ (Z : Type u) [inst_2 : TopologicalSpace Z], IsClosedMap (Prod.map f id)
The theorem `isProperMap_iff_universally_closed` states that a map `f` from a topological space `X` to another topological space `Y` is proper if and only if it is both continuous and universally closed. A map is said to be universally closed if, for any topological space `Z` in the same universe as `X`, the map `Prod.map f id` from the product space `X × Z` to `Y × Z` is a closed map. Here, `Prod.map f id` is a function that applies `f` to the first component of a pair and the identity function `id` to the second component. This is the definition of properness as given by N. Bourbaki in *General Topology*.
More concisely: A map between topological spaces is proper if and only if it is both continuous and universally closes the product with the identity map.
|
IsProperMap.isCompact_preimage
theorem IsProperMap.isCompact_preimage :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
IsProperMap f → ∀ {K : Set Y}, IsCompact K → IsCompact (f ⁻¹' K)
The theorem `IsProperMap.isCompact_preimage` states that for any two types `X` and `Y` with topological space structures, and any function `f` from `X` to `Y`, if `f` is a proper map then for any set `K` of type `Y` that is compact, the preimage of `K` under `f` (i.e., the set of all elements in `X` that map to elements in `K` under `f`) is also compact. This property completely characterises a proper map when the codomain is locally compact and Hausdorff, as shown in `isProperMap_iff_isCompact_preimage`.
More concisely: If `f` is a proper map from a topological space `X` to another topological space `Y`, then the preimage of any compact subset `K` of `Y` under `f` is a compact subset of `X`.
|
isProperMap_iff_ultrafilter
theorem isProperMap_iff_ultrafilter :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
IsProperMap f ↔
Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Filter.Tendsto f (↑𝒰) (nhds y) → ∃ x, f x = y ∧ ↑𝒰 ≤ nhds x
This theorem characterizes proper maps in terms of ultrafilters. In particular, it states that for any given types `X` and `Y` equipped with topological spaces, and a function `f` from `X` to `Y`, `f` is a proper map if and only if two conditions are met. First, `f` must be continuous. Second, for any ultrafilter `𝒰` on `X` and any `y` in `Y`, if `f` tends towards `y` under the ultrafilter `𝒰`, then there exists an `x` in `X` such that `f(x)` equals `y` and the ultrafilter `𝒰` is less than or equal to the neighborhood filter of `x`. This theorem essentially provides a characterization of proper maps using the concepts of continuity and ultrafilters.
More concisely: A function between topological spaces is proper if and only if it is continuous and for every ultrafilter on the domain and any point in the codomain, the ultrafilter witnesses convergence if and only if there exists a point in the domain mapped to that point with the ultrafilter being contained in the neighborhood filter of that point.
|
IsProperMap.ultrafilter_le_nhds_of_tendsto
theorem IsProperMap.ultrafilter_le_nhds_of_tendsto :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
IsProperMap f → ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Filter.Tendsto f (↑𝒰) (nhds y) → ∃ x, f x = y ∧ ↑𝒰 ≤ nhds x
This theorem states that if a function `f` from a topological space `X` to another topological space `Y` is proper and converges to a point `y` along some ultrafilter `𝒰` on `X`, then there exists a point `x` in `X` such that `f(x) = y` and the ultrafilter `𝒰` converges to `x`. In other words, the ultrafilter `𝒰` is dominated by the neighborhood filter of `x`.
More concisely: If a proper function `f` from a topological space `X` to another topological space `Y` converges to a point `y` along an ultrafilter `𝒰` on `X`, then there exists a point `x` in `X` with `f(x) = y` and `𝒰` converges to `x`.
|
IsProperMap.continuous
theorem IsProperMap.continuous :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
IsProperMap f → Continuous f
This theorem states that for any two types `X` and `Y`, which have the structure of topological spaces, and for any function `f` from `X` to `Y`, if `f` is a proper map (as per the definition of properness in topology), then `f` is also continuous. In mathematical terms, this theorem is verifying that every proper map between two topological spaces is a continuous function.
More concisely: Every proper map between two topological spaces is a continuous function.
|
isProperMap_iff_isClosedMap_and_compact_fibers
theorem isProperMap_iff_isClosedMap_and_compact_fibers :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
IsProperMap f ↔ Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
The theorem `isProperMap_iff_isClosedMap_and_compact_fibers` states that for any given function `f` mapping from one topological space `X` to another topological space `Y`, the function `f` is a proper map if and only if it satisfies three conditions:
1. The function `f` is continuous.
2. The function `f` is a closed map, which means that it maps any closed subset of `X` to a closed subset of `Y`.
3. For every element `y` in `Y`, the preimage of the singleton set `{y}` under `f` (denoted as `(f ⁻¹' {y})`) is a compact set in `X`. A set is said to be compact if for every nontrivial filter that contains this set, there exists an element in the set such that every set of the filter meets every neighbourhood of this element.
More concisely: A function between topological spaces is proper if and only if it is continuous, closes closed sets, and maps each fiber to a compact set.
|
isProperMap_iff_isCompact_preimage
theorem isProperMap_iff_isCompact_preimage :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
[inst_2 : T2Space Y] [inst_3 : WeaklyLocallyCompactSpace Y],
IsProperMap f ↔ Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
The theorem `isProperMap_iff_isCompact_preimage` states that for all types `X` and `Y` with respective topological spaces and for any function `f` from `X` to `Y`, if `Y` is a Hausdorff space (i.e., any two distinct points in `Y` have disjoint neighborhoods) and is locally compact (i.e., every point in `Y` has a compact neighborhood), then `f` is a proper map if and only if `f` is continuous and the pre-image of any compact set in `Y` under `f` is also a compact set in `X`. In this context, a map is said to be proper if the preimage of a compact set is compact. Hence, the theorem essentially provides the conditions under which a map is proper in terms of continuity and compactness of the pre-image of sets.
More concisely: A continuous function from a type equipped with a topology, representing a Hausdorff and locally compact space, to another type with the same properties is proper if and only if the preimage of any compact set is compact.
|
IsProperMap.clusterPt_of_mapClusterPt
theorem IsProperMap.clusterPt_of_mapClusterPt :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
IsProperMap f → ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
This theorem states that for any type `X` and `Y` with associated topological spaces, given a function `f` from `X` to `Y` that is a proper map, for any filter `ℱ` on `X` and any point `y` in `Y`, if `y` is a cluster point of the image of the filter `ℱ` under `f`, then there exists a point `x` in `X` such that `f(x) = y` and `x` is a cluster point of `ℱ`. In simple terms, if `y` is a cluster point of the mapped filter, then `y` is the image of some cluster point of the original filter under the function `f`.
More concisely: Given a proper map `f` between topological spaces `X` and `Y`, if a point `y` in `Y` is a cluster point of the image of any filter on `X` under `f`, then there exists a cluster point `x` in `X` such that `f(x) = y`.
|
isProperMap_iff_clusterPt
theorem isProperMap_iff_clusterPt :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
IsProperMap f ↔ Continuous f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
The theorem `isProperMap_iff_clusterPt` provides a characterization of proper maps in terms of cluster points. Given types `X` and `Y` with topological spaces, it states that for a function `f : X → Y`, `f` is a proper map if and only if `f` is continuous and for every filter `ℱ` in `X` and point `y` in `Y`, if `y` is a cluster point of the image of `ℱ` under `f`, there exists a point `x` in `X` such that `f(x) = y` and `x` is a cluster point of `ℱ`. Here, a point `x` is a cluster point of a filter `ℱ` in `X` if the intersection of `ℱ` and the neighborhood of `x` is not empty. Similarly, a point `y` is a cluster point of the image of `ℱ` under `f` if the intersection of the image of `ℱ` under `f` and the neighborhood of `y` is not empty.
More concisely: A function between topological spaces is proper if and only if it is continuous and preserves cluster points, that is, for every filter on the domain and every cluster point of its image, there exists a cluster point in the domain mapping to that image point.
|
IsProperMap.universally_closed
theorem IsProperMap.universally_closed :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} (Z : Type u_6)
[inst_2 : TopologicalSpace Z], IsProperMap f → IsClosedMap (Prod.map f id)
The theorem `IsProperMap.universally_closed` states that a proper map, denoted by `f : X → Y`, has a universal closed property. This means that for any given topological space `Z`, the newly formed map `Prod.map f id : X × Z → Y × Z` is a closed map. In other words, when you map pairs `(x, z)` to `(f(x), z)` for all `x` in `X` and `z` in `Z`, the image of a closed set in `X × Z` under this map is still a closed set in `Y × Z`. The theorem `isProperMap_iff_universally_closed` will later show that the proper maps are precisely the continuous maps that possess this universal closure property, but this theorem is easier to use because it permits `Z` to exist in any universe.
More concisely: A proper map from X to Y induces a closed map from X × Z to Y × Z for any topological space Z.
|
isProperMap_iff_tendsto_cocompact
theorem isProperMap_iff_tendsto_cocompact :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
[inst_2 : T2Space Y] [inst_3 : WeaklyLocallyCompactSpace Y],
IsProperMap f ↔ Continuous f ∧ Filter.Tendsto f (Filter.cocompact X) (Filter.cocompact Y)
The theorem `isProperMap_iff_tendsto_cocompact` states that for any two types `X` and `Y` with their respective topological spaces, and a function `f` from `X` to `Y`, given that `Y` is a T2 space and a weakly locally compact space, then `f` is a proper map if and only if `f` is continuous and the limit of `f` as `X` approaches the filter generated by complements to compact sets in `X` is the filter generated by complements to compact sets in `Y`. This theorem provides a characterization of proper maps in terms of limit and continuity properties.
More concisely: A continuous function between two topological spaces `X` and `Y`, where `Y` is a T2 and weakly locally compact space, is a proper map if and only if the limit of its image as `X` approaches the filter of complements to compact sets is the filter of complements to compact sets in `Y`.
|
isProperMap_iff_isClosedMap_filter
theorem isProperMap_iff_isClosedMap_filter :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
IsProperMap f ↔ Continuous f ∧ IsClosedMap (Prod.map f id)
The theorem `isProperMap_iff_isClosedMap_filter` states that for any two types `X` and `Y` equipped with the structure of topological spaces, a map `f : X → Y` is a proper map if and only if the following two conditions are met:
1) `f` is a continuous function, and
2) the function that applies `f` to the first component of a pair and leaves the second component unchanged (formally, the function `Prod.map f id : X × Filter X → Y × Filter X`) is a closed map.
This theorem provides a more specific context for verifying the propriety of a map `f`, requiring to check only one space rather than universally across all spaces. However, in most cases, this distinction does not have a significant impact.
More concisely: A map between topological spaces is proper if and only if it is continuous and the corresponding function on product spaces with the identity function is a closed map.
|
Continuous.isProperMap
theorem Continuous.isProperMap :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
[inst_2 : CompactSpace X] [inst_3 : T2Space Y], Continuous f → IsProperMap f
The theorem states that for any continuous function 'f' mapping from a compact space 'X' to a T2 space 'Y', 'f' is a proper map. Here, 'X' and 'Y' are types endowed with topological spaces, 'X' is a compact space and 'Y' is a T2 space (also known as a Hausdorff space). The continuity of 'f' guarantees that 'f' is a proper map, which intuitively means that the preimage of a compact set under 'f' is also compact.
More concisely: A continuous function from a compact space to a Hausdorff space is proper.
|
IsProperMap.pi_map
theorem IsProperMap.pi_map :
∀ {ι : Type u_5} {X : ι → Type u_6} {Y : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (X i)]
[inst_1 : (i : ι) → TopologicalSpace (Y i)] {f : (i : ι) → X i → Y i},
(∀ (i : ι), IsProperMap (f i)) → IsProperMap fun x i => f i (x i)
This theorem states that if you have an indexed family of mappings, each from a topological space `X i` to another topological space `Y i` indexed by `ι`, and if each of these mappings is "proper" (in the sense used in topology), then the product function -- which takes an element from the product of the `X i`s and returns an element in the product of the `Y i`s by applying the corresponding function to each component -- is also a proper map.
More concisely: If each mapping in an indexed family from a topological space to another, where the mappings are proper, then the product mapping is proper.
|
isProperMap_iff_isClosedMap_ultrafilter
theorem isProperMap_iff_isClosedMap_ultrafilter :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
IsProperMap f ↔ Continuous f ∧ IsClosedMap (Prod.map f id)
A function `f` from a topological space `X` to another topological space `Y` is said to be proper if and only if it is continuous and the function mapped from `X × Ultrafilter X` to `Y × Ultrafilter X` by `Prod.map f id` is a closed map. This implies that we only need to verify these conditions in one space to establish the properness of `f`. This criterion is stronger than the universally closed map criterion, although in most cases, the distinction doesn't matter. Here, `Ultrafilter X` denotes the ultrafilter on the topological space `X`, and `id` is the identity function.
More concisely: A function between topological spaces is proper if and only if it is continuous and its product with the identity function is a closed map from the function's domain space with its associated ultrafilter topology to the codomain space with its associated ultrafilter topology.
|
IsProperMap.isClosedMap
theorem IsProperMap.isClosedMap :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
IsProperMap f → IsClosedMap f
This theorem states that for any types `X` and `Y`, which are both topological spaces, if `f` is a proper map from `X` to `Y`, then `f` is a closed map. A proper map being "closed" means that for any closed set `U` in `X`, its image `f(U)` is also a closed set in `Y`. In other words, a proper map preserves the property of being closed under the mapping.
More concisely: If `f` is a proper map between topological spaces `X` and `Y`, then the image of every closed set in `X` under `f` is a closed set in `Y`.
|