eraseNone_inter — Mathlib

English

EraseNone distributes over intersection: eraseNone(s ∩ t) = eraseNone(s) ∩ eraseNone(t).

Русский

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

LaTeX

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

Lean4

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

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