count_false_add_count_true

Mathlib.Data.Bool.Count

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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