filter_union — Mathlib

English

Filter distributes over union: for any predicate p, filter p (s ∪ t) = filter p s ∪ filter p t.

Русский

Фильтр распределяется по объединению: filter p (s ∪ t) = filter p s ∪ filter p t.

LaTeX

$$$\\forall p\\, [\\text{DecidablePred } p],\\ filter\\ p (s \\cup t) = filter\\ p s \\cup filter\\ p t.$$$

Lean4

@[simp]
theorem filter_union (p : α → Prop) [DecidablePred p] (s t : Multiset α) : filter p (s ∪ t) = filter p s ∪ filter p t :=
  by simp [(· ∪ ·), union]

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