Commit 2023-12-03 21:46 52950127

View on Github →

feat: More simple simple graph lemmas (#7712) A bunch of simple lemmas for simple graphs.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

added theorem Equiv.simpleGraph_refl

added theorem Equiv.simpleGraph_trans

added theorem Equiv.symm_simpleGraph

added theorem SimpleGraph.Embedding.coe_toHom

modified theorem SimpleGraph.Embedding.map_adj_iff

added theorem SimpleGraph.Hom.coe_id

added theorem SimpleGraph.Hom.coe_ofLe

added def SimpleGraph.Hom.ofLe

added theorem SimpleGraph.comap_adj

added theorem SimpleGraph.comap_comap

added theorem SimpleGraph.comap_id

added theorem SimpleGraph.comap_symm

added theorem SimpleGraph.deleteEdges_eq

added theorem SimpleGraph.disjoint_edgeSet

added theorem SimpleGraph.disjoint_fromEdgeSet

added theorem SimpleGraph.edgeSet_eq_empty

added theorem SimpleGraph.edgeSet_nonempty

added theorem SimpleGraph.fromEdgeSet_disjoint

added theorem SimpleGraph.map_adj_apply

added theorem SimpleGraph.map_id

added theorem SimpleGraph.map_map

added theorem SimpleGraph.map_symm

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

modified theorem SimpleGraph.farFromTriangleFree_iff

Modified Mathlib/Logic/Basic.lean

added theorem Iff.ne_left

added theorem Iff.ne_right

Modified Mathlib/Logic/Relation.lean

added theorem Relation.map_apply_apply

added theorem Relation.map_id_id

added theorem Relation.map_map