supports_of_mem

Mathlib.GroupTheory.GroupAction.Support

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

English

If a ∈ s, then s supports a; i.e., any g fixing s pointwise also fixes a.

Русский

Если a ∈ s, то s поддерживает a; то есть любой g, фиксирующий s поэлементно, фиксирует a.

LaTeX

$$$ a \\in s \\Rightarrow Supports(G,s,a) $$$

Lean4

@[to_additive]
theorem supports_of_mem (ha : a ∈ s) : Supports G s a := fun _ h => h ha

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

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

Разделы

Аффилиация

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