mul_left

Mathlib.Topology.Algebra.Group.Pointwise

URI: https://scilib.ai/kg/mathlib#IsOpen.mul_left

English

If t is open in a group α, then s·t is open for any set s.

Русский

Если t открыто в группе α, то произведение s·t открыто для любого множества s.

LaTeX

$$$\\text{IsOpen}(t) \\Rightarrow \\text{IsOpen}(s\\cdot t).$$$

Lean4

@[to_additive]
theorem mul_left : IsOpen t → IsOpen (s * t) :=
  IsOpen.smul_left

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

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

Разделы

Аффилиация

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