adjoin_span — Mathlib

English

For a subset s of A, the adjoin of s is unchanged if we replace s by its R-span: adjoin_R(span_R s) = adjoin_R s.

Русский

Для подмножества s ⊆ A порождение_R s не меняется при замене s на его линейную оболочку: adjoin_R(span_R s) = adjoin_R s.

LaTeX

$$$\\operatorname{adjoin}_R(\\operatorname{span}_R s) = \\operatorname{adjoin}_R s$$$

Lean4

@[simp]
theorem adjoin_span {s : Set A} : adjoin R (Submodule.span R s : Set A) = adjoin R s :=
  le_antisymm (adjoin_le (span_le_adjoin _ _)) (adjoin_mono Submodule.subset_span)

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