count_add_count_not — Mathlib

English

For any l : List Bool and any Bool b, count b l + count (!b) l = length l.

Русский

Для любого списка булевых значений l и булевой переменной b сумма count b l и count (!b) l равна длине списка.

LaTeX

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

Lean4

@[simp]
theorem count_add_count_not (l : List Bool) (b : Bool) : count b l + count (!b) l = length l := by grind

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