set_biUnion_option_toFinset — Mathlib

English

The union over the Finset formed from an option equals the union over the option directly.

Русский

Объединение по Finset, полученному из опции, равно объединению по самой опции.

LaTeX

$$$$ \\bigcup_{x \\in o^{\\mathrm{toFinset}}} t(x) = \\bigcup_{x \\in o} t(x) $$$$

Lean4

theorem set_biUnion_option_toFinset (o : Option α) (f : α → Set β) : ⋃ x ∈ o.toFinset, f x = ⋃ x ∈ o, f x :=
  iSup_option_toFinset o f

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