eraseNone_union — Mathlib

English

EraseNone distributes over union: eraseNone(s ∪ t) = eraseNone(s) ∪ eraseNone(t).

Русский

EraseNone распределяет по объединению: eraseNone(s ∪ t) = eraseNone(s) ∪ eraseNone(t).

LaTeX

$$$\\text{eraseNone}(s \\cup t) = \\text{eraseNone}(s) \\cup \\text{eraseNone}(t)$$$

Lean4

@[simp]
theorem eraseNone_union [DecidableEq (Option α)] [DecidableEq α] (s t : Finset (Option α)) :
    eraseNone (s ∪ t) = eraseNone s ∪ eraseNone t := by
  ext
  simp

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