iSup_span — Mathlib

English

For any family p: ι → Set M, the supremum of the spans of p(i) equals the span of the union of all p(i): ⨆ i, span_R(p_i) = span_R(⋃ i, p_i).

Русский

Для семейства p: ι → Set M верхний предел спанов p(i) равен спану объединения всех p(i): ⨆ i, span_R(p_i) = span_R(⋃ i, p_i).

LaTeX

$$$\big\vee_i \operatorname{span}_R(p_i) = \operatorname{span}_R\left(\bigcup_i p_i\right)$$$

Lean4

theorem iSup_span {ι : Sort*} (p : ι → Set M) : ⨆ i, span R (p i) = span R (⋃ i, p i) :=
  le_antisymm (iSup_le fun i => span_mono <| subset_iUnion _ i) <|
    span_le.mpr <| iUnion_subset fun i _ hm => mem_iSup_of_mem i <| subset_span hm

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