countP_sub — Mathlib

English

If s and t are multisets with t ≤ s, then for any predicate p, count_p(s − t) = count_p(s) − count_p(t).

Русский

Если t ≤ s, то для любого предиката p выполняется count_p(s − t) = count_p(s) − count_p(t).

LaTeX

$$$t \le s \Rightarrow \forall p,\; \operatorname{count}_p(s - t) = \operatorname{count}_p s - \operatorname{count}_p t$$$

Lean4

@[simp]
theorem countP_sub {s t : Multiset α} :
    t ≤ s → ∀ (p : α → Prop) [DecidablePred p], countP p (s - t) = countP p s - countP p t :=
  Quotient.inductionOn₂ s t fun _l₁ _l₂ hl _ _ ↦ List.countP_diff hl _

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