centralizer_le

Mathlib.Algebra.Star.Subalgebra

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

← MathLib Explorer

English

If s ⊆ t are subsets of A, then the centralizer of t is contained in the centralizer of s.

Русский

Если s ⊆ t, то центрaлизатор t ⊆ централизатор s.

LaTeX

$$centralizer R t ≤ centralizer R s whenever s ⊆ t$$

Lean4

theorem centralizer_le (s t : Set A) (h : s ⊆ t) : centralizer R t ≤ centralizer R s :=
  Set.centralizer_subset (Set.union_subset_union h <| Set.preimage_mono h)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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