English
A variant of the previous result: the neighborhood basis at 0 can be taken from open sub-(R,R')-bimodules.
Русский
Вариант предыдущей леммы: база окрестностей нуля может быть взята из открытых под- (R,R')-би-модулей.
LaTeX
$$$ (\\mathcal{N}(0_M)).HasBasis \\Big( I : AddSubgroup M \\mapsto IsOpen(I:Set M) \\land (\\forall r\\in R, \\forall x\\in I, r\\cdot x \\in I) \\land (\\forall r'\\in R', \\forall x\\in I, r'\\cdot x \\in I) \\Big)\\,(I:Set M) $$$
Lean4
/-- A variant of `IsLinearTopology.hasBasis_subbimodule` using `IsOpen I` instead of `I ∈ 𝓝 0`. -/
theorem hasBasis_open_subbimodule [ContinuousAdd M] [IsLinearTopology R M] [IsLinearTopology R' M] :
(𝓝 (0 : M)).HasBasis
(fun I : AddSubgroup M ↦ IsOpen (I : Set M) ∧ (∀ r : R, ∀ x ∈ I, r • x ∈ I) ∧ (∀ r' : R', ∀ x ∈ I, r' • x ∈ I))
(fun I : AddSubgroup M ↦ (I : Set M)) :=
hasBasis_subbimodule R R' |>.congr (fun N ↦ and_congr_left' ⟨N.isOpen_of_mem_nhds, fun hN ↦ hN.mem_nhds (zero_mem N)⟩)
(fun _ _ ↦ rfl)
-- Even though `R` can be recovered from `a`, the nature of this lemma means that `a` will
-- often be left for Lean to infer, so making `R` explicit is useful in practice.
