count_false_le_count_true_add_one

English

Let l be a finite list of booleans in which consecutive entries are different (an alternating sequence). Then the number of false entries in l is at most the number of true entries in l plus 1.

Русский

Пусть l — конечный список булевых значений, в котором соседние элементы различаются. Тогда число элементов false в l не превосходит числа элементов true в l плюс 1.

LaTeX

$$$$\forall l : \text{List Bool},\ \text{IsChain}(\\neq) l \rightarrow \#\{ i \mid l_i = \text{false} \} \le \#\{ i \mid l_i = \text{true} \} + 1.$$$$

Lean4

theorem count_false_le_count_true_add_one (hl : IsChain (· ≠ ·) l) : count false l ≤ count true l + 1 :=
  hl.count_not_le_count_add_one true

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