count_true_le_count_false_add_one

English

Let l be a finite alternating list of booleans. Then the number of true entries in l is at most the number of false entries in l plus 1.

Русский

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

LaTeX

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

Lean4

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

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