count_not_add_count — Mathlib

English

For a list l of Bool and a Bool b, the sum of counts of !b and b equals the length of l.

Русский

Для списка l булевых значений и булевой переменной b сумма счётов !b и b равна длине списка.

LaTeX

$$$ \forall (l : List Bool) (b : Bool),\; count (\neg b) l + count b l = \text{length } l $$$

Lean4

@[simp]
theorem count_not_add_count (l : List Bool) (b : Bool) : count (!b) l + count b l = length l :=
  by
  have := length_eq_countP_add_countP (l := l) (· == !b)
  aesop (add simp this)

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