English
If the coefficient ring R is endowed with a linear topology, then the sets B(J,d) = { f ∈ MvPowerSeries(σ,R) : coeff d f ∈ J }, where J runs over neighborhoods of 0 in R and d runs over σ →₀ ℕ, form a basis of neighborhoods of 0 in the product-topology on MvPowerSeries(σ,R).
Русский
Если кольцо коэффициентов R имеет линейную топологию, то множества B(J,d) = { f ∈ MvPowerSeries(σ,R) : коэффициент d f ∈ J }, где J — окрестности 0 в R, и d — элемент σ →₀ ℕ, образуют базис окрестностей нуля в произведной топологии на MvPowerSeries(σ,R).
LaTeX
$$$\displaystyle (\mathcal{N} 0)\text{ has a basis }\{ B(J,d) \}_{J \in \mathcal{N} 0,\; d \in (\sigma \to\_0 \mathbb{N})}, \\ B(J,d)=\{ f\in \mathrm{MvPowerSeries}(\sigma,R) : \operatorname{coeff}(d)\,f \in J \}.$$$
Lean4
/-- If the ring `R` is endowed with a linear topology, then the sets `↑basis σ R (J, d)`,
for `J : TwoSidedIdeal R` which are neighborhoods of `0 : R` and `d : σ →₀ ℕ`,
constitute a basis of neighborhoods of `0 : MvPowerSeries σ R` for the product topology. -/
theorem hasBasis_nhds_zero [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R] :
(𝓝 0 : Filter (MvPowerSeries σ R)).HasBasis (fun Id : TwoSidedIdeal R × (σ →₀ ℕ) ↦ (Id.1 : Set R) ∈ 𝓝 0)
(fun Id ↦ basis _ _ Id) :=
by
classical
rw [nhds_pi]
refine IsLinearTopology.hasBasis_twoSidedIdeal.pi_self.to_hasBasis ?_ ?_
· intro ⟨D, I⟩ ⟨hD, hI⟩
refine ⟨⟨I, Finset.sup hD.toFinset id⟩, hI, fun f hf d hd ↦ ?_⟩
rw [SetLike.mem_coe, mem_basis_iff] at hf
convert hf _ <| Finset.le_sup (hD.mem_toFinset.mpr hd)
· intro ⟨I, d⟩ hI
refine ⟨⟨Iic d, I⟩, ⟨finite_Iic d, hI⟩, ?_⟩
simpa [basis, coeff_apply, Iic, Set.pi] using subset_rfl
