commute_of_mem_adjoin_of_forall_mem_commute

English

The adjoin of s is contained in the centralizer of the centralizer of s; i.e., adjoin_R(s) ≤ centralizer_R(centralizer_R(s)).

Русский

Объединение (адьён) множества s содержится в централизаоре централизатора s; т.е. adjoin_R(s) ⊆ centralizer_R(centralizer_R(s)).

LaTeX

$$\operatorname{adjoin}_R(s) \le \operatorname{centralizer}(R, \operatorname{centralizer}(R,s))$$

Lean4

theorem commute_of_mem_adjoin_of_forall_mem_commute {a b : A} {s : Set A} (hb : b ∈ adjoin R s)
    (h : ∀ b ∈ s, Commute a b) (h_star : ∀ b ∈ s, Commute a (star b)) : Commute a b :=
  NonUnitalAlgebra.commute_of_mem_adjoin_of_forall_mem_commute hb fun b hb ↦
    hb.elim (h b) (by simpa using h_star (star b))

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