not_mem_of_mem_ofFixingSubgroup

Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

URI: https://scilib.ai/kg/mathlib#SubMulAction.not_mem_of_mem_ofFixingSubgroup

English

If x is in the fixed-subgroup, its image under the projection to the orbit is outside S.

Русский

Если x принадлежит fixingSubgroup, его образ под проекцией в орбиту не лежит в S.

LaTeX

$$not_mem_of_mem_ofFixingSubgroup$$

Lean4

@[to_additive]
theorem not_mem_of_mem_ofFixingSubgroup (x : ofFixingSubgroup M s) : ↑x ∉ s :=
  x.prop

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

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

Разделы

Аффилиация

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