mul_right

Mathlib.Topology.Algebra.Group.Pointwise

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

English

If s is open, then s·t is open for any t.

Русский

Если s открыто, то s·t открыто для любого t.

LaTeX

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

Lean4

@[to_additive]
theorem mul_right (hs : IsOpen s) : IsOpen (s * t) :=
  by
  rw [← image_op_smul]
  exact hs.smul_left

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

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

Разделы

Аффилиация

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