span_attach_biUnion — Mathlib

English

Span of a union over a finite set with attached indices equals the supremum over the finite collection.

Русский

Порождающее объединение по финитной би-объединённой индексации равно верхней границе порождений.

LaTeX

$$$$\operatorname{span} R (s.attach.biUnion f) = \bigsqcup_x \operatorname{span} R (f x)$$$$

Lean4

theorem span_attach_biUnion [DecidableEq M] {α : Type*} (s : Finset α) (f : s → Finset M) :
    span R (s.attach.biUnion f : Set M) = ⨆ x, span R (f x) := by simp [span_iUnion]

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