centralizer_le — Mathlib

English

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

Русский

Если s ⊆ t, то централизация по t содержится внутри централизации по s.

LaTeX

$$$s \subseteq t \implies \operatorname{centralizer}(R,t) \le \operatorname{centralizer}(R,s)$$$

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)

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