continuous_neg — Mathlib

English

The negation map on any topological R-module with module topology is continuous; i.e., a ↦ -a is continuous for all such modules.

Русский

Отображение a ↦ -a непрерывно на любом топологическом R-модуле с модульной топологией.

LaTeX

$$$\\forall C: \\text{AddCommGroup}(C)\\, \\[Module R C] \\[TopologicalSpace C] \\[IsModuleTopology R C], \\mathrm{Continuous}(-: C \ o C).$$$

Lean4

theorem continuous_neg (C : Type*) [AddCommGroup C] [Module R C] [TopologicalSpace C] [IsModuleTopology R C] :
    Continuous (fun a ↦ -a : C → C) :=
  haveI : ContinuousAdd C := IsModuleTopology.toContinuousAdd R C
  continuous_of_linearMap (LinearEquiv.neg R).toLinearMap

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