eq_moduleTopology — Mathlib

English

If A is a topological R-module and [IsModuleTopology R A] holds, then the given topology on A coincides with the module topology.

Русский

Если A — топологический R-модуль и выполняется [IsModuleTopology R A], то данная топология на A совпадает с модульной топологией.

LaTeX

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

Lean4

theorem eq_moduleTopology [τA : TopologicalSpace A] [IsModuleTopology R A] : τA = moduleTopology R A :=
  IsModuleTopology.eq_moduleTopology' (R := R) (A := A)

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