adjoin_insert_adjoin — Mathlib

English

Let f: A →ₐ[R] B be an algebra homomorphism and s ⊆ A. Then adjoin_R(Set.image f s) = Subalgebra.map f (adjoin_R s).

Русский

Пусть f: A →ₐ[R] B — алгебра-гомоморфизм. Тогда adjoin_R(образ f от s) = образ порождающей над s: adjoin_R(Set.image f s) = Subalgebra.map f (adjoin_R s).

LaTeX

$$$\\operatorname{adjoin}_R(\\operatorname{image} f\, s) = \\operatorname{map} f(\\operatorname{adjoin}_R s)$$$

Lean4

@[simp]
theorem adjoin_insert_adjoin (x : A) : adjoin R (insert x ↑(adjoin R s)) = adjoin R (insert x s) :=
  le_antisymm
    (adjoin_le (Set.insert_subset_iff.mpr ⟨subset_adjoin (Set.mem_insert _ _), adjoin_mono (Set.subset_insert _ _)⟩))
    (Algebra.adjoin_mono (Set.insert_subset_insert Algebra.subset_adjoin))

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