iUnion_option — Mathlib

English

The union over an Option-indexed family is the union of the none-case and the some-case shifts: ⋃ o, s o = s none ∪ ⋃ i, s (some i).

Русский

Объединение по индексу Option равно объединению none и объединению по some: ⋃ o, s o = s none ∪ ⋃ i, s (some i).

LaTeX

$$$ \bigcup_o s(o) = s(\text{none}) \cup \bigcup_i s(\text{some}(i)) $$$

Lean4

theorem iUnion_option {ι} (s : Option ι → Set α) : ⋃ o, s o = s none ∪ ⋃ i, s (some i) :=
  iSup_option s

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