instContMDiffMulOfTopWithTopENat

Mathlib.Geometry.Manifold.Algebra.Monoid

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

English

If multiplication on G is continuously multiplicative, then it is C^0 (continuous) in particular.

Русский

Если умножение на G непрерывно по произведению, то оно, в частности, непрерывно (C^0).

LaTeX

$$$$ \text{ContinuousMul } G \Rightarrow \ContMDiffMul I 0 G $$$$

Lean4

@[to_additive]
instance {a : WithTop ℕ∞} [ContMDiffMul I ω G] : ContMDiffMul I a G :=
  ContMDiffMul.of_le le_top

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

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

Разделы

Аффилиация

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