SpectralMap.spectral'
theorem SpectralMap.spectral' :
∀ {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (self : SpectralMap α β),
IsSpectralMap self.toFun
This theorem states that for any two types `α` and `β`, each with a topological space structure, and any instance `self` of a `SpectralMap` from `α` to `β`, the function `toFun` (which is a member of the `SpectralMap` structure) is a spectral map. In the context of mathematics, a spectral map is a function that preserves the properties of a spectral space, which is a special kind of topological space.
More concisely: For any spectral maps `self` from topological spaces `α` to `β`, the function `toFun` is a spectral map.
|
IsSpectralMap.isCompact_preimage_of_isOpen
theorem IsSpectralMap.isCompact_preimage_of_isOpen :
∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
IsSpectralMap f → ∀ ⦃s : Set β⦄, IsOpen s → IsCompact s → IsCompact (f ⁻¹' s)
The theorem `IsSpectralMap.isCompact_preimage_of_isOpen` states that for any two topological spaces `α` and `β` and a function `f` mapping from `α` to `β`, if `f` is a spectral map (i.e., it is continuous and the preimage of every compact open set is compact open), then for any open and compact set `s` in `β`, the preimage of `s` under the function `f` is also compact. This theorem therefore captures a preservation property of spectral maps with respect to compactness under the operation of taking preimages.
More concisely: If `f` is a spectral map from a topological space `α` to `β`, then the preimage of any open and compact set `s` in `β` under `f` is a compact subset of `α`.
|
SpectralMap.ext
theorem SpectralMap.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : SpectralMap α β},
(∀ (a : α), f a = g a) → f = g
This theorem, named `SpectralMap.ext`, states that for any two spectral maps `f` and `g` from a topological space `α` to another topological space `β`, if for every element `a` in `α` the application of `f` and `g` to `a` results in the same element in `β`, then these two spectral maps `f` and `g` are indeed the same. In other words, it ensures the extensionality of spectral maps in the context of topology: two spectral maps are equal if they map every point to the same image.
More concisely: If two spectral maps from one topological space to another have the same image for every point, then they are equal.
|
SpectralMapClass.map_spectral
theorem SpectralMapClass.map_spectral :
∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : FunLike F α β] [self : SpectralMapClass F α β] (f : F), IsSpectralMap ⇑f
The theorem `SpectralMapClass.map_spectral` states that for any types `F`, `α`, and `β`, where `α` and `β` are topological spaces, and `F` is a function-like class from `α` to `β`, then for any instance of `SpectralMapClass` for `F`, `α`, and `β`, any function of type `F` is a spectral map. In other words, if we have a function `f` of type `F` (which we know can be treated as a function from `α` to `β` because `F` is `FunLike`), then the function `f` is a spectral map, as formalized by the typeclass predicate `IsSpectralMap`.
More concisely: For any function-like class `F` from topological spaces `α` to `β` with an instance of `SpectralMapClass`, any `F`-function is a spectral map.
|
IsSpectralMap.continuous
theorem IsSpectralMap.continuous :
∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
IsSpectralMap f → Continuous f
This theorem states that for any two types `α` and `β`, each equipped with a topological space structure (`inst` and `inst_1`, respectively), if a function `f` from `α` to `β` is a spectral map (`IsSpectralMap f`), then that function `f` is continuous (`Continuous f`). In other words, spectral maps preserve the property of continuity in the context of topological spaces.
More concisely: If `f` is a spectral map between topological spaces `α` and `β`, then `f` is continuous.
|