Theorems · Theorem · functional analysis

ContinuousSMul.of_nhds_zero

∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace R] [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [IsTopologicalRing R] [IsTopologicalAddGroup M],
  Filter.Tendsto (fun p => p.1 • p.2) (nhds 0 ×ˢ nhds 0) (nhds 0) →
    (∀ (m : M), Filter.Tendsto (fun a => a • m) (nhds 0) (nhds 0)) →
      (∀ (a : R), Filter.Tendsto (fun m => a • m) (nhds 0) (nhds 0)) → ContinuousSMul R M

Defined in

Mathlib.Topology.Algebra.Module.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingTopologicalSpaceTopologicalSpaceAddCommGroupModuleIsTopologicalRingIsTopologicalAddGroup