eraseNone_eq_biUnion — Mathlib

English

EraseNone of a finite set s of options equals the union, over all o in s, of the finset toFinset(o).

Русский

EraseNone множества s из опций равен объединению по всем o ∈ s конечного объединения toFinset(o).

LaTeX

$$$\\text{eraseNone}(s) = \\bigcup_{o\\in s} \\text{toFinset}(o).$$$

Lean4

theorem eraseNone_eq_biUnion [DecidableEq α] (s : Finset (Option α)) : eraseNone s = s.biUnion Option.toFinset :=
  by
  ext
  simp

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