leftCoset

Mathlib.Topology.Algebra.Group.Basic

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

English

If U is open, then the left-add coset op x • U is open.

Русский

Если U открыто, то левый добавочный косет op x • U открыт.

LaTeX

$$$IsOpen(U) \\Rightarrow IsOpen(op\\,x \\cdot U).$$$

Lean4

@[to_additive IsClosed.left_addCoset]
theorem leftCoset {U : Set G} (h : IsClosed U) (x : G) : IsClosed (x • U) :=
  isClosedMap_mul_left x _ h

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

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

Разделы

Аффилиация

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