span — Mathlib

English

For any set s ⊆ R, x belongs to span(s) if and only if x lies in every two-sided ideal containing s.

Русский

Для любого множества s ⊆ R элемент x принадлежит span(s) тогда и только тогда, когда x лежит в каждом двустороннем идеале, содержащем s.

LaTeX

$$$x \\in span(s) \\iff \\forall I, s \\subseteq I \\rightarrow x \\in I$$$

Lean4

/-- The smallest two-sided ideal containing a set.
-/
abbrev span (s : Set R) : TwoSidedIdeal R :=
  { ringCon := ringConGen (fun a b ↦ a - b ∈ s) }

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