rightCoset

Mathlib.Topology.Algebra.Group.Basic

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

English

If U is closed, then the right coset op x • U is closed for every x ∈ G.

Русский

Если U замкнуто, то для каждого x ∈ G правый косет op x • U замкнут.

LaTeX

$$$IsClosed(U) \\Rightarrow IsClosed(instHSMul.hSMul (MulOpposite.op x) U).$$$

Lean4

@[to_additive IsClosed.right_addCoset]
theorem rightCoset {U : Set G} (h : IsClosed U) (x : G) : IsClosed (op x • U) :=
  isClosedMap_mul_right x _ h

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

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

Разделы

Аффилиация

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