two_mul_count_bool_le_length_add_one

English

For l alternating and any boolean b, 2 × count b l ≤ length l + 1.

Русский

Для чередующегося l и любого b: 2 × count b l ≤ length l + 1.

LaTeX

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

Lean4

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

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