instContinuousNegAdditiveOfContinuousInv

English

If H has a topological space structure, inversion, and is continuously inverted, then the negation on the additive version is continuous.

Русский

Если у H есть топологическая структура, инверсия существует и непрерывна, то отрицание в аддитивной версии непрерывно.

LaTeX

$$$\\\\operatorname{ContinuousNeg} (\\\\operatorname{Additive} H).$$$

Lean4

instance [TopologicalSpace H] [Inv H] [ContinuousInv H] : ContinuousNeg (Additive H) where
  continuous_neg := @continuous_inv H _ _ _

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