harris_kleitman): The Harris-Kleitman inequality (#14497)

Commit

3 years ago

feat(combinatorics/set_family/harris_kleitman): The Harris-Kleitman inequality (#14497) Lower/upper sets in `finset α` are (anti)correlated.

Author

YaelDillies

Parents