length_div_two_le_count_bool — Mathlib

English

If l is alternating, then length(l) / 2 ≤ count b l for any boolean b.

Русский

Если l — чередующийся список, то length(l)/2 ≤ count b l для любого булевого b.

LaTeX

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

Lean4

theorem length_div_two_le_count_bool (hl : IsChain (· ≠ ·) l) (b : Bool) : length l / 2 ≤ count b l :=
  by
  rw [Nat.div_le_iff_le_mul_add_pred two_pos, ← tsub_le_iff_right]
  exact length_sub_one_le_two_mul_count_bool hl b

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