moduleTopology_le — Mathlib

English

The module topology is finer than any topology that makes A into a topological R-module.

Русский

Модульная топология является более тонкой любой топологии, делающей A топологическим R-модулем.

LaTeX

$$$\text{moduleTopology } R A \le \tau_A$$$

Lean4

/-- The module topology is `≤` any topology making `A` into a topological module. -/
theorem moduleTopology_le [τA : TopologicalSpace A] [ContinuousSMul R A] [ContinuousAdd A] : moduleTopology R A ≤ τA :=
  sInf_le ⟨inferInstance, inferInstance⟩

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