centralizer_eq_top_iff_subset — Mathlib

English

For any subset s of M, centralizer(s) = ⊤ if and only if s ⊆ center M.

Русский

Для любого множества s ⊆ M, centralizer(s) = ⊤ тогда и только тогда, когда s ⊆ центр M.

LaTeX

$$$ centralizer(s) = ⊤ \\iff s \\subseteq center(M) $$$

Lean4

@[to_additive (attr := simp)]
theorem centralizer_eq_top_iff_subset {s : Set M} : centralizer s = ⊤ ↔ s ⊆ center M :=
  SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset

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