orbitRel_subgroup_le

Mathlib.GroupTheory.GroupAction.Basic

URI: https://scilib.ai/kg/mathlib#MulAction.orbitRel_subgroup_le

English

For a subgroup H ≤ G, the orbit relation for H is contained in the orbit relation for G.

Русский

Для подгруппы H ≤ G орбитальная связь H содержится в орбитальной связи G.

LaTeX

$$orbitRel H α ≤ orbitRel G α$$

Lean4

@[to_additive]
theorem orbitRel_subgroup_le (H : Subgroup G) : orbitRel H α ≤ orbitRel G α :=
  Setoid.le_def.2 mem_orbit_of_mem_orbit_subgroup

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

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

Разделы

Аффилиация

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