mathlib3 documentation


List of booleans #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove lemmas about the number of ffs and tts in a list of booleans. First we prove that the number of ffs plus the number of tt equals the length of the list. Then we prove that in a list with alternating tts and ffs, the number of tts differs from the number of ffs by at most one. We provide several versions of these statements.

theorem list.count_bnot_add_count (l : list bool) (b : bool) :
theorem list.count_add_count_bnot (l : list bool) (b : bool) :
theorem list.chain.count_bnot {b : bool} {l : list bool} :
theorem list.chain'.count_bnot_eq_count {l : list bool} (hl : list.chain' ne l) (h2 : even l.length) (b : bool) :
theorem list.chain'.two_mul_count_bool_eq_ite {l : list bool} (hl : list.chain' ne l) (b : bool) :
2 * list.count b l = ite (even l.length) l.length (ite (b l.head') (l.length + 1) (l.length - 1))