Theorems · Theorem · Lie groups

ContinuousSMul.of_basis_zero

∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {ι : Type u_3} [IsTopologicalRing R] [inst_5 : TopologicalSpace M] [IsTopologicalAddGroup 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

A topological additive group with a basis of 𝓝 0 satisfying the axioms of ModuleFilterBasis is a topological module. This lemma is mathematically useless because one could obtain such a result by applying ModuleFilterBasis.continuousSMul and use the fact that group topologies are characterized by their neighborhoods of 0 to obtain the ContinuousSMul on the pre-existing topology. But it turns out it's just easier to get it as a byproduct of the proof, so this is just a free quality-of-life improvement.

Defined in

Mathlib.Topology.Algebra.FilterBasis

Cited by

1 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingTopologicalSpaceAddCommGroupModuleIsTopologicalRingTopologicalSpaceIsTopologicalAddGroup