of_continuousConstSMul — Mathlib

English

If a submodule of a topological module has nonempty interior and 0 is a limit of invertible scalars, then the submodule must be the whole space.

Русский

Если подмодуль топологического модуля имеет непустое interior и 0 является пределом обратимых скаляров, то подмодуль равен всему пространству.

LaTeX

$$$\\text{Interior}(s)\\neq \\emptyset \\Rightarrow s=\\top$ under the given hypotheses$$

Lean4

/-- A topological module over a ring has continuous negation.

This cannot be an instance, because it would cause search for `[Module ?R M]` with unknown `R`. -/
theorem of_continuousConstSMul [ContinuousConstSMul R M] : ContinuousNeg M where
  continuous_neg := by simpa using continuous_const_smul (T := M) (-1 : R)

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