centralizer_le — Mathlib

English

If s ⊆ t, then centralizer of t is contained in centralizer of s (the centralizer operation is order-reversing).

Русский

Если s ⊆ t, то центральтизатор t ⊆ центральтизатор s (операцияcentralizer возрастает в обратном порядке).

LaTeX

$$$\forall s,t\subseteq A,\; s \subseteq t \Rightarrow \mathrm{centralizer}(R,t) \subseteq \mathrm{centralizer}(R,s)$$$

Lean4

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

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