length_sub_one_le_two_mul_count_bool

English

If l is alternating and b is any boolean, then length(l) − 1 ≤ 2 × count b l.

Русский

Если l — чередующийся список и b — булева величина, то длина l минус единица не превосходит 2 × число вхождений b в l.

LaTeX

$$$$\forall l : \text{List Bool},\ \text{IsChain}(\\neq) l \rightarrow \forall b,\ \text{length}(l) - 1 \le 2 \cdot \#\{ i \mid l_i = b \}.$$$$

Lean4

theorem length_sub_one_le_two_mul_count_bool (hl : IsChain (· ≠ ·) l) (b : Bool) : length l - 1 ≤ 2 * count b l :=
  by
  rw [hl.two_mul_count_bool_eq_ite]
  split_ifs <;> simp [Nat.le_succ_of_le]

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