ProperConstVAdd.isProperMap_vadd
theorem ProperConstVAdd.isProperMap_vadd :
∀ {M : Type u_1} {X : Type u_2} [inst : VAdd M X] [inst_1 : TopologicalSpace X] [self : ProperConstVAdd M X]
(c : M), IsProperMap fun x => c +ᵥ x
The theorem `ProperConstVAdd.isProperMap_vadd` states that for any types `M` and `X`, where `M` has an operation of vector addition (`VAdd`) with `X` and `X` has a topological space structure, if `M` and `X` satisfy the `ProperConstVAdd` condition (which generally has to do with the continuity and boundedness of the vector addition operation), then for any element `c` in `M`, the function that adds `c` to any element of `X` (`fun x => c +ᵥ x`) is a proper map - a continuous map that pulls back compact sets to compact sets in topological space.
More concisely: Given types `M` and `X` with `M` having vector addition with `X`, and `M` and `X` satisfying the `ProperConstVAdd` condition, for any `c` in `M`, the function `fun x => c +ᵥ x` is a continuous, compact-valued function that maps compact sets in `X` to compact sets in `X`.
|
ProperConstSMul.isProperMap_smul
theorem ProperConstSMul.isProperMap_smul :
∀ {M : Type u_1} {X : Type u_2} [inst : SMul M X] [inst_1 : TopologicalSpace X] [self : ProperConstSMul M X]
(c : M), IsProperMap fun x => c • x
This theorem states that for a given scalar `c` of type `M`, the function that multiplies every element `x` of type `X` by `c` (denoted as `c • x`) is a proper map. This is under the condition that `X` is a topological space and `M` and `X` are equipped with an operation of scalar multiplication (denoted as `SMul M X`). The `ProperConstSMul` class is a class that contains `M` and `X` where `M` can be properly scaled on `X`.
More concisely: Given a topological space X and a scalar M equipped with scalar multiplication, the function c => x => c * x is a proper map from M to the continuous functions from X to X.
|
IsCompact.preimage_vadd
theorem IsCompact.preimage_vadd :
∀ {M : Type u_1} {X : Type u_2} [inst : VAdd M X] [inst_1 : TopologicalSpace X] [inst_2 : ProperConstVAdd M X]
{s : Set X}, IsCompact s → ∀ (c : M), IsCompact ((fun x => c +ᵥ x) ⁻¹' s)
The theorem `IsCompact.preimage_vadd` states that for any set of elements of type `X` that is compact in the context of a topological space, and an operator `+ᵥ` from a type `M` to the type `X` that has the property of proper constant vector addition, the preimage of this set under the action of `(c +ᵥ ·)` is also a compact set. In other words, given a compact set `s` and a constant `c` of type `M`, the set of elements that, when `c +ᵥ` is applied to them, map into `s`, is also compact. This is a property related to the relationship between compactness and continuous functions in topology.
More concisely: If `s : Set X` is a compact subset of a topological space `X` and `+ᵥ : M -> X` is a proper constant vector addition operation, then `(c => s).preimage (c +ᵥ)` is a compact subset of `M` for all `c : M`.
|
isProperMap_smul
theorem isProperMap_smul :
∀ {M : Type u_1} (c : M) (X : Type u_2) [inst : SMul M X] [inst_1 : TopologicalSpace X] [h : ProperConstSMul M X],
IsProperMap fun x => c • x
The theorem `isProperMap_smul` states that for any type `M`, any element `c` of `M`, and any type `X` such that `X` has a scalar multiplication operation by `M` and `X` has a topology, if `M` scalar multiplies `X` properly (specified by `ProperConstSMul M X`), then the function `fun x => c • x` is a proper map. In other words, scalar multiplication by a constant is a proper map, given that the scalar multiplication is properly defined. The term "proper map" in topology typically refers to a continuous function between topological spaces that is precompact, that is, the preimage of a compact set is also compact.
More concisely: If `M` properly scalar multiplies a topological space `X`, then the function `x => c • x` is a continuous function for any constant `c` in `M`.
|
IsCompact.preimage_smul
theorem IsCompact.preimage_smul :
∀ {M : Type u_1} {X : Type u_2} [inst : SMul M X] [inst_1 : TopologicalSpace X] [inst_2 : ProperConstSMul M X]
{s : Set X}, IsCompact s → ∀ (c : M), IsCompact ((fun x => c • x) ⁻¹' s)
The theorem `IsCompact.preimage_smul` states that for any given set `s` of a type `X` that has a topological space structure and a scalar multiplication operation (denoted `•`), if `s` is a compact set, then the preimage of `s` under the scalar multiplication by any element `c` of a type `M` that has a proper constant scalar multiplication action on `X` is also a compact set. In other words, compactness is preserved under scalar multiplication preimage for a proper constant scalar multiplication action.
More concisely: If `s` is a compact subset of a topological space `X` with a proper constant scalar multiplication operation, then the preimage of `s` under scalar multiplication by any element in the multiplication domain is also a compact subset of `X`.
|
isProperMap_vadd
theorem isProperMap_vadd :
∀ {M : Type u_1} (c : M) (X : Type u_2) [inst : VAdd M X] [inst_1 : TopologicalSpace X] [h : ProperConstVAdd M X],
IsProperMap fun x => c +ᵥ x
This theorem states that for any type `M`, any type `X` that supports a vector addition operation with `M` (`[VAdd M X]`), any instance `c` of `M`, and any `X` that is a topological space (`[TopologicalSpace X]`), if `M` and `X` satisfy the `ProperConstVAdd` condition, then the function that adds `c` to every element of `X` (`fun x => c +ᵥ x`) is a proper map. A proper map in topology is one that is precompact, meaning the preimage of every compact set is also compact. The `ProperConstVAdd` condition is a specific property related to the vector addition operation.
More concisely: Given a type `M` with a `VAdd` operation, a topological space `X`, an instance `c` of `M`, and assuming `M` and `X` satisfy the `ProperConstVAdd` condition, the constant vector addition function `x => c +ᵥ x` is a proper map from `X` to `M`.
|