continuous_mul_left

Mathlib.Topology.Algebra.Monoid

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

English

For any a ∈ M, the map b ↦ a·b is continuous.

Русский

Для любого фиксированного a ∈ M отображение b ↦ a·b непрерывно.

LaTeX

$$$a \in M \Rightarrow \text{Continuous}(b \mapsto a b)$$$

Lean4

@[to_additive (attr := continuity)]
theorem continuous_mul_left (a : M) : Continuous fun b : M => a * b :=
  continuous_const.mul continuous_id

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

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

Разделы

Аффилиация

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