count_false_eq_count_true — Mathlib

English

If hl is a chain (Ne) on l and length l is Even, then count false l = count true l.

Русский

Если hl образует цепочку по неравенству и длина l четная, то количество false в l равно количеству true в l.

LaTeX

$$$ \forall {l : List Bool},\; hl : List.IsChain (fun x y => x \neq y) l \rightarrow Even (length l) \rightarrow count false l = count true l $$$

Lean4

theorem count_false_eq_count_true (hl : IsChain (· ≠ ·) l) (h2 : Even (length l)) : count false l = count true l :=
  hl.count_not_eq_count h2 true

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