mem_span — Mathlib

English

An element x lies in the span of a set s if and only if x belongs to every ideal containing s.

Русский

Элемент x принадлежит span(s) тогда и только тогда, когда x принадлежит каждому идеалу, содержащему s.

LaTeX

$$$x \\in \\operatorname{span}(s) \\iff \\forall J,\\ s \\subseteq J \\Rightarrow x \\in J$$$

Lean4

theorem mem_span {s : Set α} (x) : x ∈ span s ↔ ∀ p : Ideal α, s ⊆ p → x ∈ p :=
  mem_iInter₂

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