span_iUnion₂ — Mathlib

English

Span of a double-indexed union equals the supremum over pairs.

Русский

Порождающее двойного индекса объединения эквивалентно наибольшему по парам индексов.

LaTeX

$$$$\operatorname{span} R\Big( \bigcup_i \bigcup_j s_{i,j} \Big) = \bigvee_{i,j} \operatorname{span} R (s_{i,j}) $$$$

Lean4

theorem span_iUnion₂ {ι} {κ : ι → Sort*} (s : ∀ i, κ i → Set M) :
    span R (⋃ (i) (j), s i j) = ⨆ (i) (j), span R (s i j) :=
  (Submodule.gi R M).gc.l_iSup₂

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