countP_cons_of_pos — Mathlib

English

Let p be a predicate on α and a ∈ α with p a. Then adding a to the front of a multiset s increases the count by 1: countP p (a ::ₘ s) = countP p s + 1.

Русский

Пусть p — предикат на α и p(a) истинно. Добавление элемента a в начало мультимножества увеличивает подсчет на 1: countP p (a ::ₘ s) = countP p s + 1.

LaTeX

$$$\operatorname{countP}(p, (a ::ₘ s)) = \operatorname{countP}(p, s) + 1 \quad\text{if } p(a)$$$

Lean4

@[simp]
theorem countP_cons_of_pos {a : α} (s) : p a → countP p (a ::ₘ s) = countP p s + 1 :=
  Quot.inductionOn s <| by simpa using fun _ => List.countP_cons_of_pos (p := (p ·))

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