continuousMul

Mathlib.Topology.MetricSpace.Algebra

URI: https://scilib.ai/kg/mathlib#LipschitzMul.continuousMul

English

Multiplication is a continuous operation in β: the product map β × β → β is continuous.

Русский

Умножение в β непрерывно: отображение (x,y) ↦ xy непрерывно.

LaTeX

$$$\\text{ContinuousMul}\\;β$$$

Lean4

@[to_additive]
instance (priority := 100) continuousMul : ContinuousMul β :=
  ⟨lipschitzWith_lipschitz_const_mul_edist.continuous⟩

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

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

Разделы

Аффилиация

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