mathlib

cd7f0626 - feat(combinatorics/simple_graph/triangle/basic): add ε-triangle-free far graph predicate (#12988)

feat(combinatorics/simple_graph/triangle/basic): add ε-triangle-free far graph predicate (#12988) Define the property of being triangle-free far. This comes up in the triangle counting and triangle removal lemmas. Co-authored-by: Bhavik Mehta <bhavik.mehta8@gmail.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com>