Commit 2023-02-28 08:27 8cf80e8b

View on Github →

feat: Port Combinatorics.SimpleGraph.Triangle.Basic (#2494)

Estimated changes

Modified Mathlib.lean

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

added theorem SimpleGraph.CliqueFree.not_farFromTriangleFree

added theorem SimpleGraph.FarFromTriangleFree.cliqueFinset_nonempty'

added theorem SimpleGraph.FarFromTriangleFree.cliqueFinset_nonempty

added theorem SimpleGraph.FarFromTriangleFree.nonpos

added theorem SimpleGraph.FarFromTriangleFree.not_cliqueFree

added def SimpleGraph.FarFromTriangleFree

added theorem SimpleGraph.farFromTriangleFree.mono

added theorem SimpleGraph.farFromTriangleFree_iff