span_eq_iSup_of_singleton_spans — Mathlib

English

Span of a set is the supremum of spans of singleton elements.

Русский

Порождающее множество эквивалентно верхнему пределу порождений отдельными элементами.

LaTeX

$$$$ \operatorname{span} R s = \bigvee_{x \in s} \operatorname{span} R (\{x\}) $$$$

Lean4

theorem span_eq_iSup_of_singleton_spans (s : Set M) : span R s = ⨆ x ∈ s, R ∙ x := by
  simp only [← span_iUnion, Set.biUnion_of_singleton s]

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