fixingSubgroup_antitone

Mathlib.GroupTheory.GroupAction.FixingSubgroup

URI: https://scilib.ai/kg/mathlib#fixingSubgroup_antitone

English

The map s ↦ fixingSubgroup(M,s) is antitone in s.

Русский

Картировка s ↦ fixingSubgroup(M,s) антимонотна по s.

LaTeX

$$$s \\subseteq t \\Rightarrow fixingSubgroup(M,t) \\le fixingSubgroup(M,s)$$$

Lean4

@[to_additive]
theorem fixingSubgroup_antitone : Antitone (fixingSubgroup M : Set α → Subgroup M) :=
  (fixingSubgroup_fixedPoints_gc M α).monotone_l

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

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

Разделы

Аффилиация

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