mul_left_of_isCompact

Mathlib.Topology.Algebra.Group.Pointwise

URI: https://scilib.ai/kg/mathlib#IsClosed.mul_left_of_isCompact

English

If t is closed and s is compact, then the product s · t is closed.

Русский

Если t замкнутое, а s компактное, то произведение s · t замкнуто.

LaTeX

$$$\\forall S,T \\subseteq G,\\ (\\text{IsClosed}(T) \\wedge \\text{IsCompact}(S)) \\Rightarrow \\text{IsClosed}(S \\cdot T)$$$

Lean4

@[to_additive]
theorem mul_left_of_isCompact (ht : IsClosed t) (hs : IsCompact s) : IsClosed (s * t) :=
  ht.smul_left_of_isCompact hs

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

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

Разделы

Аффилиация

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