English
If M has linear topologies with respect to R and R' and is an R–R' bimodule with IsLinearTopology assumptions, then the zero-neighborhood basis can be described via open two-sided ideals.
Русский
Если M имеет линейные топологические структуры по R и R' и является би-модулем, то база окрестностей нуля описывается через открытые двусторонние идеалы.
LaTeX
$$$ (\\mathcal{N}(0 : R)).HasBasis (I : TwoSidedIdeal R \\mapsto IsOpen(I:Set R)) (I:Set R) $$$
Lean4
/-- If `M` is a linearly topologized `R`-module and `i ↦ m i` tends to zero,
then `i ↦ a i • m i` still tends to zero for any family `a : ι → R`. -/
theorem tendsto_smul_zero [IsLinearTopology R M] {ι : Type*} {f : Filter ι} (a : ι → R) (m : ι → M)
(ha : Tendsto m f (𝓝 0)) : Tendsto (a • m) f (𝓝 0) :=
by
rw [hasBasis_submodule R |>.tendsto_right_iff] at ha ⊢
intro I hI
filter_upwards [ha I hI] with i ai_mem
exact I.smul_mem _ ai_mem
