instContinuousNegElemClosedBallOfNat

English

The negation map is continuous on the closed ball of radius r around 0 in a seminormed additive commutative group E.

Русский

Непрерывность отображения x ↦ −x на замкнутом шаре радиуса r вокруг нуля в полугруппе с полугрупповой нормой.

LaTeX

$$$\forall r \in \mathbb{R},\; \left(-\right)|_{\overline{B}_E(0,r)} \text{ is continuous}$$$

Lean4

instance : ContinuousNeg (closedBall (0 : E) r) :=
  IsInducing.subtypeVal.continuousNeg fun _ => rfl

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