English
A variant of construction that produces IsLinearTopology from a basis of neighborhoods of zero consisting of a class of submodules with SMul controls.
Русский
Вариант конструктора, создающий IsLinearTopology из базиса окрестностей нуля, состоящего из класса подмодулей с управляющими свойствами умножения.
LaTeX
$$$IsLinearTopology.R\\,M$ from basis h : (nhds 0).HasBasis p (s i)$$
Lean4
/-- A variant of `IsLinearTopology.mk_of_hasBasis` asking for an explicit proof that `S`
is a class of submodules instead of relying on (fragile) typeclass inference of `SMulCommClass`. -/
theorem mk_of_hasBasis' {ι : Sort*} {S : Type*} [SetLike S M] [AddSubmonoidClass S M] {p : ι → Prop} {s : ι → S}
(h : (𝓝 0).HasBasis p (fun i ↦ (s i : Set M))) (hsmul : ∀ s : S, ∀ r : R, ∀ m ∈ s, r • m ∈ s) : IsLinearTopology R M
where
hasBasis_submodule' :=
h.to_hasBasis
(fun i hi ↦
⟨{ carrier := s i, add_mem' := add_mem, zero_mem' := zero_mem _, smul_mem' := hsmul _ }, h.mem_of_mem hi,
subset_rfl⟩)
(fun _ ↦ h.mem_iff.mp)
