ContinuousSMul.of_basis_zero
theorem ContinuousSMul.of_basis_zero :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : TopologicalSpace R] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] {ι : Type u_3} [inst_4 : TopologicalRing R] [inst_5 : TopologicalSpace M]
[inst_6 : TopologicalAddGroup M] {p : ι → Prop} {b : ι → Set M},
(nhds 0).HasBasis p b →
(∀ {i : ι}, p i → ∃ V ∈ nhds 0, ∃ j, p j ∧ V • b j ⊆ b i) →
(∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ Set.MapsTo (fun x => x₀ • x) (b j) (b i)) →
(∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in nhds 0, x • m₀ ∈ b i) → ContinuousSMul R M
This theorem states that a topological add group, with a basis of neighborhoods around the point `0` that satisfies the `ModuleFilterBasis` axioms, is a topological module. Given a commutative ring `R`, a module `M` over `R`, a topological ring structure over `R`, a topological space structure over `M`, an add commutative group structure over `M`, and a property `p` and a function `b` on some type `ι`, if the filter of neighborhoods around `0` on `M` has a basis indexed by `ι` satisfying `p`, and for all `i : ι` satisfying `p`, there exists some `V` in the neighborhood of `0` and some `j` satisfying `p` such that `V` times the image of `j` under `b` is a subset of the image of `i` under `b`, and for all scalars `x₀ : R` and `i : ι` satisfying `p`, there exists some `j` satisfying `p` such that the map taking any `x` to `x₀` times `x` maps the image of `j` under `b` into the image of `i` under `b`, and for all `m₀ : M` and `i : ι` satisfying `p`, eventually for `x : R` in the neighborhood of `0`, `x` times `m₀` is in the image of `i` under `b`, then scalar multiplication is continuous on the topological module `M`.
More concisely: If a topological add group `M` over a commutative ring `R`, endowed with a topology having a basis of neighborhoods around `0` satisfying the `ModuleFilterBasis` axioms, is such that for all `i : ι` in a certain property `p`, there exist `V` and `j` in `p` with `V` times the image of `j` under `b` contained in the image of `i` under `b`, and scalar multiplication is continuous at `0`, then scalar multiplication is continuous on `M`.
|
AddGroupFilterBasis.nhds_zero_hasBasis
theorem AddGroupFilterBasis.nhds_zero_hasBasis :
∀ {G : Type u} [inst : AddGroup G] (B : AddGroupFilterBasis G), (nhds 0).HasBasis (fun V => V ∈ B) id
This theorem states that for any given additive group `G` and any `AddGroupFilterBasis` `B` of `G`, the neighborhood filter at `0` (denoted by `nhds 0`) in `G` has a certain basis. The basis consists of those sets that belong to `B`, each of which is mapped to itself by the identity function (`id`). In the context of topology, having such a basis means that every neighborhood of `0` in the topological space `G` can be represented as a "filter union" of these basis sets.
More concisely: For any additive group `G` and `AddGroupFilterBasis` `B` of `G`, the neighborhood filter at `0` in `G` has `B` as a basis, where a basis element is a set in `B` that maps to itself under the identity function.
|
AddGroupFilterBasis.mem_nhds_zero
theorem AddGroupFilterBasis.mem_nhds_zero :
∀ {G : Type u} [inst : AddGroup G] (B : AddGroupFilterBasis G) {U : Set G}, U ∈ B → U ∈ nhds 0
This theorem states that for any type `G` that has an `AddGroup` structure and any `AddGroupFilterBasis` `B` of `G`, if a set `U` is an element of `B`, then `U` is a neighborhood of the additive identity element `0`. In simpler terms, if a set `U` belongs to a certain filter basis for the additive group `G`, then `U` must also belong to the neighborhood filter of zero in `G`.
More concisely: For any AddGroup `G` and AddGroupFilterBasis `B` of `G`, any element `U` in `B` is a neighborhood of the additive identity `0` in `G`.
|
AddGroupFilterBasis.nhds_zero_eq
theorem AddGroupFilterBasis.nhds_zero_eq :
∀ {G : Type u} [inst : AddGroup G] (B : AddGroupFilterBasis G), nhds 0 = AddGroupFilterBasis.toFilterBasis.filter
This theorem states that for any additive group `G` and any additive group filter basis `B` of `G`, the neighborhood filter of the element `0` in `G` is equal to the filter associated to the filter basis which converts the additive group filter basis `B` to a filter basis. In other words, in the context of additive groups, the neighborhood filter at the 'zero' element can be constructed by taking the filter associated with the filter basis obtained from an additive group filter basis.
More concisely: For any additive group G and its filter basis B, the neighborhood filter of 0 in G equals the filter associated to the filter basis obtained from B.
|