# Documentation

Mathlib.Data.Bool.Count

# List of booleans #

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

@[simp]
theorem List.count_not_add_count (l : ) (b : Bool) :
List.count (!b) l + =
@[simp]
theorem List.count_add_count_not (l : ) (b : Bool) :
+ List.count (!b) l =
theorem List.Chain.count_not {b : Bool} {l : } :
List.Chain (fun x x_1 => x x_1) b lList.count (!b) l = + % 2
theorem List.Chain'.count_not_eq_count {l : } (hl : List.Chain' (fun x x_1 => x x_1) l) (h2 : Even ()) (b : Bool) :
List.count (!b) l =
theorem List.Chain'.count_false_eq_count_true {l : } (hl : List.Chain' (fun x x_1 => x x_1) l) (h2 : Even ()) :
theorem List.Chain'.count_not_le_count_add_one {l : } (hl : List.Chain' (fun x x_1 => x x_1) l) (b : Bool) :
List.count (!b) l + 1
theorem List.Chain'.count_false_le_count_true_add_one {l : } (hl : List.Chain' (fun x x_1 => x x_1) l) :
+ 1
theorem List.Chain'.count_true_le_count_false_add_one {l : } (hl : List.Chain' (fun x x_1 => x x_1) l) :
+ 1
theorem List.Chain'.two_mul_count_bool_of_even {l : } (hl : List.Chain' (fun x x_1 => x x_1) l) (h2 : Even ()) (b : Bool) :
2 * =
theorem List.Chain'.two_mul_count_bool_eq_ite {l : } (hl : List.Chain' (fun x x_1 => x x_1) l) (b : Bool) :
2 * = if Even () then else if (some b == ) = true then + 1 else - 1
theorem List.Chain'.length_sub_one_le_two_mul_count_bool {l : } (hl : List.Chain' (fun x x_1 => x x_1) l) (b : Bool) :
- 1 2 *
theorem List.Chain'.length_div_two_le_count_bool {l : } (hl : List.Chain' (fun x x_1 => x x_1) l) (b : Bool) :
/ 2
theorem List.Chain'.two_mul_count_bool_le_length_add_one {l : } (hl : List.Chain' (fun x x_1 => x x_1) l) (b : Bool) :
2 * + 1