span_range_eq_iSup — Mathlib

English

The span of a family’s range equals the supremum of the spans of the individual ranges.

Русский

Образ множества порождает подпроизвольную комбинацию, равную наибольшему сумме подмодулей отдельных элементов.

LaTeX

$$span_R(range v) = ⨆ i, span_R({v(i)})$$

Lean4

theorem span_range_eq_iSup {ι : Sort*} {v : ι → M} : span R (range v) = ⨆ i, R ∙ v i := by
  rw [span_eq_iSup_of_singleton_spans, iSup_range]

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