English
Equivalence between IsLinearTopology and HasBasis of neighborhoods of 0 by submodules.
Русский
Эквивалентность между IsLinearTopology и базисом окрестностей нуля из подмодулей.
LaTeX
$$$IsLinearTopology\\,R\\,M \\iff (\\mathcal N 0).HasBasis (N:\\ Submodule R M) (N)$$$
Lean4
/-- To show that `M` is linearly-topologized as an `R`-module, it suffices to show
that it has a basis of neighborhoods of zero made of `R`-submodules.
Note: for technical reasons detailed in the module docstring, Lean sometimes struggles to find the
right `SMulMemClass` instance. See `IsLinearTopology.mk_of_hasBasis'` for a more
explicit variant. -/
theorem mk_of_hasBasis {ι : Sort*} {S : Type*} [SetLike S M] [SMulMemClass S R M] [AddSubmonoidClass S M] {p : ι → Prop}
{s : ι → S} (h : (𝓝 0).HasBasis p (fun i ↦ (s i : Set M))) : IsLinearTopology R M :=
mk_of_hasBasis' R h fun _ ↦ SMulMemClass.smul_mem
