instOfDiscreteTopology — Mathlib

English

Let M be an R-module with the discrete topology. Then the topology is R-linear.

Русский

Пусть M — модуль над R, снабжён дискретной топологией. Тогда топология линейная по отношению к R.

LaTeX

$$$ DiscreteTopology(M) \\Rightarrow IsLinearTopology(R, M) $$$

Lean4

/-- The discrete topology on any `R`-module is `R`-linear. -/
instance [DiscreteTopology M] : IsLinearTopology R M :=
  have : HasBasis (𝓝 0 : Filter M) (fun _ ↦ True) (fun (_ : Unit) ↦ (⊥ : Submodule R M)) :=
    by
    rw [nhds_discrete]
    exact hasBasis_pure _
  mk_of_hasBasis R this

Похожие утверждения