tendsto_const_smul_iff
theorem tendsto_const_smul_iff :
∀ {α : Type u_2} {β : Type u_3} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G]
[inst_2 : MulAction G α] [inst_3 : ContinuousConstSMul G α] {f : β → α} {l : Filter β} {a : α} (c : G),
Filter.Tendsto (fun x => c • f x) l (nhds (c • a)) ↔ Filter.Tendsto f l (nhds a)
The theorem `tendsto_const_smul_iff` states that for any types `α`, `β`, and `G`, where `α` has a topological space structure, `G` is a group, and `α` has a multiplication action by `G` with continuous constant scalar multiplication, for any function `f` from `β` to `α`, any filter `l` on `β`, any element `a` from `α`, and any element `c` from `G`, the function that to each `x` from the domain associates `c` multiplied by `f(x)` tends toward the neighborhood of `c` multiplied by `a` as `x` tends toward the elements of the filter `l`, if and only if the function `f` tends toward the neighborhood of `a` as `x` tends toward the elements of the filter `l`. In other words, the limit of the function `f` when multiplied by a constant scalar `c` is just `c` multiplied by the limit of `f`.
More concisely: For any type `α` with a topological space structure, group `G` with continuous constant scalar multiplication action on `α`, function `f` from `β` to `α`, filter `l` on `β`, element `a` from `α`, and `c` from `G`, the function `x ↦ c * f(x)` tends to the neighborhood of `a * c` as `x` tends to the elements in `l` if and only if `f` tends to the neighborhood of `a`.
|
ContinuousConstVAdd.secondCountableTopology
theorem ContinuousConstVAdd.secondCountableTopology :
∀ {Γ : Type u_4} [inst : AddGroup Γ] {T : Type u_5} [inst_1 : TopologicalSpace T] [inst_2 : AddAction Γ T]
[inst_3 : SecondCountableTopology T] [inst_4 : ContinuousConstVAdd Γ T],
SecondCountableTopology (Quotient (AddAction.orbitRel Γ T))
The theorem `ContinuousConstVAdd.secondCountableTopology` states that for any additive group `Γ`, and any type `T` that has a topological space structure, an additive action of `Γ` on `T`, a second countable topology structure and a continuous constant-additive group action, the quotient space formed by the equivalence classes under the relation "in the same orbit of the additive group action" also has a second countable topology structure. In other words, the orbit space of a second countable topological space under an additive group action is also second countable. This is especially relevant for studying the properties of quotient spaces in algebraic and topological contexts.
More concisely: The quotient space of a second countable topological space by an additive group action with a continuous and constant-additive group action is also second countable.
|
isClosedMap_smul₀
theorem isClosedMap_smul₀ :
∀ {G₀ : Type u_4} [inst : GroupWithZero G₀] {E : Type u_5} [inst_1 : Zero E] [inst_2 : MulActionWithZero G₀ E]
[inst_3 : TopologicalSpace E] [inst_4 : T1Space E] [inst_5 : ContinuousConstSMul G₀ E] (c : G₀),
IsClosedMap fun x => c • x
The theorem `isClosedMap_smul₀` states that for any type `G₀` equipped with a group with zero structure, any type `E` equipped with a zero element, a multiplication action with zero, a topological space structure, a T1 space structure, and the ability to continuously scale by constants from `G₀`, then for any constant `c` from `G₀`, the function that maps each element `x` from `E` to `c • x` (where `•` denotes the multiplication action) is a closed map. This means the image of any closed set under this function is also a closed set.
Note that there is a related lemma `isClosedMap_smul_left` in the `Analysis.NormedSpace.FiniteDimension` module which states that `smul` is a closed map in the first argument, but it requires that `E` is a normed space over a complete normed field.
More concisely: Given a topological space `(E, τ)` equipped with a multiplication action by a group `G₀` with zero, such that `(G₀, ⋅, 0)` is a group with zero structure, `E` has a zero element and is a T1 space, and `G₀` can continuously scale elements in `E`, then for any `c` in `G₀`, the function `x mapsto c • x` is a closed map.
|
Filter.Tendsto.const_smul
theorem Filter.Tendsto.const_smul :
∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SMul M α]
[inst_2 : ContinuousConstSMul M α] {f : β → α} {l : Filter β} {a : α},
Filter.Tendsto f l (nhds a) → ∀ (c : M), Filter.Tendsto (fun x => c • f x) l (nhds (c • a))
This theorem, `Filter.Tendsto.const_smul`, states that for any topological space `α` which has a scalar multiplication operation with a certain type `M`, and for which the scalar multiplication operation with a constant is continuous, if a function `f` from `β` to `α` tends to a limit `a` as we approach according to a filter `l`, then the function resulting from scaling `f` with a constant `c` also tends to a limit, specifically `c` scaled with `a`, according to the same filter. Essentially, it guarantees that the limit of the scaled function is the scaled limit when scalar multiplication is continuous.
More concisely: If `f : β → α` tends to `a ∈ α` as filters under a topology on `α` with scalar multiplication `M → α → α` and continuous scalar multiplication by a constant, then `c → (x ↦ c * f x)` tends to `c * a`.
|
IsOpen.vadd
theorem IsOpen.vadd :
∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
[inst_3 : ContinuousConstVAdd G α] {s : Set α}, IsOpen s → ∀ (c : G), IsOpen (c +ᵥ s)
The `IsOpen.vadd` theorem states that for any set `s` in a topological space `α`, if `s` is open, then the set resulting from adding a constant value `c` from an additive group `G` to each element in the set `s` is also open. This requires `α` to be a topological space, `G` to be an additive group, an additive action of `G` on `α`, and the constant vector addition to be continuous. This theorem, therefore, establishes the preservation of openness under constant vector addition in this context.
More concisely: If `α` is a topological space, `s` is an open subset of `α`, `G` is an additive group, `α` has an additive action by `G`, and the constant vector addition is continuous, then the set `{x + c | x ∈ s}` is open in `α`.
|
set_smul_mem_nhds_smul
theorem set_smul_mem_nhds_smul :
∀ {α : Type u_2} {G₀ : Type u_6} [inst : GroupWithZero G₀] [inst_1 : MulAction G₀ α] [inst_2 : TopologicalSpace α]
[inst_3 : ContinuousConstSMul G₀ α] {c : G₀} {s : Set α} {x : α}, s ∈ nhds x → c ≠ 0 → c • s ∈ nhds (c • x)
This theorem states that scalar multiplication preserves neighborhoods in a topological space. More specifically, if `s` is a set in the neighborhood of `x` in a topological space `α` with a group action defined by scalar multiplication (where the scalar is from a GroupWithZero `G₀`), and `c` is a non-zero element of `G₀`, then the scalar multiplication of `s` by `c` is in the neighborhood of the scalar multiplication of `x` by `c`. The theorem assumes that the scalar multiplication is continuous.
More concisely: If `s` is a neighborhood of `x` in a topological space `α` with continuous scalar multiplication by a non-zero element `c` in a group `G₀`, then the scalar multiplication of `s` by `c` is a neighborhood of `cx`.
|
isOpenMap_smul
theorem isOpenMap_smul :
∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
[inst_3 : ContinuousConstSMul G α] (c : G), IsOpenMap fun x => c • x
The theorem `isOpenMap_smul` states that for any type `α` which is a topological space, any type `G` which is a group, and any instance where `G` acts on `α` multiplicatively (`MulAction G α`), and the scalar multiplication operation is continuous (`ContinuousConstSMul G α`), then for any element `c` in `G`, the map that takes an element `x` in `α` and maps it to the result of the scalar multiplication of `c` and `x` (`c • x`) is an open map. In other words, the image of any open set in `α` under this map is an open set. The theorem ensures that the scalar multiplication operation will preserve the topological structure, specifically open sets, in the context of group actions.
More concisely: For any topological space α, group G with a multiplicative action on α, and a continuous scalar multiplication on G acting on α, the scalar multiplication map is an open map.
|
isClosedMap_smul_of_ne_zero
theorem isClosedMap_smul_of_ne_zero :
∀ {α : Type u_2} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ α]
[inst_3 : ContinuousConstSMul G₀ α] {c : G₀}, c ≠ 0 → IsClosedMap fun x => c • x
This theorem states that the scalar multiplication function, denoted by `smul`, is a closed map with respect to its second argument, given that the scalar `c` is not zero. Here, a function is said to be a closed map if the image of every closed set under this function is also a closed set. The types involved are `α` and `G₀`, where `α` is a topological space and `G₀` is a group with zero. This theorem requires the assumptions that `G₀` acts multiplicatively on `α` (expressed by `MulAction G₀ α`) and that the constant scalar multiplication operation from `G₀` to `α` is continuous (expressed by `ContinuousConstSMul G₀ α`). The lemma that scalar multiplication is a closed map in the first argument, when `α` is a normed space over a complete normed field, is given by `isClosedMap_smul_left` in the `Analysis.NormedSpace.FiniteDimension` module.
More concisely: Given a topological space `α` and a group `G₀` with zero, if `G₀` acts multiplicatively on `α` and the constant scalar multiplication operation from `G₀` to `α` is continuous, then the scalar multiplication function `smul : G₀ × α → α` is a closed map with respect to its second argument when the scalar is not zero.
|
Filter.Tendsto.const_vadd
theorem Filter.Tendsto.const_vadd :
∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : VAdd M α]
[inst_2 : ContinuousConstVAdd M α] {f : β → α} {l : Filter β} {a : α},
Filter.Tendsto f l (nhds a) → ∀ (c : M), Filter.Tendsto (fun x => c +ᵥ f x) l (nhds (c +ᵥ a))
This theorem states that given a topological space `α` which allows "vector addition" with some type `M`, and a function `f` from type `β` to `α` which converges to a limit `a` as per some filter `l`, adding a constant `c` from `M` to the function `f` will result in a new function that converges to `c + a`. In mathematical terms, if $\lim_{x \to l} f(x) = a$, then $\lim_{x \to l} (c + f(x)) = c + a$. This is true under the precondition that the vector addition operation with a constant `c` is continuous in this topological space.
More concisely: If `α` is a topological space with continuous vector addition of constant `c` from `M`, and `f : β → α` converges to `a` as `x` approaches a filter `l`, then `c + f` converges to `c + a`.
|
isOpenMap_smul₀
theorem isOpenMap_smul₀ :
∀ {α : Type u_2} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ α]
[inst_3 : ContinuousConstSMul G₀ α] {c : G₀}, c ≠ 0 → IsOpenMap fun x => c • x
The theorem `isOpenMap_smul₀` asserts that for any types `α` and `G₀`, where `α` has a topological space structure, `G₀` is a group with zero, and `G₀` acts on `α` in a multiplicative fashion, if the constant scalar multiplication by any non-zero element `c` of `G₀` is continuous, then scalar multiplication by this non-zero element `c` is an open map. In other words, it says that multiplying every element of an open set in `α` by a non-zero constant `c` from `G₀` gives us an open set in `α`.
More concisely: If `α` is a topological space, `G₀` is a group with a zero element and acts multiplicatively on `α`, and scalar multiplication by a non-zero `c` in `G₀` is continuous, then scalar multiplication by `c` is an open map on `α`.
|
Continuous.const_vadd
theorem Continuous.const_vadd :
∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : VAdd M α]
[inst_2 : ContinuousConstVAdd M α] [inst_3 : TopologicalSpace β] {g : β → α},
Continuous g → ∀ (c : M), Continuous fun x => c +ᵥ g x
This theorem states that for any types `M`, `α`, and `β`, if `α` has a topological space structure, `M` and `α` have a vector addition structure, and the vector addition of a constant from `M` and a variable from `α` is a continuous function, then for any continuous function `g` from `β` to `α`, and any constant `c` from `M`, the function that adds `c` to the value of `g` at each point in `β` (denoted as `fun x => c +ᵥ g x`) is also a continuous function.
In mathematical terms, if adding a constant vector to a variable vector in `α` is a continuous operation and `g` is a continuous function, then the function resulting from adding a constant vector `c` to the image of `g` is also continuous.
More concisely: If `α` is a topological space, `M` is a vector space over `α`, and the vector addition of a constant from `M` and a variable from `α` is a continuous function, then the function that adds a constant vector from `M` to the image of a continuous function `g` from `β` to `α` is also continuous.
|
IsOpen.smul
theorem IsOpen.smul :
∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
[inst_3 : ContinuousConstSMul G α] {s : Set α}, IsOpen s → ∀ (c : G), IsOpen (c • s)
The theorem `IsOpen.smul` states that for any open set `s` in a topological space `α`, if there exists a group `G` that acts on `α` continuously via multiplication (as specified by `[MulAction G α]` and `[ContinuousConstSMul G α]`), then the action of any element `c` from `G` on `s` (denoted as `c • s`) results in a set that is also open in the topological space `α`. This result holds for all such topological spaces `α`, groups `G`, and open sets `s`.
More concisely: For any topological space α, open set s, and a group G acting continuously on α via multiplication, the set operation c • s (where c is an element of G) results in an open subset of α.
|
ContinuousConstSMul.secondCountableTopology
theorem ContinuousConstSMul.secondCountableTopology :
∀ {Γ : Type u_4} [inst : Group Γ] {T : Type u_5} [inst_1 : TopologicalSpace T] [inst_2 : MulAction Γ T]
[inst_3 : SecondCountableTopology T] [inst_4 : ContinuousConstSMul Γ T],
SecondCountableTopology (Quotient (MulAction.orbitRel Γ T))
The theorem `ContinuousConstSMul.secondCountableTopology` states that for any group `Γ` and any type `T` with a group action of `Γ` on `T`, a topological space structure and a second countable topology, if the action of the group on the space is continuous, then the quotient space of `T` by the orbit relation of the group action (i.e., the space of orbits under the group action) also has a second countable topology. In simpler terms, if a space is second countable, then the space of orbits under a continuous group action is also second countable.
More concisely: If a second countable topological space `T` is endowed with a continuous group action of a group `Γ`, then the quotient space of `T` by the orbit relation has a second countable topology.
|
ProperlyDiscontinuousSMul.finite_disjoint_inter_image
theorem ProperlyDiscontinuousSMul.finite_disjoint_inter_image :
∀ {Γ : Type u_4} {T : Type u_5} [inst : TopologicalSpace T] [inst_1 : SMul Γ T]
[self : ProperlyDiscontinuousSMul Γ T] {K L : Set T},
IsCompact K → IsCompact L → {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}.Finite
The theorem states that given two compact sets `K` and `L` in a topological space `T` with a scalar multiplication operation (`SMul`) by elements from type `Γ`, if `ProperlyDiscontinuousSMul` holds for `Γ` and `T`, then the set of scalars `γ` such that the image of scalar multiplication of `γ` with each element in `K` intersected with `L` is nonempty, is finite. In other words, there are only finitely many scalars `γ` such that `γ * K` intersects with `L` non-trivially. This theorem is under the assumption that the scalar multiplication operation by elements from type `Γ` on the topological space `T` is properly discontinuous.
More concisely: Given compact sets K and L in a topological space T with properly discontinuous scalar multiplication by elements from type Γ, the set of scalars γ such that γ * K ∩ L is non-empty has finite cardinality.
|
Continuous.const_smul
theorem Continuous.const_smul :
∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SMul M α]
[inst_2 : ContinuousConstSMul M α] [inst_3 : TopologicalSpace β] {g : β → α},
Continuous g → ∀ (c : M), Continuous fun x => c • g x
This theorem states that, given a continuous function `g` mapping from a type `β` to a type `α` in a specific topological context, the scalar multiplication operation, denoted by `c • g x`, is also continuous for any scalar `c` of type `M`. Here, type `α` is endowed with a topological space structure and a scalar multiplication structure with a continuous scalar multiplication operation, and type `β` is also endowed with a topological space structure.
More concisely: Given a continuous function `g` from a topological space `β` to another topological space `α` endowed with continuous scalar multiplication, the scalar multiplication operation `c • g` is continuous for any scalar `c`.
|
ContinuousConstSMul.continuous_const_smul
theorem ContinuousConstSMul.continuous_const_smul :
∀ {Γ : Type u_1} {T : Type u_2} [inst : TopologicalSpace T] [inst_1 : SMul Γ T] [self : ContinuousConstSMul Γ T]
(γ : Γ), Continuous fun x => γ • x
This theorem states that for any types `Γ` and `T`, where `T` is a topological space and there exists a scalar multiplication operation between `Γ` and `T`, the scalar multiplication function `(•) : Γ → T → T` is continuous in its second argument. In other words, given any scalar `γ` of type `Γ`, the function which multiplies `γ` with a variable of type `T` is a continuous function.
More concisely: For any type `Γ` and topological space `T` with a continuous scalar multiplication `• : Γ → T → T`, the function `•` is continuous in its second argument.
|
ContinuousConstVAdd.continuous_const_vadd
theorem ContinuousConstVAdd.continuous_const_vadd :
∀ {Γ : Type u_1} {T : Type u_2} [inst : TopologicalSpace T] [inst_1 : VAdd Γ T] [self : ContinuousConstVAdd Γ T]
(γ : Γ), Continuous fun x => γ +ᵥ x
The theorem `ContinuousConstVAdd.continuous_const_vadd` states that for any types `Γ` and `T`, where `T` is a topological space and `Γ` can be added to `T` (i.e., `VAdd Γ T`), if `Γ` is continuously addable to `T` (i.e., `ContinuousConstVAdd Γ T`), then for any element `γ` of type `Γ`, the function that adds `γ` to any element of `T` is continuous. In mathematical terms, it means that the additive action `(+ᵥ) : Γ → T → T` is continuous in its second argument.
More concisely: If `Γ` is a continuously addable type to a topological space `T`, then the function that adds any element of `Γ` to an element of `T` is continuous in the second argument.
|
isOpenMap_quotient_mk'_add
theorem isOpenMap_quotient_mk'_add :
∀ {Γ : Type u_4} [inst : AddGroup Γ] {T : Type u_5} [inst_1 : TopologicalSpace T] [inst_2 : AddAction Γ T]
[inst_3 : ContinuousConstVAdd Γ T], IsOpenMap Quotient.mk'
This theorem states that the quotient map by a group action is open. In other words, given a type Γ with an addition group structure, a type T with a topological structure, an addition action of Γ on T, and the assumption that the addition action is continuous, then the canonical quotient map `Quotient.mk'`, which maps each element to its equivalence class in the quotient set, is an open map. An open map is one which maps any open set in the domain to an open set in the codomain. Thus, this theorem ensures that topological properties are preserved under the quotient operation by a group action.
More concisely: Given a topological space T with a continuous group action by a group Γ, the quotient map by this action is an open map.
|
ProperlyDiscontinuousVAdd.finite_disjoint_inter_image
theorem ProperlyDiscontinuousVAdd.finite_disjoint_inter_image :
∀ {Γ : Type u_4} {T : Type u_5} [inst : TopologicalSpace T] [inst_1 : VAdd Γ T]
[self : ProperlyDiscontinuousVAdd Γ T] {K L : Set T},
IsCompact K → IsCompact L → {γ | (fun x => γ +ᵥ x) '' K ∩ L ≠ ∅}.Finite
The theorem `ProperlyDiscontinuousVAdd.finite_disjoint_inter_image` states that for any two compact sets `K` and `L` in a topological space `T` with a proper discontinuous vector addition operation, there are only a finite number of elements `γ` such that the image (under the vector addition operation) of `K` intersected with `L` is not empty. In other words, there are only finitely many ways to add an element to the set `K` so that it has a non-empty intersection with `L`.
More concisely: For any two compact sets $K, L$ in a topological space $T$ with a proper discontinuous vector addition operation, the number of elements $\gamma$ such that $K + \gamma \cap L \neq \emptyset$ is finite.
|
isOpenMap_quotient_mk'_mul
theorem isOpenMap_quotient_mk'_mul :
∀ {Γ : Type u_4} [inst : Group Γ] {T : Type u_5} [inst_1 : TopologicalSpace T] [inst_2 : MulAction Γ T]
[inst_3 : ContinuousConstSMul Γ T], IsOpenMap Quotient.mk'
The theorem `isOpenMap_quotient_mk'_mul` states that the quotient map created by a group action is an open map. In more detail, for any type $\Gamma$ that has a group structure, and any topological space $T$ over which $\Gamma$ acts multiplicatively and continuously, the map that takes an element of $T$ to its equivalence class in the quotient space (created by the group action) is an open map. This means that the image of any open set in $T$ under this quotient map is an open set in the quotient space.
More concisely: The quotient map obtained by a multiplicatively acting and continuous group action on a topological space is an open map.
|