count_true_add_count_false

Mathlib.Data.Bool.Count

URI: https://scilib.ai/kg/mathlib#List.count_true_add_count_false

English

For any list l of Bool, count true l + count false l = length l.

Русский

Для любого списка булевых значений l, count true l + count false l = length l.

LaTeX

$$$ \forall (l : List Bool),\; count true l + count false l = length l $$$

Lean4

@[simp]
theorem count_true_add_count_false (l : List Bool) : count true l + count false l = length l :=
  count_not_add_count l false

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru