CocompactMapClass.cocompact_tendsto
theorem CocompactMapClass.cocompact_tendsto :
∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} [inst : TopologicalSpace α]
[inst_1 : TopologicalSpace β] [inst_2 : FunLike F α β] [self : CocompactMapClass F α β] (f : F),
Filter.Tendsto (⇑f) (Filter.cocompact α) (Filter.cocompact β)
This theorem states that for any types `α` and `β` that have topological spaces, any type `F` that is a function-like from `α` to `β`, and any instance of `CocompactMapClass` for `F`, `α`, and `β`, any function `f` of type `F` has the property that it maps the cocompact filter on `α` to the cocompact filter on `β`. In other words, if we take any set in `β` that is the complement of a compact set, take its preimage under `f`, it will be in the cocompact filter on `α`. This is a statement about the limit of function `f` between the cocompact filters on `α` and `β`.
More concisely: Given functions `F` from type `α` to type `β` that are continuous and have a cocompact map class instance, any such function `f` maps the cocompact filter on `α` to the cocompact filter on `β`.
|
CocompactMap.isCompact_preimage
theorem CocompactMap.isCompact_preimage :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : T2Space β]
(f : CocompactMap α β) ⦃s : Set β⦄, IsCompact s → IsCompact (⇑f ⁻¹' s)
This theorem states that, given a fixed cocompact continuous map 'f' from a topological space 'α' to a Hausdorff space 'β', if 's' is a compact set in 'β', then the preimage of 's' under the map 'f' is compact in 'α'.
In other words, if we have a cocompact continuous map from one topological space to another, where the codomain is a Hausdorff space, then the preimage through this map of any compact set in the codomain is also compact in the domain. This theorem is an important result in the field of topological spaces and the concept of compactness.
More concisely: Given a cocompact continuous map from a topological space to a Hausdorff space, the preimage of any compact set is compact.
|
CocompactMap.cocompact_tendsto'
theorem CocompactMap.cocompact_tendsto' :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (self : CocompactMap α β),
Filter.Tendsto self.toFun (Filter.cocompact α) (Filter.cocompact β)
This theorem states that for any given `CocompactMap` from a topological space `α` to another topological space `β`, the function represented by the `CocompactMap` has the property that it tends to take cocompact sets in `α` to cocompact sets in `β`. Here, "cocompact" refers to the filter generated by the complements of compact sets, and "tends to" is defined in terms of the pre-images of neighborhoods.
More concisely: For any CocompactMap f from topological space α to topological space β, the preimage of every cocompact set in β under f is a cocompact set in α.
|