centralizer_le

Mathlib.GroupTheory.Subgroup.Centralizer

URI: https://scilib.ai/kg/mathlib#Subgroup.centralizer_le

English

If s ⊆ t are subsets of G, then centralizer(t) ≤ centralizer(s).

Русский

Если s ⊆ t являются подмножества G, то centralizer(t) ≤ centralizer(s).

LaTeX

$$s \subseteq t \Rightarrow centralizer(t) \le centralizer(s)$$

Lean4

@[to_additive]
theorem centralizer_le {s t : Set G} (h : s ⊆ t) : centralizer t ≤ centralizer s :=
  Submonoid.centralizer_le h

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

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

Разделы

Аффилиация

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