LeanAide GPT-4 documentation

Module: Mathlib.Data.Bool.Count


List.count_not_add_count

theorem List.count_not_add_count : ∀ (l : List Bool) (b : Bool), List.count (!b) l + List.count b l = l.length := by sorry

This theorem states that for any list of Boolean values, the total count of occurrences of a Boolean value and its negation in the list equals the length of the list. In other words, if you sum the number of times a particular boolean (either `true` or `false`) and its opposite appear in a list, you will always get the total number of elements in the list.

More concisely: For any list of Boolean values, the sum of the count of each Boolean value and its negation is equal to the length of the list.