Commit 2022-09-08 17:38 cd7f0626

View on Github →

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.

Estimated changes

Modified src/combinatorics/simple_graph/basic.lean

added theorem simple_graph.coe_edge_finset

added theorem simple_graph.delete_edges_sdiff_eq_of_le

added theorem simple_graph.delete_far.mono

added def simple_graph.delete_far

added theorem simple_graph.delete_far_iff

added theorem simple_graph.edge_finset_delete_edges

added theorem simple_graph.edge_finset_mono

added theorem simple_graph.edge_set_delete_edges

added theorem simple_graph.edge_set_mono

Modified src/combinatorics/simple_graph/clique.lean

added theorem simple_graph.is_n_clique.not_clique_free

Created src/combinatorics/simple_graph/triangle/basic.lean

added theorem simple_graph.clique_free.not_far_from_triangle_free

added theorem simple_graph.far_from_triangle_free.clique_finset_nonempty'

added theorem simple_graph.far_from_triangle_free.clique_finset_nonempty

added theorem simple_graph.far_from_triangle_free.mono

added theorem simple_graph.far_from_triangle_free.nonpos

added theorem simple_graph.far_from_triangle_free.not_clique_free

added def simple_graph.far_from_triangle_free

added theorem simple_graph.far_from_triangle_free_iff