instContinuousNegElemBallOfNat

Mathlib.Analysis.Normed.Group.BallSphere

URI: https://scilib.ai/kg/mathlib#instContinuousNegElemBallOfNat

English

The negation map on the ball is continuous: the negation map from ball 0,r to itself is continuous.

Русский

Отображение отрицания на шаре непрерывно.

LaTeX

$$$\text{ContinuousNeg} \big(\mathsf{ball}(0,r)\big)$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru