Commit 2024-05-04 19:51 0ebb8ea3

View on Github →

feat: Locally linear graphs (#12526) Define predicates for a graph to have edge-disjoint triangles and to be locally linear (edge-disjoint triangles and each edge belongs to a triangle).

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean

added theorem SimpleGraph.EdgeDisjointTriangles.card_edgeFinset_le

added theorem SimpleGraph.EdgeDisjointTriangles.map

added def SimpleGraph.EdgeDisjointTriangles

added theorem SimpleGraph.LocallyLinear.card_edgeFinset

added theorem SimpleGraph.LocallyLinear.map

added def SimpleGraph.LocallyLinear

added theorem SimpleGraph.edgeDisjointTriangles_bot

added theorem SimpleGraph.edgeDisjointTriangles_iff_mem_sym2_subsingleton

added theorem SimpleGraph.farFromTriangleFree_of_disjoint_triangles

added theorem SimpleGraph.locallyLinear_bot

added theorem SimpleGraph.locallyLinear_comap

Modified Mathlib/Data/Finset/Card.lean

modified theorem Finset.card_eq_zero

added theorem Finset.card_ne_zero

modified theorem Finset.card_pos