filter_add — Mathlib

English

Let p be a predicate on α. For any multisets s,t of α, the p-filter of s+t equals the sum of the p-filters of s and t.

Русский

Пусть p — предикат на α. Для любых мультимножеств s и t над α выполняется фильтрация по p от суммы s+t равна сумме фильтров по p от s и от t.

LaTeX

$$$\\mathrm{filter}_p(s+t) =\\;\\mathrm{filter}_p(s) + \\mathrm{filter}_p(t)$$$

Lean4

@[simp]
theorem filter_add (s t : Multiset α) : filter p (s + t) = filter p s + filter p t :=
  Quotient.inductionOn₂ s t fun _l₁ _l₂ => congr_arg ofList <| filter_append _ _

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